← all areas

Namespace groupCohomology 361 theorems

— 331 · Cores 6 · H1 1 · IsGradedCupProduct 4 · Kummer 19

directly in groupCohomology 331

• Locally constant classes unramified outside S give H¹(G_S,M) groupCohomology.eq_continuousH1S_of_forall_mem_iff 0 below · cited by 5 · depth 12
• H¹ under restriction of scalars of a representation groupCohomology.exists_bijective_H1_map_of_restrictScalars 0 below · cited by 2 · depth 12
• Finite-dimensionality of H¹ with restricted ramification groupCohomology.finiteDimensional_continuousH1S 3 below · cited by 9 · depth 12
• Strict equivalence of dual-number lifts versus coboundaries groupCohomology.dualLiftToCochain_sub_mem_oneCoboundaries_iff 0 below · cited by 1 · depth 13
• Unipotent first-order lifts on I are coboundaries there groupCohomology.dualLift_unipotentOn_iff_exists_cochain_eq_sub_conj 0 below · cited by 1 · depth 13
• Finiteness of continuous H¹ for open subgroups of G_q groupCohomology.finiteDimensional_continuousH1_of_isOpen_of_primeLocal 54 below · cited by 8 · depth 13
• Upper bound for continuous H¹ at q ≠ p groupCohomology.finrank_continuousClasses_le_invariants_add_dualTwist 26 below · cited by 2 · depth 13
• dim_{𝔽_p} H¹_{cont}(ℚₚ,μₚ)=2 for odd p groupCohomology.finrank_continuousClasses_ofChar_cycloChar_eq_two_of_primeLocal 26 below · cited by 1 · depth 13
• Greenberg–Wiles inequality: strict at S, relaxed at Q groupCohomology.greenbergWiles_le_strict_relaxed_continuousH1S 1,208 below · cited by 1 · depth 13
• Functoriality preserves continuous degree-one classes groupCohomology.map_apply_mem_continuousH1_comp 0 below · cited by 4 · depth 13
• Local triviality at Q gives classes unramified outside S groupCohomology.mem_continuousH1S_of_forall_map_primeLocalToGlobal_eq_zero 8 below · cited by 1 · depth 13
• Finiteness of continuous H¹ for local K ni ζₚ groupCohomology.finiteDimensional_continuousH1_fixingSubgroup_of_forall_apply_eq_of_primeLocal 31 below · cited by 1 · depth 14
• Dévissage to trivial lines for continuous H¹ and H² groupCohomology.finiteDimensional_continuous_of_forall_apply_eq_of_rank_one 12 below · cited by 2 · depth 14
• Finiteness propagates along the continuous cohomology sequence groupCohomology.finiteDimensional_continuous_of_shortExact 10 below · cited by 3 · depth 14
• Bound for inflation images in H¹ at a tame level groupCohomology.finrank_inflationImage_le_finrank_invariants_add_finrank_invariants_dualTwist 12 below · cited by 1 · depth 14
• Greenberg–Wiles formula for the pairing-free Selmer menu over ℚ groupCohomology.greenbergWiles_eq_unramifiedMenu_extArithLoc 1,207 below · cited by 1 · depth 14
• Continuous H¹(ℚₚ,μₚ) counted by ℚₚ^×/(ℚₚ^×)ᵖ groupCohomology.natCard_continuousClasses_ofChar_cycloChar_eq_natCard_units_quot_of_primeLocal 16 below · cited by 1 · depth 14
• Degree-one Shapiro lemma for continuous H¹ groupCohomology.nonempty_continuousH1_coind_linearEquiv_continuousH1 2 below · cited by 2 · depth 14
• Invariance of continuous H⁰, H¹, H² under isomorphic data groupCohomology.nonempty_continuous_linearEquiv_of_mulEquiv 0 below · cited by 11 · depth 14
• Vanishing of H¹ when |G| is invertible groupCohomology.subsingleton_H1_of_isUnit_card 0 below · cited by 5 · depth 14
• Vanishing of H¹ in the twisted dual of ad⁰ groupCohomology.H1pi_dualTwist_adjointTraceZero_eq_zero_of_finite_range 13 below · cited by 1 · depth 15
• A 1-cocycle is right u-invariant iff it vanishes at u groupCohomology.cocycles1_forall_apply_mul_right_eq_iff_apply_eq_zero 0 below · cited by 1 · depth 15
• Shapiro's lemma in degree one: cocycle-level injectivity groupCohomology.coind_cocycles1_mem_coboundaries1_of_eval_one_mem_coboundaries1 0 below · cited by 4 · depth 15
• Exactness of C^G → H¹(G,A) → H¹(G,B) groupCohomology.comp_mem_coboundaries1_iff_exists_invariants_sub_deltaCochain0 0 below · cited by 4 · depth 15
• Exactness at H¹(B) for level-constant cochains groupCohomology.comp_mem_coboundaries1_iff_exists_isLevelConstant1_sub_comp 0 below · cited by 4 · depth 15
• Exactness at H² in level-constant cochains, smooth B groupCohomology.comp_mem_levelCoboundaries2_iff_exists_levelCocycles2_sub_comp 1 below · cited by 5 · depth 15
• Exactness at H² of the level-constant connecting map groupCohomology.comp_mem_levelCoboundaries2_iff_exists_sub_deltaCochain1 0 below · cited by 5 · depth 15
• Connecting 0-cochain is a level-constant 1-cocycle groupCohomology.deltaCochain0_mem_cocycles1_and_isLevelConstant1 0 below · cited by 4 · depth 15
• Exactness at H¹ for level-constant continuous cochains groupCohomology.deltaCochain1_mem_levelCoboundaries2_iff 0 below · cited by 5 · depth 15
• Unramified, U-trivial cocycle representatives and inflation from G/(I∨ U) groupCohomology.exists_cocycles1_unramified_iff_mem_inflationImage_sup 2 below · cited by 1 · depth 15
• Degree-one Shapiro lifting of level-constant cocycles groupCohomology.exists_coind_cocycles1_isLevelConstant1_eval_one_eq 0 below · cited by 4 · depth 15
• Linearity of the connecting map on level-constant 1-cocycles groupCohomology.exists_linearMap_levelCocycles1_continuousH2_eq_continuousH2pi_deltaCochain1 3 below · cited by 4 · depth 15
• Local duality package in degree one at q∈ S groupCohomology.exists_localDualityPackage_res_dualTwist_extArithLoc 202 below · cited by 1 · depth 15
• Finite-dimensionality of the inflation image in H¹ groupCohomology.finiteDimensional_inflationImage 1 below · cited by 4 · depth 15
• Bound on dim H¹ for a group with cyclic quotient groupCohomology.finrank_H1_le_finrank_invariants_add_finrank_ker_of_cyclic_quotient 2 below · cited by 1 · depth 15
• Local Euler characteristic at p, with H² folded by duality groupCohomology.finrank_finiteQuotientH1_eq_invariants_add_dualTwist_add_finrank_of_primeLocal 250 below · cited by 2 · depth 15
• Smooth H¹ at q ≠ p: h¹ = h⁰(M) + h⁰(M^∨(1)) groupCohomology.finrank_finiteQuotientH1_eq_invariants_add_dualTwist_of_primeLocal_ne 44 below · cited by 2 · depth 15
• Dimension of the inflation image in H¹ groupCohomology.finrank_inflationImage_eq_finrank_H1_quotientToInvariants 0 below · cited by 3 · depth 15
• Dimension of the inflation image for cyclic quotient with vanishing norm groupCohomology.finrank_inflationImage_eq_finrank_invariants_of_norm_eq_zero 1 below · cited by 1 · depth 15
• Inflation image in H¹ bounded by invariants, cyclic quotient groupCohomology.finrank_inflationImage_le_finrank_invariants 1 below · cited by 1 · depth 15
• Archimedean Euler identity for M and its cyclotomic dual groupCohomology.finrank_invariants_archimedean_add_dualTwist_add_H1_eq 1 below · cited by 1 · depth 15
• Invariants of the twisted dual via the a-eigenspace on coinvariants groupCohomology.finrank_invariants_dualTwist_eq_finrank_ker_coinvariants_sub_smul 1 below · cited by 2 · depth 15
• Eigenspace bound for Frobenius on ̄ t-coinvariants via a model groupCohomology.finrank_ker_frobeniusOnCoinvariants_le_finrank_ker_of_model 0 below · cited by 1 · depth 15
• Vanishing rank of submodules of the archimedean slot H¹ groupCohomology.finrank_submodule_res_extArithLoc_archSlot_eq_zero 0 below · cited by 3 · depth 15
• Greenberg–Wiles inequality for the arithmetic localisation family, odd p groupCohomology.greenbergWilesLeAdm_extArithLoc_of_isTheta1_eval_of_ne_two 1,189 below · cited by 1 · depth 15
• Antitonicity of the inflation image in the subgroup groupCohomology.inflationImage_antitone 1 below · cited by 5 · depth 15
• Inflation image unchanged when W/U is a finite q-group groupCohomology.inflationImage_eq_inflationImage_of_forall_pow_mem 4 below · cited by 2 · depth 15
• Injectivity of restriction on H¹ when [G:S] is invertible groupCohomology.injective_H1_restriction_of_isUnit_index 1 below · cited by 3 · depth 15
• Localisation preserves continuous degree-one classes groupCohomology.locRes_extArithLoc_apply_mem_continuousH1 0 below · cited by 3 · depth 15
• Local invariant of χsmileκₐ equals χ(Frob) v_q(a) groupCohomology.localInv_smul_kummerCocycle_eq_apply_frobenius_mul_valuation 120 below · cited by 1 · depth 15
• Orthogonality under a pairing agreeing with θ on continuous classes groupCohomology.mem_orthogonal_iff_of_agree_on_continuous 0 below · cited by 1 · depth 15
• Level-constant classes in H¹(χ) count K^×/(K^×)ᵖ groupCohomology.natCard_continuousClasses_ofChar_eq_natCard_units_quot 8 below · cited by 1 · depth 15
• Connecting 2-cochain is independent of the chosen lift groupCohomology.preimageFun_comp_d12_sub_deltaCochain1_mem_levelCoboundaries2 0 below · cited by 6 · depth 15
• Unramified classes are isotropic for local duality at q groupCohomology.theta1_apply_eq_zero_of_mem_unramified_of_mem_unramified 10 below · cited by 1 · depth 15
• Two-sided nondegeneracy of a bijective pairing into the dual groupCohomology.theta1_nondegenerate_of_bijective 0 below · cited by 1 · depth 15
• Local Tate duality at q in all three degrees groupCohomology.bijective_theta_dualTwist_of_primeLocal 195 below · cited by 6 · depth 16
• A 1-cocycle vanishing on generators vanishes on the generated subgroup groupCohomology.cocycles1_apply_eq_zero_of_mem_closure 0 below · cited by 1 · depth 16
• Level-constancy of the connecting cochain δ¹(c) groupCohomology.deltaCochain1_mem_levelCocycles2 1 below · cited by 2 · depth 16
• Degree-two Poitou–Tate duality for S-level classes, odd p groupCohomology.exists_continuousH2S_locRes_eq_iff_and_surjective_sum_theta2_of_ne_two 664 below · cited by 1 · depth 16
• Inflated 2-cocycle with p-torsion coefficients is a coboundary groupCohomology.exists_eq_d12_of_invariant_of_mul_dvd_orderOf 2 below · cited by 1 · depth 16
• Finite level for the mod-p cyclotomic line groupCohomology.exists_level_ofChar_cycloChar_comp 1 below · cited by 11 · depth 16
• Poitou–Tate exactness in degree one, odd p groupCohomology.exists_mem_continuousH1S_locRes_eq_iff_forall_sum_theta_eq_zero_of_ne_two 757 below · cited by 1 · depth 16
• Existence of θ⁰ and θ² for an equivariant pairing groupCohomology.exists_theta0_and_theta2 0 below · cited by 10 · depth 16
• Existence of the bidegree-(1,1) cup-product duality map groupCohomology.exists_theta1 3 below · cited by 11 · depth 16
• Finite-dimensionality of H¹(G,A) for finite G groupCohomology.finiteDimensional_H1_of_finite 0 below · cited by 2 · depth 16
• Finiteness of continuous H² for a local Galois module groupCohomology.finiteDimensional_continuousH2_of_primeLocal 145 below · cited by 2 · depth 16
• Dimension formula for H¹ of a finite cyclic group groupCohomology.finrank_H1_add_finrank_range_norm 0 below · cited by 2 · depth 16
• dim H¹ = dim H⁰ for cyclic G with vanishing norm groupCohomology.finrank_H1_eq_finrank_invariants_of_norm_eq_zero 0 below · cited by 4 · depth 16
• Local Euler–Poincaré formula for continuous H¹ at p groupCohomology.finrank_continuousClasses_eq_invariants_add_continuousH2_add_finrank_of_primeLocal 243 below · cited by 2 · depth 16
• Local duality in degrees 2 and 0: dimension form groupCohomology.finrank_continuousH2_eq_invariants_dualTwist_of_primeLocal 197 below · cited by 2 · depth 16
• Global Euler–Poincaré characteristic over ℚ for odd p groupCohomology.finrank_invariants_add_finrank_continuousH2S_add_finrank_eq_of_ne_two 682 below · cited by 1 · depth 16
• dim Ш¹_S(M^∨(1)) = dim Ш²_S(M) for odd p groupCohomology.finrank_sha1_dualTwist_eq_finrank_sha2_of_ne_two 959 below · cited by 1 · depth 16
• Lower bound for continuous H¹ at q≠ p groupCohomology.invariants_add_dualTwist_le_finrank_continuousClasses 37 below · cited by 1 · depth 16
• Local invariant: normalisation and bijectivity groupCohomology.isLocalInv_localInv_and_bijective 118 below · cited by 6 · depth 16
• Multiplicative μₚ-cocycles versus additive cocycles of 𝔽ₚ(χ) groupCohomology.isMulCocycle1_pow_val_iff_mem_cocycles1_ofChar 0 below · cited by 2 · depth 16
• Level-constant coboundaries lie in level-constant 2-cocycles groupCohomology.levelCoboundaries2_le_levelCocycles2 0 below · cited by 3 · depth 16
• Local invariant of unramified carry class is v_q(a) mod p groupCohomology.localInv_apply_eq_valuation_of_carryFun 119 below · cited by 2 · depth 16
• Inflation images are carried into inflation images groupCohomology.map_inflationImage_le 0 below · cited by 1 · depth 16
• Additive coboundaries of 𝔽ₚ(χ) versus μₚ-coboundaries groupCohomology.mem_coboundaries1_ofChar_iff_exists_rootOfUnity 0 below · cited by 2 · depth 16
• Inflated classes are those with a cocycle vanishing on N groupCohomology.mem_inflationImage_iff_exists_cocycles1_apply_eq_zero 0 below · cited by 3 · depth 16
• Pairing cochain χsmileκₐ differs from inflated carry by a level coboundary groupCohomology.smul_kummerCocycle_sub_unitsInflate2_carryFun_mem_levelCoboundaries2 0 below · cited by 3 · depth 16
• H¹ vanishing for conjugates of SL₂(F) on (mathfraksl₂)^∨ groupCohomology.subsingleton_H1_dual_traceZero_of_toMatrix_eq_conj_specialLinearGroup_map 2 below · cited by 1 · depth 16
• Vanishing of H¹ with twisted dual trace-zero coefficients, characteristic 3 groupCohomology.subsingleton_H1_dual_traceZero_twist_of_injective_of_not_nine_dvd_card 1 below · cited by 1 · depth 16
• Vanishing of H¹(G,A) from vanishing on a subgroup of unit index groupCohomology.subsingleton_H1_of_subsingleton_H1_res_of_isUnit_index 2 below · cited by 1 · depth 16
• Local Tate duality over open subgroups of G_{ℚ_q} groupCohomology.bijective_theta_dualTwist_of_isOpen 196 below · cited by 1 · depth 17
• Descent of local duality along a subgroup of index prime to p groupCohomology.bijective_theta_dualTwist_of_res 135 below · cited by 1 · depth 17
• Local Tate duality at a Sylow level groupCohomology.bijective_theta_dualTwist_of_sylowLevel 186 below · cited by 2 · depth 17
• Surjectivity of continuous H² for local Galois subgroups groupCohomology.continuousH2MapHom_surjective_of_surjective_of_primeLocal 162 below · cited by 3 · depth 17
• Cup product of a 1-coboundary with a level-constant cocycle groupCohomology.cup_mem_levelCoboundaries2_of_mem_coboundaries1_left 0 below · cited by 1 · depth 17
• Cup product with the coboundary of a level-fixed vector groupCohomology.cup_mem_levelCoboundaries2_of_mem_coboundaries1_right 0 below · cited by 1 · depth 17
• Cup product of level-constant 1-cocycles is level-constant groupCohomology.cup_mem_levelCocycles2 0 below · cited by 5 · depth 17
• Additivity of the global Euler defect, p odd groupCohomology.eulerDefect_add_of_shortExact_of_ne_two 575 below · cited by 1 · depth 17
• Local Euler–Poincaré identity from five named inputs groupCohomology.euler_poincare_identity_of_hypotheses 26 below · cited by 1 · depth 17
• Unique local invariant functional on continuous H² at q groupCohomology.existsUnique_isLocalInv 117 below · cited by 1 · depth 17
• Every 2-cocycle of a finite cyclic group is cohomologous to a carry cocycle groupCohomology.exists_carry_H2pi_eq 1 below · cited by 9 · depth 17
• Injection of Ш¹_S(M^∨(1)) into the dual of Ш²_S(M) groupCohomology.exists_injective_sha1_dualTwist_to_dual_sha2_of_ne_two 957 below · cited by 1 · depth 17
• Smooth finite Galois module unramified outside S trivialises over finite F groupCohomology.exists_isUnramifiedOutside_forall_apply_eq_one_of_smooth 0 below · cited by 8 · depth 17
• Long exact sequence for S-ramified continuous cohomology in degrees 0,1,2 groupCohomology.exists_les_continuousHS_of_shortExact_of_isLevelConstant 4 below · cited by 2 · depth 17
• Nonzero continuous H² class matching an unramified carry cocycle groupCohomology.exists_levelCocycles2_ofChar_cycloChar_isLocalInv_witness 33 below · cited by 4 · depth 17
• Level and Sylow data for a smooth local 𝔽ₚ-representation groupCohomology.exists_level_sylow_of_primeLocal 3 below · cited by 1 · depth 17
• Poitou–Tate degree-one existence at S, odd p groupCohomology.exists_mem_continuousH1S_locRes_eq_of_forall_sum_theta_eq_zero_of_ne_two 756 below · cited by 1 · depth 17
• Degree-two localisation: supplement bounded by h⁰(M^∨(1)), p odd groupCohomology.exists_range_locRes_continuousH2S_sup_eq_top_finrank_le_finrank_invariants_dualTwist_of_ne_two 663 below · cited by 1 · depth 17
• Finiteness of continuous H¹ and H² for local Galois groups groupCohomology.finiteDimensional_continuousH1_and_continuousH2_of_isOpen_of_primeLocal 145 below · cited by 1 · depth 17
• Tate's global Euler characteristic for a coinduced S-level module groupCohomology.finiteDimensional_continuousH2S_coind_and_finrank_eq 562 below · cited by 2 · depth 17
• Finiteness of continuous H² for smooth mod p modules over open subgroups locally at q groupCohomology.finiteDimensional_continuousH2_of_isOpen_of_primeLocal 144 below · cited by 3 · depth 17
• Tame local Euler characteristic for subgroups of Gₚ groupCohomology.finrank_continuousH1_eq_invariants_add_dualTwist_add_index_mul_of_tame 66 below · cited by 1 · depth 17
• Continuous H² of the cyclotomic line on open subgroups groupCohomology.finrank_continuousH2_ofChar_cycloChar_of_isOpen 114 below · cited by 4 · depth 17
• Local H²(ℚ_q,μₚ) is one-dimensional groupCohomology.finrank_continuousH2_ofChar_cycloChar_of_primeLocal 113 below · cited by 3 · depth 17
• Isomorphism invariance of the global Euler terms groupCohomology.finrank_eulerTerms_eq_of_iso 0 below · cited by 1 · depth 17
• Depth bound: h⁰(M)+h⁰(M^∨(χ)) at most the inflation image groupCohomology.finrank_invariants_add_finrank_invariants_dualTwist_le_finrank_inflationImage 16 below · cited by 1 · depth 17
• Unit-root inertia classes in H¹ span at most a line groupCohomology.finrank_span_H1_unitRootInertia_le_one 279 below · cited by 1 · depth 17
• Vanishing of H¹(SL₂(F),mathfraksl₂(k)) in characteristic 3 groupCohomology.subsingleton_H1_specialLinearGroup_fin_two_traceZero_algebra_of_charP_three 1 below · cited by 1 · depth 17
• Vanishing of the sum of local invariants, p odd groupCohomology.sum_localInv_locRes2S_eq_zero_of_ne_two 462 below · cited by 3 · depth 17
• Sum of local Tate pairings of global classes vanishes, p odd groupCohomology.sum_theta1_locRes_eq_zero_of_mem_continuousH1S_of_ne_two 464 below · cited by 2 · depth 17
• Bijectivity of θ⁰ and θ² for a trivial 𝔽ₚ-line groupCohomology.bijective_theta0_theta2_of_trivial_line_of_isOpen 115 below · cited by 1 · depth 18
• Local duality in degree one for a trivial line groupCohomology.bijective_theta1_of_trivial_line_of_isOpen 102 below · cited by 1 · depth 18
• Shapiro transport of duality to a coinduced pair groupCohomology.bijective_theta_coind 7 below · cited by 2 · depth 18
• Local duality over S descends from a subgroup of index prime to p groupCohomology.bijective_theta_dualTwist_of_res_of_isOpen 20 below · cited by 1 · depth 18
• Duality maps transfer along a compatible group isomorphism groupCohomology.bijective_theta_of_mulEquiv 0 below · cited by 1 · depth 18
• Duality maps descend to retracts of dual pairs groupCohomology.bijective_theta_of_retract 1 below · cited by 2 · depth 18
• Continuous duality passes to extensions of representations groupCohomology.bijective_theta_of_shortExact 15 below · cited by 1 · depth 18
• The carry 2-cochain of a cyclic group is a cocycle groupCohomology.carryFun_mem_cocycles2 0 below · cited by 28 · depth 18
• Carry class in H² vanishes iff the element is a norm groupCohomology.carry_H2pi_eq_zero_iff 0 below · cited by 13 · depth 18
• Degree-two Shapiro injectivity for level coboundaries groupCohomology.coind_mem_levelCoboundaries2_of_eval_one_mem_levelCoboundaries2 0 below · cited by 7 · depth 18
• Continuous Kummer map H²(G_K,μₚ)→ H²(G_K,Ω^×): injective with p-torsion image groupCohomology.continuousH2Map_kummerRep_injective_and_range_iff_smul_eq_zero 15 below · cited by 5 · depth 18
• Cup product of level-S cocycles and local invariants groupCohomology.cupCochain_mem_levelCocyclesS2_and_theta1_eq_localInv_locRes2S 3 below · cited by 1 · depth 18
• Shapiro's lemma in degree two: surjectivity on level cocycles groupCohomology.exists_coind_mem_levelCocycles2_eval_one_eq 0 below · cited by 5 · depth 18
• Cokernel bound for degree-two localisation at coinduced trivial modules groupCohomology.exists_forall_locRes_continuousH2S_coind_eq_add_sum_of_exists_sq_eq_neg_one 540 below · cited by 1 · depth 18
• Uniform killing of level 2-cocycles in a higher unramified layer groupCohomology.exists_forall_restrict_comap_rootsOfUnity_mem_levelCoboundaries2_of_primeLocal 157 below · cited by 1 · depth 18
• An injective functional on the archimedean continuous H² groupCohomology.exists_injective_dual_continuousH2_archimedean 0 below · cited by 1 · depth 18
• Descent to a p-group layer and its local invariants, p odd groupCohomology.exists_isPGroup_layer_inv_eq_localInv_locRes2S_div_and_sum_inv_eq_zero_of_ne_two 458 below · cited by 1 · depth 18
• A Sylow p-level inside an open subgroup of G_{ℚ_q} groupCohomology.exists_level_sylow_of_isOpen 9 below · cited by 1 · depth 18
• Poitou–Tate exactness in degree one at {∞}∪ S, p odd groupCohomology.exists_mem_continuousH1S_locRes_eq_iff_forall_sum_theta_eq_zero_arch_of_ne_two 750 below · cited by 1 · depth 18
• Dévissage of the degree-two localisation cokernel bound, odd p groupCohomology.exists_range_locRes_continuousH2S_sup_eq_top_of_surjective_of_ne_two 543 below · cited by 1 · depth 18
• Poitou–Tate pairing between `sha₁` of M^∨(1) and `sha₂` of M groupCohomology.exists_sha1_dualTwist_sha2_pairing_nondegenerate_of_ne_two 956 below · cited by 2 · depth 18
• Tate's Euler-characteristic formula for N(1) at level S groupCohomology.finiteDimensional_and_finrank_continuousH1Sr_twist_cycloChar_eq_of_trivial 553 below · cited by 1 · depth 18
• Finite-dimensionality of continuous H² of a trivial mod p line groupCohomology.finiteDimensional_continuousH2_fixingSubgroup_of_forall_apply_eq_of_primeLocal 112 below · cited by 1 · depth 18
• Finite-level 1-cocycles of a non-cyclotomic line have dimension ≤ 2 groupCohomology.finrank_cocycles_level_le_two_of_finrank_eq_one_of_not_cyclotomic 255 below · cited by 1 · depth 18
• Unit-inertia finite-level cocycles in 𝔽ₚ(ω) span at most a plane groupCohomology.finrank_cocycles_ofChar_cycloChar_level_unitRootInertia_le_two 55 below · cited by 1 · depth 18
• Tame local Euler characteristic over a finite base K/ℚₚ groupCohomology.finrank_continuousH1_eq_invariants_add_dualTwist_add_finrank_mul_of_tame_intermediateField 62 below · cited by 1 · depth 18
• Dimensions of invariants, twisted duals and continuous H¹ under group transport groupCohomology.finrank_continuousH1_res_mulEquiv_symm_eq 1 below · cited by 1 · depth 18
• End correction of the nine-term sequence, odd p groupCohomology.finrank_continuousH2S_add_archimedean_eq_of_shortExact_of_ne_two 569 below · cited by 1 · depth 18
• dim_{mathbb F_p} H²_{cts}(G_K,μₚ)=1 for K/mathbb Q_q finite groupCohomology.finrank_continuousH2_eq_one_of_equiv_rootsOfUnity_of_padic 107 below · cited by 3 · depth 18
• Invariants and continuous H¹, H² under reindexing S'≤ S groupCohomology.finrank_continuous_res_subgroupOf_eq_res_inclusion 0 below · cited by 1 · depth 18
• Euler characteristic of a coinduced module multiplies by p groupCohomology.finrank_euler_coind_res_index_eq_mul 14 below · cited by 1 · depth 18
• Additivity of continuous Euler characteristics in short exact sequences groupCohomology.finrank_euler_even_eq_odd_of_continuousH2MapHom_surjective 12 below · cited by 2 · depth 18
• Lower bound for dim H¹ by invariants and Frobenius kernel groupCohomology.finrank_invariants_add_finrank_ker_le_finrank_H1_of_depth 7 below · cited by 1 · depth 18
• Mackey decomposition of archimedean invariants of a coinduced module groupCohomology.finrank_invariants_archimedean_coind 2 below · cited by 2 · depth 18
• Reverse eigenspace comparison for a surjective model (D,π,φ_D) groupCohomology.finrank_ker_le_finrank_ker_frobeniusOnCoinvariants_of_model 0 below · cited by 1 · depth 18
• Archimedean sum splits between N and N(-1) groupCohomology.finsum_finrank_invariants_twist_inv_add_eq_index_mul 1 below · cited by 1 · depth 18
• Injectivity of degree-two inflation via continuous Hilbert 90 groupCohomology.mem_coboundaries2_of_unitsInflate2_mem_levelCoboundaries2 2 below · cited by 4 · depth 18
• Herbrand quotient one for U over a cohomologically trivial V groupCohomology.natCard_H1_eq_natCard_H2_ofMulDistribMulAction_of_subgroup 6 below · cited by 1 · depth 18
• Shapiro's lemma for H¹ with ramification restricted to S groupCohomology.nonempty_continuousH1S_coind_equiv_continuousH1Sr 4 below · cited by 1 · depth 18
• Degree-two Shapiro isomorphism for S-level cohomology groupCohomology.nonempty_continuousH2S_coind_equiv_continuousH2Sr 4 below · cited by 1 · depth 18
• Continuous Shapiro isomorphism in degree two for open S groupCohomology.nonempty_continuousH2_coind_linearEquiv_continuousH2 2 below · cited by 2 · depth 18
• Isomorphic representations give equivalent S-restricted H¹, H² groupCohomology.nonempty_continuousHSr_linearEquiv_of_iso 0 below · cited by 1 · depth 18
• Vanishing of H¹ when all multiplicative 1-cocycles are coboundaries groupCohomology.subsingleton_H1_ofMulDistribMulAction 0 below · cited by 2 · depth 18
• Vanishing of H¹(SL₂(F),mathfraksl₂) in characteristic three groupCohomology.subsingleton_H1_specialLinearGroup_fin_two_traceZero_of_charP_three 0 below · cited by 1 · depth 18
• Inflation of a 2-cocycle is level-constant groupCohomology.unitsInflate2_mem_levelCocycles2 0 below · cited by 5 · depth 18
• Global degree-one reading as a sum of local pairings groupCohomology.alpha1Read_comp_eq_sum_theta_of_forall_local 4 below · cited by 2 · depth 19
• Degree-one local duality at q: bijectivity of θ groupCohomology.bijective_of_isTheta1_localInv_extArithLoc 201 below · cited by 1 · depth 19
• Vanishing of level-S H² for the mod p cyclotomic character groupCohomology.continuousH2S_ofChar_cycloChar_eq_zero_of_not_mem 7 below · cited by 1 · depth 19
• Second cup-product square: δ¹csmile y-csmileδ⁰y is a level coboundary groupCohomology.cup20_deltaCochain1_sub_cup_deltaCochain0_mem_levelCoboundaries2 0 below · cited by 1 · depth 19
• Evaluation at 1 commutes with the cup cochain on coinduced modules groupCohomology.cupCochain_coind_apply_one 0 below · cited by 1 · depth 19
• Cup product against connecting cochains is a level coboundary groupCohomology.cup_deltaCochain0_add_cup02_deltaCochain1_mem_levelCoboundaries2 0 below · cited by 1 · depth 19
• Exactness at C^G of the connecting sequence groupCohomology.deltaCochain0_mem_coboundaries1_iff 0 below · cited by 3 · depth 19
• Reading δ-images in ℤ/p through an injective invariant groupCohomology.exists_alpha1Read_of_injective_invariant 0 below · cited by 2 · depth 19
• Extending a value on the tame generator to a 1-cocycle groupCohomology.exists_cocycles1_apply_eq_of_frobenius_tame_relations 0 below · cited by 1 · depth 19
• Descent of a cyclotomic mod-p 2-cocycle to F^× groupCohomology.exists_cocycles2_units_eq_pow_of_levelCocyclesS2_ofChar_cycloChar 0 below · cited by 1 · depth 19
• Existence of corestriction with corcircres=[G:H] groupCohomology.exists_corestriction_comp_res_eq_index_nsmul 2 below · cited by 12 · depth 19
• Cocycles with values in Fₙ are coboundaries modulo Fₙ₊₁ groupCohomology.exists_div_mem_of_isMulCocycle1_of_presentation 0 below · cited by 1 · depth 19
• Lifting a 2-cocycle through a presented filtration step groupCohomology.exists_div_mem_of_isMulCocycle2_of_presentation 0 below · cited by 1 · depth 19
• Hilbert 90 for locally constant cocycles on K's fixing subgroup groupCohomology.exists_eq_smul_div_of_isMulCocycle1_fixingSubgroup 1 below · cited by 3 · depth 19
• Degree-two localisation for coinduced modules: cokernel of rank one groupCohomology.exists_forall_locRes_continuousH2S_coind_trivial_eq_add_smul 538 below · cited by 1 · depth 19
• A uniform level killing all continuous H² classes groupCohomology.exists_forall_restrict_comap_mem_levelCoboundaries2_of_finiteDimensional 0 below · cited by 1 · depth 19
• Inflation H¹(Gal(F/ℚ),B)→ H¹(Γ,M): injective, with image the F-split classes groupCohomology.exists_inflate_H1_injective_range_iff_split 0 below · cited by 2 · depth 19
• A common unramified Galois splitting field for H¹_S groupCohomology.exists_isGalois_forall_mem_continuousH1S_exists_cocyclesOne 4 below · cited by 2 · depth 19
• A Galois S-level containing ζₚ and p-th roots of S groupCohomology.exists_isGalois_isUnramifiedOutside_mem_levelCocyclesS2_continuousH2Spi_eq_of_mem 7 below · cited by 1 · depth 19
• Existence of a global degree-two bridge map groupCohomology.exists_isGlobalBridge2 3 below · cited by 2 · depth 19
• Existence of the degree-two local bridge Λ groupCohomology.exists_isLocalBridge2 0 below · cited by 2 · depth 19
• Poitou–Tate exactness at P¹_S: global direction, odd p groupCohomology.exists_mem_continuousH1S_locRes_eq_of_forall_sum_theta_eq_zero_arch_of_ne_two 749 below · cited by 1 · depth 19
• Level 2-cocycles become coboundaries on an unramified subgroup groupCohomology.exists_restrict_comap_rootsOfUnity_mem_levelCoboundaries2_of_primeLocal 117 below · cited by 1 · depth 19
• Assembly of a non-degenerate Ш¹–Ш² pairing groupCohomology.exists_sha1_dualTwist_sha2_pairing_nondegenerate_of_assembly 0 below · cited by 1 · depth 19
• χ∪κₐ is not a level coboundary over a p-adic field groupCohomology.exists_smul_kummerCocycle_not_mem_levelCoboundaries2_of_padic 60 below · cited by 1 · depth 19
• Kummer rank formula for H¹_S(K, N(1)) groupCohomology.finiteDimensional_and_finrank_continuousH1Sr_twist_eq_unitsModP_add_sClassTorsionP 33 below · cited by 1 · depth 19
• Dimension of H²_S(K,N(1)) via S-class group and places groupCohomology.finiteDimensional_and_finrank_continuousH2Sr_twist_add_eq_sClassTorsionP_add_sum_placesRep 492 below · cited by 1 · depth 19
• Rank decomposition of H¹ along inflation–restriction groupCohomology.finrank_H1_eq_finrank_inflationImage_add_finrank_range_res 0 below · cited by 1 · depth 19
• Dimension of level-constant H¹(G,A) via cocycles on S groupCohomology.finrank_continuousClasses_eq_finrank_of_isUnit_index_of_forall_apply_eq 6 below · cited by 1 · depth 19
• Equivariant continuous Kummer theory in Hom form groupCohomology.finrank_continuousEquivariantHom_eq_finrank_invariants_linHom_dualTwist 11 below · cited by 1 · depth 19
• Inflation image in H¹ has dimension dim A^G groupCohomology.finrank_inflationImage_eq_finrank_invariants 2 below · cited by 1 · depth 19
• Restriction image and evaluation at a generator have equal rank groupCohomology.finrank_range_res_eq_finrank_range_evalAtGen 1 below · cited by 1 · depth 19
• Cocycles into a translation module are coboundaries groupCohomology.isCoboundary1_of_addEquiv_pi 0 below · cited by 1 · depth 19
• Every 2-cocycle is a coboundary for a translation module groupCohomology.isCoboundary2_of_addEquiv_pi 0 below · cited by 1 · depth 19
• Level-constancy of local cochains via finite extensions of ℚ_q groupCohomology.isLevelConstant1_primeLocalToGlobal_iff 5 below · cited by 1 · depth 19
• Injectivity of the degree-two local bridge map groupCohomology.isLocalBridge2_injective 0 below · cited by 2 · depth 19
• Vanishing of multiplicative 1-cocycles for a complete separated filtration groupCohomology.isMulCoboundary1_of_filtration 0 below · cited by 1 · depth 19
• Hilbert 90 for locally constant cocycles groupCohomology.isMulCoboundary1_of_isMulCocycle1_of_level 0 below · cited by 2 · depth 19
• Degree-two coboundary criterion for complete separated filtrations groupCohomology.isMulCoboundary2_of_filtration 0 below · cited by 1 · depth 19
• Localisation of an S-level global class is locally continuous groupCohomology.locRes_mem_continuousH1_of_mem_continuousH1S 1 below · cited by 2 · depth 19
• Restriction multiplies a carry class by f/gcd(ord s,f) groupCohomology.map_carry_H2pi_eq_smul_carry 3 below · cited by 10 · depth 19
• Change of group commutes with the connecting homomorphism groupCohomology.map_delta_eq_delta_map 0 below · cited by 5 · depth 19
• Shapiro bijectivity for H¹(G,Hom(R,Coind Y)) groupCohomology.map_resIhom_comp_ihom_map_counit_one_bijective 1 below · cited by 1 · depth 19
• Herbrand quotient 1 for an extension of a finite module groupCohomology.natCard_H1_eq_natCard_H2_of_shortExact_of_subsingleton_of_finite 5 below · cited by 2 · depth 19
• The p-torsion of H²_{cts}(Gal(ℚ̄_q/K),ℚ̄_q^×) has order p groupCohomology.natCard_torsionBy_continuousH2_units_eq_of_padic 91 below · cited by 2 · depth 19
• Poitou–Tate reciprocity at {∞}∪ S for odd p groupCohomology.sum_theta1_locRes_eq_zero_of_mem_continuousH1S_arch_of_ne_two 466 below · cited by 2 · depth 19
• Surjectivity of H²_S(N₂)→ H²_S(N₃) for odd p groupCohomology.surjective_continuousH2S_map_of_shortExact_of_ne_two 568 below · cited by 1 · depth 19
• Restriction to the top subgroup is bijective on cohomology groupCohomology.bijective_map_top_subtype 0 below · cited by 5 · depth 20
• Conjugating a 1-cocycle changes it by a coboundary groupCohomology.cocycles1_conj_apply_sub_eq 0 below · cited by 2 · depth 20
• Shapiro's isomorphism as restriction followed by evaluation at 1 groupCohomology.coindIso_hom_eq_map_subtype_comp_map_eval_one 0 below · cited by 9 · depth 20
• S-level H¹ via restriction to an index-prime-to-p subgroup groupCohomology.exists_continuousH1Sr_linearEquiv_inf_of_isTrivial_of_coprime 4 below · cited by 1 · depth 20
• Existence of corestriction satisfying the projection formula groupCohomology.exists_corestriction_map_map_res_eq_map_norm 2 below · cited by 3 · depth 20
• Cyclic cokernel for S-localisation of H²(G_{F,S},ℤ/p) groupCohomology.exists_forall_eq_res_continuousH2Sr_trivial_add_smul_of_exists_sq_eq_neg_one 533 below · cited by 1 · depth 20
• Degree-p Galois subextension cut out by an additive character groupCohomology.exists_intermediateField_mem_fixingSubgroup_iff_apply_eq_zero 0 below · cited by 1 · depth 20
• Invariant maps in degree 2 from a class formation axiom groupCohomology.exists_invariant_addCircle_of_natCard_H2_eq_of_span_eq_top 1 below · cited by 3 · depth 20
• Vanishing of H³(G_{ℚ,S},N) for odd p, at cochain level groupCohomology.exists_isLevelConstant_inhomogeneousCochains_d_eq_of_ne_two 567 below · cited by 1 · depth 20
• Existence of the degree-one local bridge map groupCohomology.exists_isLocalBridge1 0 below · cited by 3 · depth 20
• Restriction in degree 1 is an isomorphism onto V at invertible index groupCohomology.exists_linearEquiv_H1_of_forall_iff_of_isUnit_index 3 below · cited by 2 · depth 20
• Assembly of Poitou–Tate exactness at P¹_S from level data groupCohomology.exists_mem_continuousH1S_locRes_eq_of_forall_sum_theta_eq_zero_of_assembly 0 below · cited by 1 · depth 20
• Level-constant degree-two Shapiro–Mackey surjectivity for coinduced modules groupCohomology.exists_mem_levelCocycles2_res_coind_apply_eq 2 below · cited by 1 · depth 20
• Splitting of local Brauer classes by cyclotomic layers groupCohomology.exists_mem_split_adjoin_rootsOfUnity_of_padic 87 below · cited by 2 · depth 20
• Level H² classes over open subgroups of G_{ℚ_q} die in an unramified layer groupCohomology.exists_restrict_rootsOfUnity_mem_levelCoboundaries2_of_primeLocal 116 below · cited by 1 · depth 20
• Classes split by the unramified layer form ℤu groupCohomology.exists_split_adjoin_rootsOfUnity_eq_zmultiples_of_padic 59 below · cited by 1 · depth 20
• Conjugation-invariant classes in H¹(S,A) form a submodule groupCohomology.exists_submodule_mem_iff_conjInvariant 0 below · cited by 1 · depth 20
• Equivariant splitting of S-ramified H² with μₚ coefficients groupCohomology.finiteDimensional_and_nonempty_cyclotomicQuotientH2Rep_biprod_trivial_iso 489 below · cited by 1 · depth 20
• Finiteness of H¹ in the middle of a short exact sequence groupCohomology.finite_H1_of_shortExact 1 below · cited by 1 · depth 20
• Finiteness of H² in the middle of a short exact sequence groupCohomology.finite_H2_of_shortExact 1 below · cited by 2 · depth 20
• Vanishing of H¹ at the archimedean slot for odd p groupCohomology.finrank_H1_res_extArithLoc_archSlot_eq_zero 0 below · cited by 1 · depth 20
• Conjugation invariance up to coboundaries under trivial S-action groupCohomology.forall_exists_conj_sub_eq_iff_of_forall_apply_eq 0 below · cited by 1 · depth 20
• Kernel of a degree-one local bridge groupCohomology.isLocalBridge1_apply_eq_zero_iff 0 below · cited by 2 · depth 20
• Level change for the degree-one local bridge groupCohomology.isLocalBridge1_apply_resFunctor_map_comp_eq_of_exact 0 below · cited by 1 · depth 20
• Image of the degree-one local bridge is exactly H¹_{cts} groupCohomology.isLocalBridge1_mem_continuousH1_and_exists_eq 0 below · cited by 2 · depth 20
• Class formation axioms transport along an isomorphism of G-modules groupCohomology.isZero_H1_and_natCard_H2_and_span_map_of_iso 0 below · cited by 3 · depth 20
• Exactness of inflation–restriction in degree two groupCohomology.map_two_injective_and_range_eq_ker_of_isZero_H1 0 below · cited by 9 · depth 20
• Restriction to a finite-index subgroup is injective on H¹ groupCohomology.mem_coboundaries1_of_restrict_of_isUnit_index 0 below · cited by 3 · depth 20
• Herbrand quotient one: #H¹ = #H² for finite cyclic G groupCohomology.natCard_H1_eq_natCard_H2_of_finite 0 below · cited by 1 · depth 20
• Multiplicativity of the Herbrand quotient in a short exact sequence groupCohomology.natCard_H2_mul_of_shortExact 0 below · cited by 2 · depth 20
• H²_S with cyclotomic twist as tensor invariants groupCohomology.nonempty_continuousH2Sr_twist_linearEquiv_invariants_cyclotomicQuotientH2Rep_tensor 1 below · cited by 1 · depth 20
• Semi-local Shapiro–Mackey injectivity in degree two for coinduced modules groupCohomology.res_coind_mem_levelCoboundaries2_of_forall_apply_mem_levelCoboundaries2 2 below · cited by 1 · depth 20
• Pairing χsmileκₐ is a level coboundary iff a is a norm groupCohomology.smul_kummerCocycle_mem_levelCoboundaries2_iff_exists_norm_eq 22 below · cited by 1 · depth 20
• Additivity in a of the cyclic carry class in H² groupCohomology.carry_H2pi_add 0 below · cited by 1 · depth 21
• Restriction on continuous H² is injective when [G:S] is invertible groupCohomology.continuousH2Map_res_injective_of_isUnit_index 2 below · cited by 2 · depth 21
• Leibniz rule for the cup product of inhomogeneous cochains groupCohomology.d_cochainCup_apply 0 below · cited by 7 · depth 21
• Restriction in degree one is surjective at invertible index groupCohomology.exists_cocycles1_restrict_eq_add_of_isUnit_index 0 below · cited by 1 · depth 21
• Pinned relative Shapiro isomorphism in degree two groupCohomology.exists_continuousH2Sr_cyclotomicQuotientRep_equiv_pin 4 below · cited by 1 · depth 21
• Trivial finite-dimensional coefficients factor out of H²_S groupCohomology.exists_continuousH2Sr_trivial_tensor_linearEquiv 0 below · cited by 1 · depth 21
• Existence of corestriction on H² with corcircres=[G:S] groupCohomology.exists_cor_map_res_two_eq_index_smul 1 below · cited by 3 · depth 21
• Corank at most one for S-localisation of H²(Γ_F,mathcal O_S^×)[p] groupCohomology.exists_forall_eq_res_continuousH2Sr_galoisSUnitsRep_add_zsmul_of_sq_eq_neg_one 527 below · cited by 1 · depth 21
• Two-sided level invariance over a finite Galois extension groupCohomology.exists_isGalois_of_isLevelConstant1 0 below · cited by 1 · depth 21
• Existence of a graded cup product on group cohomology groupCohomology.exists_isGradedCupProduct 1 below · cited by 3 · depth 21
• Degree-three cochain exactness for ℤ/p over K supseteq μₚ groupCohomology.exists_isLevelConstant_d_two_three_eq_trivial_of_cycloChar_eq_one 559 below · cited by 1 · depth 21
• Vanishing of H³(G_{ℚ,S},N) from the cyclotomic levels groupCohomology.exists_isLevelConstant_inhomogeneousCochains_d_eq_of_forall_cyclotomicLevel 10 below · cited by 1 · depth 21
• Natural Kummer–Brauer exact sequence for H²_S with μₚ groupCohomology.exists_kummerBrauer_maps_continuousH2Sr_cyclotomic_natural 470 below · cited by 1 · depth 21
• Kummer theory in degree two for Galois S-units groupCohomology.exists_levelCocyclesSr2_sub_pow_mem_levelCoboundariesSr2_of_zsmul_mem 4 below · cited by 1 · depth 21
• Inflation into continuous H² as a ℤ-linear map groupCohomology.exists_linearMap_H2_continuousH2_ofAlgebraAutOnUnits 2 below · cited by 2 · depth 21
• Degree-two restriction onto G-invariant S-level classes is surjective groupCohomology.exists_mem_levelCocyclesSr2_res_sub_mem_levelCoboundariesSr2_of_isUnit_index 3 below · cited by 1 · depth 21
• Dévissage to the trivial line for level 2-cocycles groupCohomology.exists_restrict_mem_levelCoboundaries2_of_forall_pow_eq_one 2 below · cited by 1 · depth 21
• Trivial mod-p level 2-cocycles split over an unramified layer groupCohomology.exists_restrict_rootsOfUnity_mem_levelCoboundaries2_trivial_of_fixingSubgroup 109 below · cited by 1 · depth 21
• Inflation of unit-valued 2-cocycles along L ⊆ L' groupCohomology.exists_unitsInflate2_eq_of_le 0 below · cited by 1 · depth 21
• Dévissage bound #H²(G,A)≤#G for solvable G groupCohomology.finite_H2_and_natCard_H2_le_of_isSolvable 3 below · cited by 2 · depth 21
• Finiteness of Hⁿ(G,X₂) along a short exact sequence groupCohomology.finite_groupCohomology_of_shortExact 0 below · cited by 2 · depth 21
• Finiteness of Hⁿ⁺¹(G,L) for finite G and L finitely generated groupCohomology.finite_groupCohomology_succ_of_moduleFinite_int 20 below · cited by 2 · depth 21
• Inflation multiplies a cyclic carry class by |N| groupCohomology.infNatTrans_app_H2pi_carryFun_eq_card_nsmul 2 below · cited by 2 · depth 21
• Naturality of Shapiro's isomorphism in the coefficients groupCohomology.map_coindFunctor_map_comp_coindIso_hom 1 below · cited by 1 · depth 21
• Injectivity of inflation on H² when H¹ of the kernel vanishes groupCohomology.map_two_injective_of_injective_of_isZero_H1_ker 0 below · cited by 1 · depth 21
• Degree-two Kummer theory for μₚ⊂ℚ̄^× groupCohomology.mem_levelCoboundaries2_of_pow_mem_and_exists_pow_sub_mem_of_zsmul_mem 0 below · cited by 1 · depth 21
• Continuous degree-two inflation: classes split by L are inflated groupCohomology.mem_split_of_restrict_mem_levelCoboundaries2 3 below · cited by 1 · depth 21
• Cohomology classes of full order and restriction to subgroups groupCohomology.natCard_eq_and_span_map_eq_top_of_addOrderOf_eq_natCard 0 below · cited by 3 · depth 21
• H¹ of a trivial module as equivariant level-constant homomorphisms groupCohomology.nonempty_continuousH1Sr_inf_linearEquiv_eqLevelConstantHom 0 below · cited by 1 · depth 21
• Invariants of C ⊗ N as equivariant level-constant maps groupCohomology.nonempty_invariants_tensor_linearEquiv_eqLevelConstantHom 0 below · cited by 1 · depth 21
• Transport of Hⁿ along an isomorphism of group–module pairs groupCohomology.nonempty_linearEquiv_of_iso_res_mulEquiv 0 below · cited by 12 · depth 21
• Inflated carry cochain restricts to a level coboundary over E groupCohomology.unitsInflate2_carryFun_restrict_mem_levelCoboundaries2_of_dvd 53 below · cited by 1 · depth 21
• Inflation carries 2-coboundaries to level coboundaries groupCohomology.unitsInflate2_mem_levelCoboundaries2 0 below · cited by 3 · depth 21
• Hasse principle for p-torsion of H²(Γ_F,mathcal O_S^×) groupCohomology.continuousH2Sr_galoisSUnitsRep_eq_zero_of_forall_res_extArithIndex_eq_zero 270 below · cited by 1 · depth 22
• Pinned degree-two Shapiro isomorphism for ℤ/p(1) groupCohomology.exists_continuousH2Sr_cyclotomicQuotientRep_equiv_apply_eq 3 below · cited by 1 · depth 22
• p-power-torsion level-constant 3-cocycles on S-units are coboundaries groupCohomology.exists_isLevelConstant_d_two_three_eq_of_pPow_smul_sUnitsMax 486 below · cited by 1 · depth 22
• Descent of a degree-three cochain along an S-level prime to p groupCohomology.exists_isLevelConstant_inhomogeneousCochains_d_eq_of_res_fixingSubgroup_three 4 below · cited by 1 · depth 22
• Degree-three middle exactness for level-constant cochains groupCohomology.exists_isLevelConstant_three_eq_comp_add_d_of_shortExact 4 below · cited by 1 · depth 22
• Kummer maps δ,ι on S-level cohomology groupCohomology.exists_kummer_connecting_maps_continuousHSr_of_smooth_of_divisible 4 below · cited by 1 · depth 22
• Carry class upstairs plus a norm condition forces H²(Γ/S,C^S) cyclic of order [Γ:S] groupCohomology.exists_natCard_H2_eq_and_span_eq_top_of_carry_of_exists_norm_eq 6 below · cited by 2 · depth 22
• Local invariants of the p-primary S-unit H² groupCohomology.exists_natural_localInv_pPrimary_continuousH2Sr_sUnitsMax 464 below · cited by 2 · depth 22
• Local invariants on p-torsion of H²_S, with naturality groupCohomology.exists_natural_localInv_torsionBy_continuousH2Sr_sUnitsMax 465 below · cited by 2 · depth 22
• Torsion of classes in the S-level continuous H² groupCohomology.exists_nsmul_eq_zero_continuousH2Sr 4 below · cited by 1 · depth 22
• Level 2-cocycles in μₚ bound over an unramified layer groupCohomology.exists_restrict_adjoin_rootsOfUnity_mem_levelCoboundaries2_kummerRep_of_padic 105 below · cited by 1 · depth 22
• Finiteness and bound for H²(G,A) from H²(G/S,A^S) and H²(S,A) groupCohomology.finite_H2_and_natCard_H2_le 2 below · cited by 1 · depth 22
• Product of local H² p-torsion bounded via global S-units groupCohomology.finprod_natCard_torsionBy_continuousH2_le_mul_natCard_torsionBy_continuousH2Sr_galoisSUnitsRep_of_sq_eq_neg_one 513 below · cited by 1 · depth 22
• Kummer exactness in degrees 2–3 for S-level cohomology groupCohomology.kummer_degreeThree_exactness_continuousH2Sr_of_smooth_of_divisible 4 below · cited by 1 · depth 22
• Vanishing of the restricted carry class when [K_N:K]∣[E:K] groupCohomology.map_carryFun_adjoin_rootsOfUnity_eq_zero_of_dvd 50 below · cited by 1 · depth 22
• Order of H² equals #G under an invariant valuation groupCohomology.natCard_H2_ofMulDistribMulAction_eq_of_valuation 9 below · cited by 1 · depth 22
• Inflation from K(μ_{q^N-1}) restricts to inflation from E(μ_{q^N-1}) groupCohomology.unitsInflate2_restrict_sub_unitsInflate2_map_mem_levelCoboundaries2 0 below · cited by 1 · depth 22
• Degree-two inflation followed by restriction vanishes groupCohomology.H2res_comp_H2inf_eq_zero 0 below · cited by 1 · depth 23
• Change of S-unit coefficients is bijective on H² groupCohomology.bijective_continuousH2SrMap_sUnitsMaxRep_galoisSUnitsRep 3 below · cited by 3 · depth 23
• Hasse principle for 2-torsion classes split by F(i) groupCohomology.continuousH2Sr_galoisSUnitsRep_eq_zero_of_res_adjoin_sqrt_neg_one_eq_zero 266 below · cited by 1 · depth 23
• Hasse principle for the p-primary part of H² of S-units groupCohomology.eq_zero_of_forall_continuousH2Map_primeLocal_eq_zero_pPrimary_continuousH2Sr_sUnitsMax 258 below · cited by 1 · depth 23
• Restriction is injective on p-primary H² when index is prime to p groupCohomology.eq_zero_of_map_res_two_eq_zero_of_coprime 1 below · cited by 2 · depth 23
• Inflation surjects onto the kernel of restriction on H² groupCohomology.exists_H2inf_eq_of_H2res_eq_zero 0 below · cited by 1 · depth 23
• Classes in Hⁿ(G,B) come from a member of a directed family groupCohomology.exists_map_eq_of_directed_of_injective 0 below · cited by 1 · depth 23
• A generator of H²(Γ/S,C^S) from an inflated class groupCohomology.exists_natCard_H2_eq_and_span_eq_top_of_map_res_inf_smul_eq_zero 1 below · cited by 1 · depth 23
• Unramified splitting of level 2-cocycles over a p-adic field groupCohomology.exists_restrict_adjoin_rootsOfUnity_mem_levelCoboundaries2_of_padic 88 below · cited by 1 · depth 23
• Archimedean continuous H²: finite, of order at most two groupCohomology.finite_continuousH2_inf_map_conj_range_archimedeanLoc_and_natCard_le_two 0 below · cited by 1 · depth 23
• Inner automorphisms act trivially on group cohomology groupCohomology.map_conj_eq_id 0 below · cited by 4 · depth 23
• Degree-two Kummer comparison for S-units of the maximal extension groupCohomology.mem_levelCoboundaries2_sUnitsMaxRep_of_zsmul_mem_of_val_mem 1 below · cited by 2 · depth 23
• Order of H²(G,X₂) for an extension of ℤ groupCohomology.natCard_H2_eq_natCard_of_shortExact_of_iso_trivial 5 below · cited by 1 · depth 23
• At most p elements in p-torsion of local H² groupCohomology.natCard_torsionBy_continuousH2_inf_map_conj_range_primeLocalToGlobal_le 108 below · cited by 1 · depth 23
• Inflation is an isomorphism when H^{≥ 1}(N,A) vanishes groupCohomology.nonempty_quotientToInvariants_iso_of_forall_isZero 1 below · cited by 1 · depth 23
• Lower bound for p-torsion in H²(G_{F,S},𝒪_S^×) groupCohomology.pow_natCard_places_le_mul_natCard_torsionBy_continuousH2Sr_galoisSUnitsRep_of_sq_eq_neg_one 475 below · cited by 1 · depth 23
• Injectivity of inflation in degree 2 when H¹(S,A)=0 groupCohomology.H2inf_injective_of_subsingleton_H1_res 0 below · cited by 2 · depth 24
• Inflations of two S-level 2-cocycles with equal values agree groupCohomology.continuousH2SrInflation_H2pi_eq_of_le 0 below · cited by 8 · depth 24
• Hasse principle for p-primary S-unit classes H²_S(Γ_L, E_S) groupCohomology.eq_zero_of_forall_continuousH2Map_primeLocal_archimedean_eq_zero_pPrimary_continuousH2Sr_sUnitsMax 262 below · cited by 1 · depth 24
• Every S-ramified continuous H² class is an inflation groupCohomology.exists_continuousH2SrInflation_eq 3 below · cited by 2 · depth 24
• Torsion classes in H²_S inflate from torsion at a finite level groupCohomology.exists_continuousH2SrInflation_eq_of_nsmul_eq_zero 6 below · cited by 4 · depth 24
• Inflation–restriction in degree q under partial vanishing groupCohomology.inf_injective_and_exact_of_isZero_res 0 below · cited by 2 · depth 24
• Hilbert 90 for subgroups: vanishing of H¹(S,M^×) groupCohomology.isZero_H1_res_units_of_smul_eq 0 below · cited by 1 · depth 24
• #H²(G,ℤ) = #G for finite cyclic G groupCohomology.natCard_H2_trivial_int 0 below · cited by 1 · depth 24
• Vanishing of H¹(G,ℤ) for finite G acting trivially groupCohomology.subsingleton_H1_trivial_int 0 below · cited by 3 · depth 24
• Inflated H²_S class vanishes iff cocycle bounds deeper groupCohomology.continuousH2SrInflation_H2pi_eq_zero_iff 3 below · cited by 3 · depth 25
• Morphisms of representations preserve inhomogeneous n-cocycles groupCohomology.inhomogeneousCochains_d_comp_eq_zero_of_d_eq_zero 0 below · cited by 2 · depth 25
• Vanishing of H² when |G| is invertible groupCohomology.subsingleton_H2_of_isUnit_card 0 below · cited by 1 · depth 25
• Equal cohomology classes differ by a coboundary of cochains groupCohomology.exists_eq_add_d_of_pi_cocyclesMk_eq 0 below · cited by 2 · depth 27
• Exactness of Hⁿ at the middle term, on elements groupCohomology.exists_map_eq_of_map_eq_zero_of_injective_of_surjective 0 below · cited by 2 · depth 27
• Morphisms of representations commute with the inhomogeneous differential groupCohomology.inhomogeneousCochains_d_comp_apply 0 below · cited by 3 · depth 27
• Equivariant maps commute with the inhomogeneous coboundary groupCohomology.inhomogeneousCochains_d_comp_res_apply 0 below · cited by 2 · depth 27
• Pointwise vanishing of d∘ d on inhomogeneous cochains groupCohomology.inhomogeneousCochains_d_d_apply 0 below · cited by 2 · depth 27
• Coefficient change on an explicit cocycle class groupCohomology.map_id_pi_cocyclesMk_apply 1 below · cited by 1 · depth 27
• Functoriality of Hⁿ on explicit cocycle representatives groupCohomology.map_pi_cocyclesMk_apply 0 below · cited by 2 · depth 27
• The cohomology class of the zero cochain vanishes groupCohomology.pi_cocyclesMk_eq_zero_of_eq_zero 0 below · cited by 2 · depth 27
• Integer multiple of a cocycle class vanishes if it is a coboundary groupCohomology.zsmul_pi_cocyclesMk_eq_zero_of_eq_d 0 below · cited by 1 · depth 27
• Cochain-level Shapiro lemma in degree two for permutation modules groupCohomology.exists_forall_eq_mapDomain_smul_sub_add_of_forall_stabilizer 0 below · cited by 1 · depth 28
• Vanishing of H¹(G,ℤ[X]) for a permutation module groupCohomology.exists_forall_eq_sub_mapDomain_smul_of_forall_mul_eq_add_mapDomain_smul 0 below · cited by 1 · depth 28
• Cochains mod W killed by p^k after a coboundary groupCohomology.exists_pow_smul_sub_d_mem_of_isPGroup_of_d_mem 0 below · cited by 1 · depth 28
• Cochain-level Shapiro section for H² of a coinduced module groupCohomology.exists_two_cocycle_coind_apply_one_eq 0 below · cited by 1 · depth 28
• The class of m· x is m times the class of x groupCohomology.pi_cocyclesMk_zsmul 0 below · cited by 1 · depth 28

groupCohomology.Cores 6

• Corestriction after restriction is multiplication by the index on H² groupCohomology.Cores.cores_map_res_eq_index_smul 0 below · cited by 7 · depth 20
• Naturality of the degree-2 corestriction in the coefficients groupCohomology.Cores.map_cores_eq_cores_map 0 below · cited by 2 · depth 22
• Double coset formula for the degree-2 corestriction groupCohomology.Cores.map_subtype_cores_eq_finsum_cores_map 1 below · cited by 1 · depth 22
• Independence of the corestriction on H² from the transversal groupCohomology.Cores.cores_eq_cores 0 below · cited by 1 · depth 23
• Corestriction cochains commute with the inhomogeneous differential groupCohomology.Cores.corFin_d 0 below · cited by 1 · depth 25
• corcircres=[G:H] on 3-cocycles, up to an invariant coboundary groupCohomology.Cores.exists_d_eq_corFin_resFin_sub_index_smul_three 0 below · cited by 2 · depth 25

groupCohomology.H1 1

• Vanishing of H¹ when |G| is invertible groupCohomology.H1.subsingleton_of_isUnit_card 0 below · cited by 1 · depth 16

groupCohomology.IsGradedCupProduct 4

• Connecting map and cup product in the second variable groupCohomology.IsGradedCupProduct.cup_delta 1 below · cited by 2 · depth 21
• Connecting map commutes with cup product in the first variable groupCohomology.IsGradedCupProduct.delta_cup 1 below · cited by 2 · depth 21
• Functoriality of graded cup products under (f,φ⊗ψ) groupCohomology.IsGradedCupProduct.map_cup 1 below · cited by 1 · depth 21
• Uniqueness of a graded cup product on group cohomology groupCohomology.IsGradedCupProduct.unique 1 below · cited by 1 · depth 21

groupCohomology.Kummer 19

• Locally constant μₚ-valued cocycles are Kummer cocycles groupCohomology.Kummer.exists_kummerCocycle_eq_of_isMulCocycle1_of_level 1 below · cited by 4 · depth 14
• Surjectivity of the Kummer map via Hilbert 90 groupCohomology.Kummer.exists_kummerCocycle_eq_of_isMulCocycle1 0 below · cited by 2 · depth 15
• Kummer count: K^×/(K^×)ᵖ versus level-constant p-torsion characters groupCohomology.Kummer.natCard_quotient_range_pow_eq_natCard_levelHom 10 below · cited by 1 · depth 15
• Kummer characters from p-torsion homomorphisms when μₚ⊂ K groupCohomology.Kummer.exists_kummerCocycle_eq_of_monoidHom_fixingSubgroup 3 below · cited by 3 · depth 16
• Kummer cocycle is a coboundary of a root of unity groupCohomology.Kummer.exists_pow_eq_iff_exists_rootOfUnity_coboundary 0 below · cited by 4 · depth 16
• Triviality of the Kummer cocycle when μₚ⊆ K groupCohomology.Kummer.exists_pow_eq_iff_forall_kummerCocycle_eq_one 2 below · cited by 2 · depth 16
• Independence of the Kummer cocycle of the chosen p-th root groupCohomology.Kummer.kummerCocycle_eq_of_pow_eq_of_mem_fixingSubgroup 0 below · cited by 1 · depth 16
• Kummer cocycle is right-invariant under Gal(L/K(α)) groupCohomology.Kummer.kummerCocycle_mul_eq_of_mem_fixingSubgroup_adjoin 1 below · cited by 1 · depth 16
• Kummer cocycle is multiplicative on Gal(Ω/K) groupCohomology.Kummer.kummerCocycle_mul_of_mem_fixingSubgroup 0 below · cited by 2 · depth 16
• Kummer cocycle of a p-th root is μₚ-valued on Gal(Ω/K) groupCohomology.Kummer.kummerCocycle_pow_eq_one_of_mem_fixingSubgroup 0 below · cited by 2 · depth 16
• Kummer description of p-torsion cocycles on a fixing subgroup groupCohomology.Kummer.exists_kummerCocycle_eq_of_isMulCocycle1_fixingSubgroup 2 below · cited by 1 · depth 17
• Kummer descent criterion on the fixing subgroup of K groupCohomology.Kummer.exists_pow_eq_iff_of_fixingSubgroup 1 below · cited by 1 · depth 17
• Right-invariance of the Kummer cocycle under stabilisers of α groupCohomology.Kummer.kummerCocycle_mul_eq_of_apply_eq 0 below · cited by 2 · depth 17
• Kummer isomorphism as a cardinality identity groupCohomology.Kummer.natCard_H1_eq_natCard_quotient 6 below · cited by 1 · depth 18
• Kernel of the Kummer map is the group of p-th powers groupCohomology.Kummer.ker_kummerHom 2 below · cited by 1 · depth 19
• Surjectivity of the Kummer map for finite Galois L/K groupCohomology.Kummer.kummerHom_surjective 2 below · cited by 2 · depth 19
• Surjectivity of the Kummer map onto H¹(Gal(L/K),μₚ) groupCohomology.Kummer.exists_kummerClass_eq 1 below · cited by 1 · depth 20
• Vanishing of the Kummer class and p-th powers groupCohomology.Kummer.kummerClass_eq_zero_iff 1 below · cited by 1 · depth 20
• Galois equivariance of the Kummer cocycle groupCohomology.Kummer.kummerCocycle_conj 0 below · cited by 1 · depth 20