← all areas

Namespace PadicAlgCl 39 theorems

— 38 · ringOfIntegers 1

directly in PadicAlgCl 38

• Inertia moves p-th roots of x when p∤ v(x) PadicAlgCl.exists_mem_inertiaSubgroupIn_apply_ne_of_forall_pow_eq_of_not_dvd_valuation 24 below · cited by 3 · depth 11
• Value group of ℚₚ^{nr}(ζₚ) divides p^{1/(p-1)} PadicAlgCl.exists_nnnorm_pow_sub_one_eq_zpow_of_mem_adjoin_rootsOfUnity_coprime_sup_cyclotomicTower 21 below · cited by 1 · depth 12
• Inertia as the fixing subgroup of ℚₚ(μ_{p'}) PadicAlgCl.fixingSubgroup_adjoin_rootsOfUnity_coprime 0 below · cited by 4 · depth 12
• Socle thickening forces p ∣ vₚ(a) for Kummer data PadicAlgCl.exists_isUnit_forall_dvd_valuation_of_thickening 129 below · cited by 1 · depth 13
• Kummer datum from an upper-triangular cocycle package PadicAlgCl.exists_kummer_datum_of_triangular_package 2 below · cited by 1 · depth 13
• Inertia fixing μₚ and (1+p)^{1/p} acts residually trivially PadicAlgCl.exists_root_one_add_prime_forall_inertia_residual_trivial 0 below · cited by 1 · depth 13
• The degree-n unramified extension ℚₚ(μ_{pⁿ-1}) PadicAlgCl.finrank_adjoin_rootsOfUnity_eq_and_forall_norm_eq_zpow 18 below · cited by 5 · depth 13
• Degree of K·ℚₚ(μ_{pⁿ}) for absolutely unramified K PadicAlgCl.finrank_sup_cyclotomicTower_of_forall_norm_eq_zpow 1 below · cited by 1 · depth 13
• Level coboundary of χ∪κ_α forces p ∣ vₚ(a) PadicAlgCl.dvd_valuation_of_smul_kummerCocycle_pairing_mem_levelCoboundaries2 121 below · cited by 1 · depth 14
• A Frobenius element raising (p^N-1)-st roots of unity to the p-th power PadicAlgCl.exists_algEquiv_apply_eq_pow_of_pow_eq_one 11 below · cited by 3 · depth 14
• Unramified order-p character from a socle deviation of z² PadicAlgCl.exists_unramified_level_char_of_sq_sub_one_mem_span_socle 28 below · cited by 1 · depth 14
• Degrees in the p-power cyclotomic tower over ℚₚ PadicAlgCl.finrank_cyclotomicTower_and_pow_mem_fixingSubgroup 0 below · cited by 6 · depth 14
• Thickening: the χ-twisted Kummer cochain is a level coboundary PadicAlgCl.smul_kummerCocycle_pairing_mem_levelCoboundaries2_of_thickening 0 below · cited by 1 · depth 14
• Automorphisms act on m-th roots of unity as Frobenius powers PadicAlgCl.exists_apply_eq_pow_pow_of_pow_eq_one_of_not_dvd 17 below · cited by 3 · depth 15
• Every element of ℚ̄_q lies over an algebraic number PadicAlgCl.exists_mem_adjoin_padicEmbedding 0 below · cited by 1 · depth 17
• Unramified additive characters of G_{ℚ_p} span at most a line PadicAlgCl.finrank_span_addChar_inertia_eq_zero_finiteLevel_le_one 5 below · cited by 1 · depth 17
• Inertia-fixed integers in ℚ̄ₚ form a DVR PadicAlgCl.exists_dvr_subring_mem_inertiaSubgroupIn_iff_forall_apply_eq 21 below · cited by 4 · depth 18
• Unit-root inertia moves p-th roots of valuation prime to p PadicAlgCl.exists_mem_unitRootInertia_apply_ne_of_not_dvd_valuation 26 below · cited by 1 · depth 19
• Local inertia is the fixing subgroup of its fixed field PadicAlgCl.fixingSubgroup_fixedField_inertiaSubgroupIn 0 below · cited by 2 · depth 19
• Integrality over ℤₚ in ℚ̄ₚ is equivalent to ‖x‖≤ 1 PadicAlgCl.isIntegral_padicInt_iff_norm_le_one 0 below · cited by 14 · depth 19
• Normality of the inertia subgroup over ℚₚ PadicAlgCl.inertiaSubgroupIn_normal 0 below · cited by 2 · depth 23
• Inertia fixes roots of unity of order prime to p PadicAlgCl.apply_eq_self_of_forall_norm_sub_lt_one_of_pow_eq_one_of_coprime 0 below · cited by 1 · depth 26
• Frobenius lift and decomposition G_K=bigcup φⁿ I G_M PadicAlgCl.exists_frobeniusLift_forall_eq_pow_mul_inertia_mul_of_finiteDimensional 1 below · cited by 1 · depth 26
• Inertia-fixed elements have norm a power of ‖p‖ PadicAlgCl.exists_norm_eq_norm_pow_of_forall_inertia_apply_eq_self 22 below · cited by 1 · depth 26
• Teichmüller, Artin–Schreier and Lang congruences over ℚ̄ₚ PadicAlgCl.exists_rootOfUnity_norm_sub_lt_one_and_artinSchreier_and_lang 0 below · cited by 1 · depth 26
• Inertia in Gal(ℚ̄ₚ/ℚₚ) via norms PadicAlgCl.mem_inertiaSubgroupIn_iff_forall_norm_sub_lt_one 0 below · cited by 2 · depth 26
• Fixed points of all 𝒪_K-algebra automorphisms of ℚ̄ₚ PadicAlgCl.mem_range_algebraMap_of_forall_algEquiv_ringOfIntegers_apply_eq 0 below · cited by 1 · depth 26
• Ax's approximation lemma over ℚ̄ₚ PadicAlgCl.exists_mem_intermediateField_norm_sub_le_mul_of_forall_norm_algEquiv_sub_le 0 below · cited by 1 · depth 28
• Tate: trace surjectivity onto 𝔪 in the cyclotomic tower PadicAlgCl.exists_norm_le_one_and_trace_eq_of_norm_lt_one_sup_cyclotomicTower 10 below · cited by 1 · depth 28
• Tate's trace estimate in the p-cyclotomic tower PadicAlgCl.norm_sum_pow_apply_le_of_mem_cyclotomicTower 1 below · cited by 1 · depth 28
• Tate: different of MK(μ_{pⁿ})/K(μ_{pⁿ}) tends to one PadicAlgCl.exists_forall_traceDual_norm_le_rpow_sup_cyclotomicTower 8 below · cited by 1 · depth 29
• Trace surjectivity from a bound on the codifferent PadicAlgCl.exists_norm_le_one_and_trace_eq_of_forall_traceDual_norm_le 0 below · cited by 1 · depth 29
• Monogenic integers in finite extensions inside ℚ̄ₚ PadicAlgCl.exists_forall_exists_polynomial_aeval_eq_of_norm_le_one 1 below · cited by 2 · depth 30
• Tate: the cyclotomic tower is almost étale PadicAlgCl.exists_forall_rpow_neg_lt_norm_algEquiv_sub_of_mem_sup_cyclotomicTower 6 below · cited by 1 · depth 30
• Dedekind: f'(α) multiplies the codifferent into the integers PadicAlgCl.norm_mul_aeval_derivative_minpoly_le_one_of_forall_norm_trace_mul_le_one 1 below · cited by 1 · depth 30
• Compatible integral sections of a finite free p-adic tower PadicAlgCl.exists_forall_ringHom_apply_algebraMap_eq_of_free_of_ker_eq_span_pow 2 below · cited by 1 · depth 31
• Galois displacement on ℚₚ(μ_{pⁿ}) bounded by that of ζ PadicAlgCl.norm_apply_sub_le_norm_apply_sub_of_mem_cyclotomicTower 2 below · cited by 1 · depth 31
• Absolute values of ζ-1 and σζ-ζ in the p-cyclotomic tower PadicAlgCl.norm_apply_sub_self_eq_of_isPrimitiveRoot_of_mem_fixingSubgroup 0 below · cited by 1 · depth 31

PadicAlgCl.ringOfIntegers 1

• Ring of integers of a finite extension of ℚₚ PadicAlgCl.ringOfIntegers.finite_and_isDiscreteValuationRing_and_isAdicComplete 1 below · cited by 15 · depth 25