← all areas

Namespace ExtCitation 85 theorems

— 31 · Cyclotomic 5 · LocalLevel 49

directly in ExtCitation 31

• Splitting of continuous admissible extensions for p≥ 3 ExtCitation.extVanishingCts_of_three_le 16 below · cited by 1 · depth 6
• Mod p cyclotomic character computes the Galois action on μₚ ExtCitation.map_primitiveRoot_eq_pow_cycloExp 0 below · cited by 1 · depth 6
• (EXT) continuous admissible extensions split for p≥ 5 ExtCitation.extVanishingCts_of_five_le 11 below · cited by 1 · depth 7
• (EXT) vanishing at p = 3 for continuous admissible extensions ExtCitation.extVanishingCts_three 5 below · cited by 1 · depth 7
• Kummer reduction of continuous (EXT) vanishing for p ≥ 5 ExtCitation.extVanishingCts_of_e2ClassGroup_and_e2Units 2 below · cited by 1 · depth 8
• The chosen place above q lies over q ExtCitation.liesOverPrime_primeLocalPlace 0 below · cited by 10 · depth 10
• Mod-p cyclotomic character of a Frobenius at q ≠ p ExtCitation.coe_cycloChar_primeLocalToGlobal_eq_natCast_of_isFrobeniusAt 0 below · cited by 3 · depth 13
• Triviality of χₚ on automorphisms fixing ζₚ ExtCitation.cycloChar_eq_one_of_apply_eq_self_of_isPrimitiveRoot 0 below · cited by 10 · depth 13
• Existence of a Frobenius element in the image of G_{ℚ_q} ExtCitation.exists_isFrobeniusAt_apply_primeLocalToGlobal 0 below · cited by 11 · depth 13
• Unramified continuous classes at q have dimension h⁰ ExtCitation.finrank_unramifiedContinuousClasses_eq_finrank_invariants 18 below · cited by 2 · depth 13
• Triviality of χₚ on inertia at q≠ p ExtCitation.cycloChar_primeLocalToGlobal_eq_one_of_mem_inertia 0 below · cited by 2 · depth 14
• Frobenius generates the local group modulo inertia and level ExtCitation.exists_frobenius_pow_inv_mul_mem_inertia_sup_level 0 below · cited by 8 · depth 14
• A mod p generator of tame inertia at q≠ p ExtCitation.exists_inertia_pCharacter_generator 11 below · cited by 1 · depth 14
• Arbitrarily deep levels: Frobenius order divisible by n ExtCitation.exists_level_dvd_of_frobenius_pow_mem_inertia_sup 0 below · cited by 3 · depth 14
• A finite level containing μₚ, inside S, trivial on N ExtCitation.exists_padicLevel_fixingSubgroup_le_of_smooth 6 below · cited by 4 · depth 14
• Tame generator for inertia at a finite Galois level ExtCitation.exists_tame_generator_at_level 4 below · cited by 5 · depth 14
• Locally constant classes bounded by a uniform inflation bound ExtCitation.finrank_le_of_levelBound_of_forall_iff_exists_rightInvariantRep 4 below · cited by 1 · depth 14
• Unramified continuous classes have dimension h⁰ at q ExtCitation.finrank_unramifiedContinuousClasses_eq_finrank_invariants_of_cyclic_of_depth 14 below · cited by 1 · depth 14
• Inertia p-characters at q≠ p are powers of the Kummer character ExtCitation.exists_eq_kummerCharacter_pow 10 below · cited by 1 · depth 15
• Galois action on μₚ ⊂ ℚ̄_q via the cyclotomic character ExtCitation.exists_isPrimitiveRoot_smul_eq_pow_cycloChar_localGaloisToGlobal 0 below · cited by 10 · depth 15
• Nontriviality of the Kummer character on inertia at q ExtCitation.exists_kummerCharacter_ne_one 3 below · cited by 2 · depth 15
• Mod-p cyclotomic character of complex conjugation is -1 ExtCitation.cycloChar_complexConjugation_eq_neg_one 0 below · cited by 2 · depth 16
• Inertia at p acts non-trivially on p-th roots of unity ExtCitation.exists_localAut_mem_inertiaSubgroupIn_forall_pow_eq_and_not_modEq_one 5 below · cited by 5 · depth 16
• Local finite level implies global finite level ExtCitation.exists_finiteDimensional_fixingSubgroup_comap_primeLocalToGlobal_le 6 below · cited by 1 · depth 17
• Tame generator at a deep level with prescribed divisibilities ExtCitation.exists_tame_generator_at_level_of_dvd 12 below · cited by 1 · depth 17
• Tame-or-descent dichotomy for simple smooth mod p local representations ExtCitation.tame_or_descent_of_isSimple 13 below · cited by 1 · depth 17
• Unramified layers in an open subgroup of G_{ℚ_q} ExtCitation.comap_rootsOfUnity_levels_of_isOpen 27 below · cited by 2 · depth 18
• Mod p cyclotomic character trivial when ζₚ ∈ L ExtCitation.cycloChar_eq_one_of_mem_fixingSubgroup_of_isPrimitiveRoot_mem 0 below · cited by 4 · depth 18
• Open subgroups of Gal(ℚ̄_q/ℚ_q) are finite levels ExtCitation.exists_padicLevel_fixingSubgroup_eq_of_isOpen 5 below · cited by 4 · depth 18
• Global and local smoothness agree for G_q-modules ExtCitation.forall_exists_finiteDimensional_primeLocalToGlobal_iff 5 below · cited by 1 · depth 18
• Triviality of χₚ on Gal(ℚ̄_q/K) forces μₚ ⊂ K ExtCitation.exists_isPrimitiveRoot_of_cycloChar_localGaloisToGlobal_eq_one 1 below · cited by 1 · depth 19

ExtCitation.Cyclotomic 5

• Vanishing of the ω²-eigenspace of Cl(ℚ(ζₚ))/p ExtCitation.Cyclotomic.clGalAction_omegaEigenspace_two_eq_bot 6 below · cited by 1 · depth 8
• ω²-eigen-units that are local p-th powers at p ExtCitation.Cyclotomic.unitsOmegaEigenvector_two_eq_zero_of_local_pow 1 below · cited by 1 · depth 8
• One-dimensionality of the ω²-eigenspace of the cyclotomic units ExtCitation.Cyclotomic.finrank_unitsOmegaEigenspace_two 0 below · cited by 2 · depth 9
• Nonvanishing of the ω²-component of 1+ζₚ ExtCitation.Cyclotomic.omegaIdempotent_two_cycloUnitTwo_ne_zero 0 below · cited by 2 · depth 9
• A Thaine relation for a degree-one prime of K⁺ ExtCitation.Cyclotomic.thaine_relation_plusField 2 below · cited by 1 · depth 9

ExtCitation.LocalLevel 49

• Inertia at q moves an e-th root of q ExtCitation.LocalLevel.exists_mem_inertiaSubgroupIn_apply_ne_of_pow_eq_prime 2 below · cited by 3 · depth 10
• Kummer divisibility for q^{1/n} under inertia at q ExtCitation.LocalLevel.dvd_of_forall_inertia_apply_pow_eq 3 below · cited by 2 · depth 11
• A G_q-stable inertia-fixed level has degree at most f ExtCitation.LocalLevel.finrank_le_of_forall_resw_pow_eq 0 below · cited by 1 · depth 11
• Lifts of 𝔽_q-independent residues are orthonormal ExtCitation.LocalLevel.norm_sum_smul_eq_of_linearIndependent_resw 0 below · cited by 1 · depth 11
• Conjugates of m-th roots of unity are Frobenius powers ExtCitation.LocalLevel.exists_eq_pow_card_pow_of_mem_rootSet 9 below · cited by 1 · depth 15
• Fundamental identity ef=[K_w:ℚ_q] for R_w ExtCitation.LocalLevel.exists_ramification_inertia_Rw 3 below · cited by 10 · depth 15
• Relative ramification and inertia degrees in a tower of local fields ExtCitation.LocalLevel.exists_relative_ramification_inertia_Rw 3 below · cited by 7 · depth 15
• Finiteness of the residue field of R_w ExtCitation.LocalLevel.finite_residueField_Rw 2 below · cited by 10 · depth 15
• The valuation ring R_w of a finite extension of ℚ_q is a DVR ExtCitation.LocalLevel.isDiscreteValuationRing_Rw 2 below · cited by 12 · depth 15
• Reduction is injective on m-th roots of unity when q ∤ m ExtCitation.LocalLevel.residue_injOn_rootsOfUnity 0 below · cited by 3 · depth 15
• ζ₀^{q^a} is a K-conjugate of ζ₀ ExtCitation.LocalLevel.aeval_pow_card_residueField_minpoly_eq_zero 8 below · cited by 2 · depth 16
• ℚ_q-automorphisms of K_w preserve its ring of integers ExtCitation.LocalLevel.algEquiv_apply_mem_Rw_iff 0 below · cited by 5 · depth 16
• Normalised discrete valuation on a finite extension K_w/ℚ_q ExtCitation.LocalLevel.exists_valuation_units_Kw 3 below · cited by 6 · depth 16
• Index of principal unit subgroups at a finite local level ExtCitation.LocalLevel.index_principalUnits_Rw 9 below · cited by 3 · depth 16
• m-adic completeness of the ring of integers of K_w ExtCitation.LocalLevel.isAdicComplete_Rw 2 below · cited by 3 · depth 16
• Unit ball of a finite level equals integral closure of ℤ_q ExtCitation.LocalLevel.mem_Rw_iff_isIntegral 0 below · cited by 9 · depth 16
• A finite Galois level with nd ∣ m and φ^m fixing q^{1/n} ExtCitation.LocalLevel.exists_level_frobenius_pow_dvd_and_apply_eq 2 below · cited by 1 · depth 18
• A cohomologically trivial open subgroup of the local units ExtCitation.LocalLevel.exists_subgroup_units_forall_isMulCocycle 21 below · cited by 2 · depth 18
• Existence and uniqueness of the local fundamental class ExtCitation.LocalLevel.existsUnique_isLocalFundamentalClass 77 below · cited by 21 · depth 19
• A Galois-stable normal-basis lattice in a local field ExtCitation.LocalLevel.exists_normalBasis_lattice 3 below · cited by 1 · depth 19
• Tame local 𝔽ₚ[Δ]-dimension count for K_w^×/(K_w^×)ᵖ ExtCitation.LocalLevel.finrank_invariants_linHom_unitsModPow_of_isGalois_intermediateField 34 below · cited by 1 · depth 19
• Local class-formation axioms from a local fundamental class ExtCitation.LocalLevel.isZero_H1_and_natCard_H2_and_span_res_of_isLocalFundamentalClass 64 below · cited by 16 · depth 19
• Invariant isomorphism for H² of an unramified sub-layer ExtCitation.LocalLevel.exists_addEquiv_H2_quotientToInvariants_units_zmod_forall_carryFun 36 below · cited by 5 · depth 20
• Fixed field of a finite group acting on a q-adic layer ExtCitation.LocalLevel.exists_intermediateField_forall_mem_iff_smul_eq 0 below · cited by 5 · depth 20
• Galois over-layer carrying the unramified level of degree n ExtCitation.LocalLevel.exists_overlayer_unramified_level 23 below · cited by 4 · depth 20
• Local second inequality for H²(G,L^×), G solvable ExtCitation.LocalLevel.finite_H2_units_and_natCard_le_of_isSolvable 39 below · cited by 4 · depth 20
• Degree of a faithful layer: [L:ℚ_q]=|G| [K:ℚ_q] ExtCitation.LocalLevel.finrank_eq_natCard_mul_finrank_of_forall_mem_iff_smul_eq 0 below · cited by 16 · depth 20
• Counting Δ-maps into K_w^×/(K_w^×)^q ExtCitation.LocalLevel.finrank_invariants_linHom_unitsModPow_Kw_of_basis 33 below · cited by 1 · depth 20
• Restriction of the local fundamental class to a subgroup ExtCitation.LocalLevel.isLocalFundamentalClass_map_subtype 66 below · cited by 3 · depth 20
• Pinning in one unramified over-layer gives the local fundamental class ExtCitation.LocalLevel.isLocalFundamentalClass_of_pin 46 below · cited by 3 · depth 20
• Solvability of faithful finite group actions on q-adic fields ExtCitation.LocalLevel.isSolvable_of_faithfulSMul_of_padic 14 below · cited by 13 · depth 20
• Hilbert 90 for units along an injective restriction ExtCitation.LocalLevel.isZero_groupCohomology_one_res_units 1 below · cited by 7 · depth 20
• Inflation multiplies the local fundamental class by [L':L] ExtCitation.LocalLevel.map_eq_natCard_smul_of_isLocalFundamentalClass 30 below · cited by 5 · depth 20
• Equality of inflation images: solvable layer versus unramified layer ExtCitation.LocalLevel.range_infNatTrans_eq_of_unramified_level 68 below · cited by 1 · depth 20
• Unramified levels of equal index coincide ExtCitation.LocalLevel.eq_of_unramified_level_of_index_eq 7 below · cited by 1 · depth 21
• A common Galois overlayer for two finite layers ExtCitation.LocalLevel.exists_common_overlayer 0 below · cited by 2 · depth 21
• Fixed level L^N and N-invariant units as a G/N-representation ExtCitation.LocalLevel.exists_fixedLevel_quotientToInvariants_iso 0 below · cited by 3 · depth 21
• Frobenius and uniformiser for an unramified level over L^S ExtCitation.LocalLevel.exists_frobenius_uniformiser_inf_level 21 below · cited by 2 · depth 21
• A ℚ_q-basis ℤ_q-spans a lattice containing q^N R_w ExtCitation.LocalLevel.exists_pow_smul_mem_span_of_linearIndependent_of_mem_Rw 2 below · cited by 1 · depth 21
• Ramification index, residue degree and ψ ≡ φ^f mod N ExtCitation.LocalLevel.exists_ramificationIdx_inertiaDeg_mk_eq_mk_pow 7 below · cited by 2 · depth 21
• Ramification datum and q-powers on principal units of R_w ExtCitation.LocalLevel.exists_ramification_principalUnits_Rw 9 below · cited by 1 · depth 21
• Unramified layer of degree n with Frobenius and uniformiser ExtCitation.LocalLevel.exists_unramified_layer_frobenius_uniformiser 21 below · cited by 1 · depth 21
• Finite index of q^N R_w in R_w ExtCitation.LocalLevel.finiteIndex_toAddSubgroup_span_pow_Rw 7 below · cited by 1 · depth 21
• Index of mathfrak m_wⁿ in R_w equals (#κ_w)ⁿ ExtCitation.LocalLevel.index_toAddSubgroup_maximalIdeal_pow_Rw 5 below · cited by 2 · depth 21
• Carry classes of a reciprocity homomorphism equal (m|H'|)u ExtCitation.LocalLevel.infNatTrans_carryFun_eq_mul_natCard_smul_of_forall_norm_mem 82 below · cited by 1 · depth 21
• Restriction multiplies the local invariant by the index [G:S] ExtCitation.LocalLevel.inv_res_inf_eq_index_smul_inv 16 below · cited by 1 · depth 21
• Triviality of inertia at an unramified level ExtCitation.LocalLevel.mem_of_unramified_level_of_forall_norm_smul_sub_lt_one 5 below · cited by 5 · depth 21
• #H²(G,L^×)=#G for a cyclic local Galois group ExtCitation.LocalLevel.natCard_H2_units_eq_natCard_of_isCyclic 33 below · cited by 5 · depth 21
• Fixed field of N∩ S lies in a cyclotomic layer over K' ExtCitation.LocalLevel.mem_adjoin_rootsOfUnity_of_forall_inf_smul_eq 6 below · cited by 1 · depth 22