Monogenic extensions of discrete valuation rings
TheoremAlgebras generated by a root with invertible derivative are formally unramified#✓fully proved
Let \(R\) and \(S\) be commutative rings, let \(S\) be an \(R\)-algebra, and let \(x \in S\) generate \(S\) as an \(R\)-algebra, that is \(R[x] = S\). If some polynomial \(P \in R[X]\) satisfies \(P(x) = 0\) and \(P'(x)\) is a unit of \(S\), then \(S\) is formally unramified over \(R\).
theorem of_isUnit_aeval_derivative_of_adjoin_eq_top
{R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
(x : S) (P : R[X]) (hP : aeval x P = 0)
(hP' : IsUnit (aeval x P.derivative))
(hx : Algebra.adjoin R {x} = ⊤) :
Algebra.FormallyUnramified R STheoremÉtale finite local algebras are generated by one element with separable reduction#✓fully proved
Let \(R\) and \(S\) be local rings and let \(S\) be an \(R\)-algebra whose structure map \(R \to S\) is injective, which is finitely generated and flat as an \(R\)-module and finitely presented as an \(R\)-algebra. Let \(k\) be the residue field of \(R\). Then \(S\) is étale over \(R\) if and only if there is an element \(x \in S\) with \(R[x] = S\) such that the image in \(k[X]\) of the minimal polynomial of \(x\) over \(R\) (a monic polynomial in \(R[X]\) of least degree with root \(x\)) is separable.
theorem etale_iff_exists_adjoin_eq_top_and_separable_map_minpoly
{R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
[IsLocalRing R] [IsLocalRing S] [Module.Finite R S] [FaithfulSMul R S]
[Module.Flat R S] [Algebra.FinitePresentation R S] :
Algebra.Etale R S ↔
∃ x : S, Algebra.adjoin R ({x} : Set S) = ⊤ ∧
((minpoly R x).map (IsLocalRing.residue R)).SeparableUses 1 · Used by 1
TheoremMonogenic generator with a uniformizing residue polynomial#✓fully proved
Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\), \(\mathfrak m_B\) and residue fields \(\kappa_A\), \(\kappa_B\), and let \(B\) be an \(A\)-algebra that is finitely generated as an \(A\)-module and whose structure map is a local homomorphism. If \(\kappa_B / \kappa_A\) is separable, then there are \(\alpha \in B\) and a polynomial \(F \in A[X]\) such that, writing \(\bar\alpha\) for the residue of \(\alpha\) in \(\kappa_B\): \(A[\alpha] = B\); \(\kappa_A[\bar\alpha] = \kappa_B\); \(F\) is monic; the reduction of \(F\) modulo \(\mathfrak m_A\) is the minimal polynomial of \(\bar\alpha\) over \(\kappa_A\); \(F'(\alpha)\) is a unit of \(B\); and \(\mathfrak m_B\) is the principal ideal generated by \(F(\alpha)\).
In general \(F\) is not the minimal polynomial of \(\alpha\) over \(A\): \(F(\alpha)\) is a nonzero uniformizer, whereas the minimal polynomial vanishes at \(\alpha\).
theorem exists_generator_with_residue_minpoly_uniformizer
[Algebra.IsSeparable (ResidueField A) (ResidueField B)] :
∃ (α : B) (F : Polynomial A),
Algebra.adjoin A ({α} : Set B) = ⊤ ∧
Algebra.adjoin (ResidueField A)
({residue B α} : Set (ResidueField B)) = ⊤ ∧
F.Monic ∧
F.map (residue A) =
minpoly (ResidueField A) (residue B α) ∧
IsUnit (Polynomial.aeval α F.derivative) ∧
maximalIdeal B = Ideal.span {Polynomial.aeval α F}Used by 1
TheoremMonogenicity of extensions with separable residue field extension#✓fully proved
Let \(A\) and \(B\) be discrete valuation rings with residue fields \(\kappa_A\), \(\kappa_B\), and let \(B\) be an \(A\)-algebra that is finitely generated as an \(A\)-module and whose structure map is a local homomorphism. If \(\kappa_B / \kappa_A\) is separable, then there is \(\alpha \in B\) with \(A[\alpha] = B\).
No unramifiedness is assumed: in the ramified case a lift of a generator of \(\kappa_B\) over \(\kappa_A\) is perturbed so that the lifted minimal polynomial takes a uniformizer as value.
theorem exists_adjoin_eq_top_of_separable_residueField
[Algebra.IsSeparable (ResidueField A) (ResidueField B)] :
∃ α : B, Algebra.adjoin A ({α} : Set B) = ⊤TheoremLifts of residue generators generate unramified extensions#✓fully proved
Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\), \(\mathfrak m_B\) and residue fields \(\kappa_A\), \(\kappa_B\), and let \(B\) be an \(A\)-algebra that is finitely generated as an \(A\)-module and whose structure map is a local homomorphism. Suppose \(\kappa_B / \kappa_A\) is separable and the ideal \(\mathfrak m_A B\) generated by the image of \(\mathfrak m_A\) equals \(\mathfrak m_B\). If \(\beta \in B\) has residue \(\bar\beta \in \kappa_B\) with \(\kappa_A[\bar\beta] = \kappa_B\), then \(A[\beta] = B\).
theorem adjoin_eq_top_of_lift_of_map_maximalIdeal
[Algebra.IsSeparable (ResidueField A) (ResidueField B)]
(hunram : (maximalIdeal A).map (algebraMap A B) = maximalIdeal B)
{β : B} (hβ : Algebra.adjoin (ResidueField A) ({residue B β} : Set _) = ⊤) :
Algebra.adjoin A ({β} : Set B) = ⊤TheoremÉtale criterion for extensions of discrete valuation rings#✓fully proved
Let \(A\) and \(B\) be discrete valuation rings with residue fields \(\kappa_A\), \(\kappa_B\), and let \(B\) be an \(A\)-algebra that is finitely generated as an \(A\)-module and whose structure map is a local homomorphism. If \(\kappa_B / \kappa_A\) is separable and the rank of \(B\) as an \(A\)-module equals the degree \([\kappa_B : \kappa_A]\), then \(B\) is étale over \(A\).
theorem etale_of_isSeparable_residueField_of_finrank_eq
[Algebra.IsSeparable (ResidueField A) (ResidueField B)]
(hfin : Module.finrank A B = Module.finrank (ResidueField A) (ResidueField B)) :
Algebra.Etale A BTheoremCharacterization of unramified extensions of a complete DVR#✓fully proved
Let \(A\) and \(B\) be discrete valuation rings, with \(A\) complete with respect to its maximal ideal, and let \(B\) be an \(A\)-algebra via a local homomorphism \(A \to B\), such that \(B\) is finitely generated and torsion-free as an \(A\)-module. Let \(k_A\) and \(k_B\) be the residue fields of \(A\) and \(B\). Then the following are equivalent: (a) \(k_B\) is separable over \(k_A\) and the rank of \(B\) as an \(A\)-module equals \([k_B : k_A]\); (b) there is \(\alpha \in B\) with \(B = A[\alpha]\) such that the reduction modulo the maximal ideal of \(A\) of the minimal polynomial of \(\alpha\) over \(A\) is separable over \(k_A\).
theorem unramified_iff_exists_monogenic_separable_reduced_minpoly :
(Algebra.IsSeparable (ResidueField A) (ResidueField B) ∧
Module.finrank A B = Module.finrank (ResidueField A) (ResidueField B)) ↔
∃ α : B, Algebra.adjoin A ({α} : Set B) = ⊤ ∧
((minpoly A α).map (residue A)).SeparableSources
- ATLAS NumberTheoryI, Corollary 10.15.
TheoremAdjoining a root of unity of order coprime to the residue characteristic is unramified#✓fully proved
Let \(A\) and \(B\) be discrete valuation rings, with \(A\) complete with respect to its maximal ideal, and let \(B\) be an \(A\)-algebra via a local homomorphism \(A \to B\), such that \(B\) is finitely generated and torsion-free as an \(A\)-module. Let \(k_A\) and \(k_B\) be the residue fields of \(A\) and \(B\). Let \(n\) be a natural number coprime to the characteristic of \(k_A\), and let \(\zeta \in B\) be a primitive \(n\)-th root of unity with \(B = A[\zeta]\). Then \(k_B\) is separable over \(k_A\) and the rank of \(B\) as an \(A\)-module equals \([k_B : k_A]\).
Coprimality is meant literally, with \(\gcd(n, 0) = n\), so when \(k_A\) has characteristic \(0\) the hypothesis forces \(n = 1\).
theorem unramified_of_primitive_root_of_unity_of_coprime {n : ℕ} {ζ : B}
(hprim : IsPrimitiveRoot ζ n)
(hcoprime : Nat.Coprime n (ringChar (IsLocalRing.ResidueField A)))
(hgen : Algebra.adjoin A ({ζ} : Set B) = ⊤) :
Algebra.IsSeparable (ResidueField A) (ResidueField B) ∧
Module.finrank A B =
Module.finrank (ResidueField A) (ResidueField B)Sources
- ATLAS NumberTheoryI, the helper
cor_10_16_of_adjoinfor Corollary 10.16; the generation \(B = A[\zeta]\) is assumed here rather than proved from the integral-closure setup.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.