← all areas

Namespace IsDedekindDomain 57 theorems

— 4 · FiniteAdeleRing 9 · HeightOneSpectrum 43 · selmerGroup 1

directly in IsDedekindDomain 4

• Étale quotient by a separable polynomial over a Dedekind domain IsDedekindDomain.etale_quotient_map_span_of_separable_of_forall_isUnramifiedAt 1 below · cited by 2 · depth 18
• Étale fibre of B/k[X] at an unramified irreducible h IsDedekindDomain.etale_quotient_map_span_of_forall_isUnramifiedAt 0 below · cited by 2 · depth 19
• A single nonzero element cutting out the ramified primes IsDedekindDomain.exists_ne_zero_forall_isUnramifiedAt_of_notMem 0 below · cited by 3 · depth 19
• Ramification index one makes π a uniformiser at q IsDedekindDomain.exists_zpow_mul_div_of_ramificationIdx_eq_one 0 below · cited by 1 · depth 35

IsDedekindDomain.FiniteAdeleRing 9

• Finite adeles are K-translates of integral adeles IsDedekindDomain.FiniteAdeleRing.exists_sub_algebraMap_mem_adicCompletionIntegers 0 below · cited by 5 · depth 13
• Finite adeles decompose as K + widehatA IsDedekindDomain.FiniteAdeleRing.exists_forall_sub_algebraMap_mem_adicCompletionIntegers 0 below · cited by 5 · depth 16
• Common denominator for a finite adele IsDedekindDomain.FiniteAdeleRing.exists_mem_nonZeroDivisors_forall_mul_apply_mem_adicCompletionIntegers 0 below · cited by 3 · depth 17
• A common denominator for a compact set of finite adeles IsDedekindDomain.FiniteAdeleRing.exists_ne_zero_forall_mul_apply_mem_adicCompletionIntegers_of_isCompact 0 below · cited by 14 · depth 17
• Finite ideles surject onto the class group with kernel widehat R^× K^× IsDedekindDomain.FiniteAdeleRing.exists_monoidHom_units_classGroup_surjective_ker_eq 0 below · cited by 3 · depth 18
• The ideal content homomorphism on finite idèles IsDedekindDomain.FiniteAdeleRing.exists_contentHom_eq_finprod_and_mem_sup_unitIdelesOutside_iff 0 below · cited by 4 · depth 19
• Finite idèles: S-units together with K^× generate everything IsDedekindDomain.FiniteAdeleRing.unitIdelesOutside_sup_range_eq_top 0 below · cited by 1 · depth 19
• Idelic presentation of the class group of a Dedekind domain IsDedekindDomain.FiniteAdeleRing.nonempty_classGroup_mulEquiv_units_quotient_unitIdeles_sup_range 0 below · cited by 1 · depth 32
• Haar measure on S-integral part of finite adeles IsDedekindDomain.FiniteAdeleRing.exists_map_restrict_integralOutside_eq_smul_pi_of_isAddHaarMeasure 1 below · cited by 1 · depth 35

IsDedekindDomain.HeightOneSpectrum 43

• Principality of a height-one prime from a pulled-back simple zero IsDedekindDomain.HeightOneSpectrum.exists_eq_span_singleton_of_map_eq 0 below · cited by 1 · depth 9
• Finiteness of the residue field of 𝒪ᵥ IsDedekindDomain.HeightOneSpectrum.finite_residueField_adicCompletionIntegers 0 below · cited by 16 · depth 10
• Completion at a finite place is adically complete IsDedekindDomain.HeightOneSpectrum.isAdicComplete_adicCompletionIntegers 0 below · cited by 12 · depth 10
• v-adic valuation as exp of minus the multiplicity of v IsDedekindDomain.HeightOneSpectrum.valuation_eq_exp_neg_count 0 below · cited by 2 · depth 10
• Ideal-power inertia equals lower ramification groups at a finite place IsDedekindDomain.HeightOneSpectrum.inertia_asIdeal_pow_succ_eq_map_subtype_lowerRamificationGroup 2 below · cited by 2 · depth 14
• Stabiliser of a prime equals its valuation ring's decomposition group IsDedekindDomain.HeightOneSpectrum.stabilizer_asIdeal_eq_decompositionSubgroup_valuationSubring 0 below · cited by 5 · depth 14
• Finite places of ℚ are generated by rational primes IsDedekindDomain.HeightOneSpectrum.exists_prime_and_asIdeal_eq_span_ringOfIntegers_rat 0 below · cited by 9 · depth 15
• Unramified local units are norms: N(𝒪_w^×)=𝒪ᵥ^× IsDedekindDomain.HeightOneSpectrum.Extension.exists_norm_eq_of_inertia_eq_bot 3 below · cited by 7 · depth 17
• Inertia of the w-adic valuation ring equals ideal inertia IsDedekindDomain.HeightOneSpectrum.map_subtype_inertiaSubgroup_valuationSubring_eq_inertia 1 below · cited by 4 · depth 17
• Cardinality of ℤᵥ/nℤᵥ equals ℓ^{v_ℓ(n)} IsDedekindDomain.HeightOneSpectrum.natCard_adicCompletionIntegers_rat_quotient_span_natCast_eq_prime_pow_factorization 2 below · cited by 6 · depth 17
• Local degree one for Kummer generators that are local n-th powers IsDedekindDomain.HeightOneSpectrum.Extension.finrank_adicCompletion_eq_one_of_pow_eq 0 below · cited by 2 · depth 18
• Trivial inertia in multi-radical extensions above v ∤ n IsDedekindDomain.HeightOneSpectrum.Extension.inertia_eq_bot_of_forall_pow_eq 0 below · cited by 1 · depth 18
• Triviality of inertia in radical extensions away from n IsDedekindDomain.HeightOneSpectrum.Extension.inertia_eq_bot_of_pow_eq 0 below · cited by 3 · depth 18
• Fibrewise factorisation of products over finite places IsDedekindDomain.HeightOneSpectrum.finprod_eq_finprod_prod_extension 0 below · cited by 1 · depth 18
• Elements near 1 in Kᵥ are n-th powers IsDedekindDomain.HeightOneSpectrum.exists_forall_exists_pow_eq_of_valued_sub_one_le 1 below · cited by 1 · depth 19
• Completion maps compose in a tower of number fields IsDedekindDomain.HeightOneSpectrum.adicCompletionSemialgHom_comp_of_tower 0 below · cited by 3 · depth 20
• Hensel's lemma with |f(a₀)| < |f'(a₀)|² over Kᵥ IsDedekindDomain.HeightOneSpectrum.exists_isRoot_and_valued_sub_mul_le_of_valued_eval_lt 0 below · cited by 1 · depth 20
• Transitivity of restriction of finite places in a tower IsDedekindDomain.HeightOneSpectrum.under_under_ringOfIntegers 0 below · cited by 5 · depth 20
• Global representatives for square classes of Kᵥ^× IsDedekindDomain.HeightOneSpectrum.exists_algebraMap_eq_mul_sq_adicCompletion 0 below · cited by 1 · depth 23
• A sequence of primes of 𝒪_L outside a finite set, with injective and exhaustive traces to K IsDedekindDomain.HeightOneSpectrum.exists_seq_not_mem_injective_under_forall_exists_under_eq 0 below · cited by 2 · depth 23
• Unique place above a local non-square in a quadratic field IsDedekindDomain.HeightOneSpectrum.exists_unique_extension_and_algEquiv_adjoinRoot_of_not_isSquare 1 below · cited by 1 · depth 23
• Twisted norms in K'ᵥ⊗_{K_v}L_w at unramified places IsDedekindDomain.HeightOneSpectrum.exists_units_prod_tensor_map_iterate_eq_tmul_one_of_finrank_dvd_valuation_norm 10 below · cited by 1 · depth 23
• Completion commutes with base change along a compositum IsDedekindDomain.HeightOneSpectrum.exists_tensor_adicCompletion_algEquiv_of_baseChange 0 below · cited by 1 · depth 24
• A field base change M⊗_F Fᵥ forces a unique place above v IsDedekindDomain.HeightOneSpectrum.exists_unique_extension_algEquiv_adicCompletion_of_isField_tensor 0 below · cited by 2 · depth 24
• Inertia degree divides the valuation of x after base change IsDedekindDomain.HeightOneSpectrum.exists_valued_eq_exp_inertiaDeg_mul_of_valued_norm_eq_of_baseChange 3 below · cited by 1 · depth 24
• Unramified base change: e=1 and f∣[L:K] IsDedekindDomain.HeightOneSpectrum.ramificationIdx_eq_one_and_inertiaDeg_dvd_of_baseChange_of_unramified 0 below · cited by 2 · depth 24
• Residue degree one above an inert place in M=LK' IsDedekindDomain.HeightOneSpectrum.inertiaDeg_eq_one_of_inertiaDeg_eq_two_of_finrank_eq_two_of_baseChange 0 below · cited by 1 · depth 25
• v-adic valuation as ofAdd of minus countᵥ IsDedekindDomain.HeightOneSpectrum.valuation_eq_ofAdd_neg_count_spanSingleton 0 below · cited by 1 · depth 25
• Refining a ball of ℚₚ into q balls: indicator identity IsDedekindDomain.HeightOneSpectrum.exists_finset_card_eq_absNorm_indicator_ball_eq_sum_rat 1 below · cited by 1 · depth 26
• Residue ring at a uniformiser has absNorm many elements IsDedekindDomain.HeightOneSpectrum.natCard_adicCompletionIntegers_quot_span_eq_absNorm 0 below · cited by 4 · depth 27
• A rational prime lies in a unique height-one prime of ℤ IsDedekindDomain.HeightOneSpectrum.eq_of_natCast_prime_mem_asIdeal 0 below · cited by 1 · depth 28
• Open unit subgroup fixing a locally constant compactly supported Φ IsDedekindDomain.HeightOneSpectrum.exists_isOpen_subgroup_forall_apply_mul_eq_of_isLocallyConstant_of_hasCompactSupport 0 below · cited by 4 · depth 32
• Continuous characters of Kᵥ^× are unitary and locally trivial IsDedekindDomain.HeightOneSpectrum.norm_apply_units_eq_one_of_valuation_eq_one_and_exists_isOpen_subgroup_apply_eq_one 0 below · cited by 2 · depth 32
• Unramified non-trivial automorphism moves an integer by a unit IsDedekindDomain.HeightOneSpectrum.Extension.exists_norm_le_one_and_norm_algEquiv_sub_eq_one_of_ramificationIdx_eq_one 6 below · cited by 1 · depth 34
• Index q^{min(s,m)} of a twisted lattice over mathcal O_w IsDedekindDomain.HeightOneSpectrum.Extension.relIndex_adicCompletionIntegers_comap_sub_mulLeft_eq_absNorm_pow_min_of_ramificationIdx_eq_one 3 below · cited by 3 · depth 34
• Index of a twisted lattice at an unramified place IsDedekindDomain.HeightOneSpectrum.Extension.relIndex_adicCompletionIntegers_comap_sub_mulLeft_eq_absNorm_pow_min_of_ramificationIdx_eq_one_of_forall_lt_finrank 3 below · cited by 1 · depth 34
• Shell decomposition of a window with logarithmic germ at 1 IsDedekindDomain.HeightOneSpectrum.exists_isLocallyConstant_add_shell_defect_of_cells_of_norm_sub_le 1 below · cited by 1 · depth 35
• Shells and uniform cell counts in higher unit groups of Kᵥ^× IsDedekindDomain.HeightOneSpectrum.exists_subgroups_shells_finset_card_le_of_units_adicCompletion 0 below · cited by 2 · depth 35
• Index of nested 𝒪ᵥ-lattices equals inverse norm of determinant IsDedekindDomain.HeightOneSpectrum.relIndex_span_range_mul_norm_det_eq_one_of_forall_mem_span 3 below · cited by 4 · depth 36
• The n-th power map is open at 1 on Kᵥ^× IsDedekindDomain.HeightOneSpectrum.image_pow_mem_nhds_one_units_adicCompletion 0 below · cited by 4 · depth 37
• Residue count times normalised absolute value equals one IsDedekindDomain.HeightOneSpectrum.natCard_adicCompletionIntegers_quotient_span_singleton_mul_norm_eq_one 1 below · cited by 2 · depth 37
• Logarithmic mass of thin slabs in Kᵥ-vector spaces IsDedekindDomain.HeightOneSpectrum.exists_forall_integrableOn_and_setIntegral_one_add_abs_log_norm_le_of_surjective 2 below · cited by 1 · depth 40
• Linear Haar-mass bound for thin slabs over Kᵥ IsDedekindDomain.HeightOneSpectrum.exists_forall_measureReal_inter_norm_le_le_of_surjective 2 below · cited by 1 · depth 40

IsDedekindDomain.selmerGroup 1

• Finiteness of the Selmer group K⟨ S,n⟩ IsDedekindDomain.selmerGroup.finite_of_finite_classGroup_of_fg_units 0 below · cited by 2 · depth 11