15.106 Weakly étale ring maps to 15.122 Determinants of…
Section15.106 Weakly étale ring maps#
Section 15.106 of the Stacks Project, Tag 092A. 24 tags here are carried by 26 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 092B, a definition
Tag 092B in the Stacks Project.
IsAbsolutelyFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AbsolutelyFlat/Basic.lean, line 85.
Stacks 092B. A commutative ring is absolutely flat if every module over it is flat.
abbrev IsAbsolutelyFlat (A : Type u) [CommRing A] : Prop
Tag 092C, a lemma
Tag 092C in the Stacks Project.
flat_of_flat_of_mul_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Flat.lean, line 431.
Stacks Tag 092C. Let
A → Bbe a ring map such that the multiplication mapμ : B ⊗_A B → BmakesBa flat(B ⊗_A B)-module. LetNbe aB-module. IfNis flat as anA-module, thenNis flat as aB-module.
theorem flat_of_flat_of_mul_flat
(A B : Type*) [CommRing A] [CommRing B] [Algebra A B]
(hB : Algebra.MulFlat A B)
(N : Type*) [AddCommGroup N] [Module B N]
[Module A N] [IsScalarTower A B N]
(hN : Module.Flat A N) :
Module.Flat B N
Tag 092D, a definition
Tag 092D in the Stacks Project.
HasWeakDimensionLE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Defs.lean, line 53.
A commutative ring has weak dimension at most
dif every module over it has Tor dimension at mostd.
def HasWeakDimensionLE {A : Type u} [CommRing A]
(derivedTensor :
DerivedCategory (ModuleCat.{u} A) ⥤
DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} A))
(comparison : ∀ N : ModuleCat.{u} A,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N) ⟶
((tensoringRight (ModuleCat.{u} A)).obj N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} A,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ)))
(d : ℕ) : Prop
Tag 092E, a lemma
Tag 092E in the Stacks Project.
hasWeakDimensionLE_of_weaklyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeakDimension/WeaklyEtale.lean, line 456.
Stacks Tag 092E. A weakly étale algebra over a commutative ring of weak dimension at most
dalso has weak dimension at mostd.
theorem hasWeakDimensionLE_of_weaklyEtale
(A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
(derivedTensorA :
DerivedCategory (ModuleCat.{u} A) ⥤
DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} A))
(comparisonA : ∀ N : ModuleCat.{u} A,
DerivedCategory.Q ⋙
derivedTensorA.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N) ⟶
((tensoringRight (ModuleCat.{u} A)).obj N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerivedA : ∀ N : ModuleCat.{u} A,
(derivedTensorA.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N)).IsLeftDerivedFunctor
(comparisonA N)
(HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ)))
(d : ℕ) (hAB : Algebra.WeaklyEtale A B)
(hA : HasWeakDimensionLE derivedTensorA comparisonA isLeftDerivedA d) :
∃ (derivedTensorB :
DerivedCategory (ModuleCat.{v} B) ⥤
DerivedCategory (ModuleCat.{v} B) ⥤ DerivedCategory (ModuleCat.{v} B))
(comparisonB : ∀ N : ModuleCat.{v} B,
DerivedCategory.Q ⋙
derivedTensorB.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{v} B) 0).obj N) ⟶
((tensoringRight (ModuleCat.{v} B)).obj N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerivedB : ∀ N : ModuleCat.{v} B,
(derivedTensorB.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{v} B) 0).obj N)).IsLeftDerivedFunctor
(comparisonB N)
(HomologicalComplex.quasiIso (ModuleCat.{v} B) (ComplexShape.up ℤ))),
HasWeakDimensionLE derivedTensorB comparisonB isLeftDerivedB d
Tag 092F, a lemma
Tag 092F in the Stacks Project.
absolutelyFlat_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AbsolutelyFlat/Basic.lean, line 205.
For a commutative ring
A, the following are equivalent:Ahas weak dimension at most zero;Ais absolutely flat;Ais reduced and every prime ideal is maximal; and the localization ofAat every prime ideal is a field.Weak dimension is
HasWeakDimensionLE, which carries the derived tensor product, its comparison with termwise tensor product, and the universal property certifying that the comparison exhibits the derived tensor product as a total left derived functor. Those data are part of the statement, exactly as in the source and as inweakDimensionLE_one_tfae(Stacks 092S).
theorem absolutelyFlat_tfae (A : Type u) [CommRing A]
(derivedTensor :
DerivedCategory (ModuleCat.{u} A) ⥤
DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} A))
(comparison : ∀ N : ModuleCat.{u} A,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N) ⟶
((tensoringRight (ModuleCat.{u} A)).obj N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} A,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ))) :
[ HasWeakDimensionLE derivedTensor comparison isLeftDerived 0,
(∀ (M : Type u) [AddCommGroup M] [Module A M], Module.Flat A M),
IsReduced A ∧ ∀ p : Ideal A, p.IsPrime → p.IsMaximal,
∀ (p : Ideal A) [p.IsPrime], IsField (Localization.AtPrime p) ].TFAE
Tag 092G, a lemma
Tag 092G in the Stacks Project.
product_of_fields_absolutely_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AbsolutelyFlat/ProductOfFields.lean, line 162.
Stacks Tag 092G. A product of fields is an absolutely flat ring: every module over
∏ i, K iis flat.
theorem product_of_fields_absolutely_flat {I : Type*} (K : I → Type*) [∀ i, Field (K i)]
(M : Type*) [AddCommGroup M] [Module (∀ i, K i) M] : Module.Flat (∀ i, K i) M
Tag 092H, a lemma
Tag 092H in the Stacks Project.
mulFlat_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Basic.lean, line 113. The attribute's comment: “(1)”.
If the multiplication map
μ_{B/A} : B ⊗[A] B → Bis flat, then the multiplication mapμ_{B'/A'} : B' ⊗[A'] B' → B'of the base changeB' = A' ⊗[A] Bis flat.Under the canonical
A'-algebra isomorphisme : (A' ⊗[A] B) ⊗[A'] (A' ⊗[A] B) ≃ₐ[A'] A' ⊗[A] (B ⊗[A] B)one hasμ_{B'/A'} = (id_{A'} ⊗ μ_{B/A}) ∘ e, andid_{A'} ⊗ μ_{B/A}is flat byRingHom.Flat.tensorProductMap.
theorem mulFlat_baseChange (A : Type u₁) (B : Type u₂) (A' : Type u₃)
[CommRing A] [CommRing B] [CommRing A']
[Algebra A B] [Algebra A A']
(h : Algebra.MulFlat A B) :
Algebra.MulFlat A' (A' ⊗[A] B)
weaklyEtale_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Basic.lean, line 123. The attribute's comment: “(2)”.
If
A → Bis weakly étale, thenA' → B'is weakly étale, whereB' = A' ⊗[A] Bis the base change. This is Mathlib's base-change instance forAlgebra.WeaklyEtale.
theorem weaklyEtale_baseChange (A : Type u₁) (B : Type u₂) (A' : Type u₃)
[CommRing A] [CommRing B] [CommRing A']
[Algebra A B] [Algebra A A']
(h : Algebra.WeaklyEtale A B) :
Algebra.WeaklyEtale A' (A' ⊗[A] B)
Tag 092I, a lemma
Tag 092I in the Stacks Project.
absolutelyFlat_and_isReduced_of_flat_lmul', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AbsolutelyFlat/Basic.lean, line 247.
If the multiplication map
B ⊗[A] B → Bis flat, then an absolutely flat base ring makesBabsolutely flat. Under the same hypothesis, ifAis reduced andA → Bis weakly étale, thenBis reduced.
theorem absolutelyFlat_and_isReduced_of_flat_lmul'
(A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
(hμ : (Algebra.TensorProduct.lmul' A (S := B)).Flat) :
((∀ (M : Type u) [AddCommGroup M] [Module A M], Module.Flat A M) →
∀ (N : Type v) [AddCommGroup N] [Module B N], Module.Flat B N) ∧
(IsReduced A → Algebra.WeaklyEtale A B → IsReduced B)
Tag 092J, a lemma
Tag 092J in the Stacks Project.
mulFlat_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Basic.lean, line 138. The attribute's comment: “(1)”.
If the multiplication maps
μ_{B/A}andμ_{C/B}are both flat, then the multiplication mapμ_{C/A}is flat.After reducing to a single universe with
Algebra.MulFlat.ulift_iff, this is the factorisationμ_{C/A} = μ_{C/B} ∘ (C ⊗_A C → C ⊗_B C)together withRingHom.Flat.mapOfCompatibleSMulandRingHom.Flat.comp.
theorem mulFlat_comp (A : Type u₁) (B : Type u₂) (C : Type u₃) [CommRing A] [CommRing B]
[CommRing C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
(hAB : Algebra.MulFlat A B) (hBC : Algebra.MulFlat B C) : Algebra.MulFlat A C
weaklyEtale_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Basic.lean, line 146. The attribute's comment: “(2)”.
If
A → BandB → Care both weakly étale, then the compositeA → Cis weakly étale. This is Mathlib'sAlgebra.WeaklyEtale.trans.
theorem weaklyEtale_comp (A B C : Type*) [CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
(hAB : Algebra.WeaklyEtale A B) (hBC : Algebra.WeaklyEtale B C) :
Algebra.WeaklyEtale A C
Tag 092K, a lemma
Tag 092K in the Stacks Project.
flat_lmul'_and_weaklyEtale_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Descent.lean, line 98.
Let
A → B → Cbe compatible maps of commutative rings and suppose thatCis faithfully flat overB. Then flatness of the multiplication mapC ⊗[A] C → Cdescends to the multiplication mapB ⊗[A] B → B; consequently, ifA → Cis weakly étale, thenA → Bis weakly étale.
theorem flat_lmul'_and_weaklyEtale_of_faithfullyFlat
(A : Type u) (B : Type v) (C : Type w)
[CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
[Module.FaithfullyFlat B C] :
((Algebra.TensorProduct.lmul' A (S := C)).Flat →
(Algebra.TensorProduct.lmul' A (S := B)).Flat) ∧
(Algebra.WeaklyEtale A C → Algebra.WeaklyEtale A B)
Tag 092L, a lemma
Tag 092L in the Stacks Project.
weaklyEtale_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Descent.lean, line 145.
If
A → BandA → Care weakly étale, then a compatible algebra mapB → Cis weakly étale.
theorem weaklyEtale_of_comp (A : Type u) (B : Type v) (C : Type w)
[CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
(hAB : Algebra.WeaklyEtale A B) (hAC : Algebra.WeaklyEtale A C) :
Algebra.WeaklyEtale B C
Tag 092M, a lemma
Tag 092M in the Stacks Project.
formallyUnramified_of_flat_lmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/FormallyUnramified.lean, line 49.
If the multiplication map
B ⊗[A] B → Bis flat, thenBis formally unramified overA.
theorem formallyUnramified_of_flat_lmul (A : Type u) (B : Type v)
[CommRing A] [CommRing B] [Algebra A B]
(h : (Algebra.TensorProduct.lmul' A (S := B)).Flat) :
Algebra.FormallyUnramified A B
Tag 0CKP, a lemma
Tag 0CKP in the Stacks Project.
unramified_of_finiteType_and_etale_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/FormallyUnramified.lean, line 66.
If the multiplication map
B ⊗[A] B → Bis flat, finite type implies unramified and finite presentation together with flatness implies étale. In particular, every weakly étale algebra of finite presentation is étale.
theorem unramified_of_finiteType_and_etale_of_finitePresentation
(A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] :
((Algebra.TensorProduct.lmul' A (S := B)).Flat →
(Algebra.FiniteType A B → Algebra.Unramified A B) ∧
(Algebra.FinitePresentation A B → Module.Flat A B → Algebra.Etale A B)) ∧
(Algebra.WeaklyEtale A B →
Algebra.FinitePresentation A B → Algebra.Etale A B)
Tag 092N, a lemma
Tag 092N in the Stacks Project.
weaklyEtale_of_isLocalization_etale_filteredColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Descent.lean, line 410.
A localization and an étale algebra over a commutative ring are weakly étale, and an arbitrary filtered colimit of weakly étale algebras is weakly étale.
theorem weaklyEtale_of_isLocalization_etale_filteredColimit
(A : Type u) [CommRing A] :
(∀ (B : Type v) [CommRing B] [Algebra A B] (M : Submonoid A)
[IsLocalization M B], Algebra.WeaklyEtale A B) ∧
(∀ (B : Type v) [CommRing B] [Algebra A B] [Algebra.Etale A B],
Algebra.WeaklyEtale A B) ∧
(∀ (J : Type w) [SmallCategory J] [IsFiltered J] [Small.{max u (w + 1)} J]
(F : J ⥤ CommAlgCat.{w} A) (c : Cocone F), IsColimit c →
(∀ j, Algebra.WeaklyEtale A (F.obj j)) → Algebra.WeaklyEtale A c.pt)
Tag 092P, a lemma
Tag 092P in the Stacks Project.
isSeparable_of_flat_lmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Field.lean, line 88.
Let
L/Kbe a field extension. If the multiplication mapL ⊗[K] L → Lis flat, thenL/Kis algebraic and separable.
theorem isSeparable_of_flat_lmul (K : Type u) (L : Type v)
[Field K] [Field L] [Algebra K L]
(h : (Algebra.TensorProduct.lmul' K (S := L)).Flat) :
Algebra.IsSeparable K L
Tag 092Q, a lemma
Tag 092Q in the Stacks Project.
flat_lmul_weaklyEtale_filteredColimitEtale_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Field.lean, line 362.
Let
Bbe an algebra over a fieldK. The following are equivalent: the multiplication mapB ⊗[K] B → Bis flat;Bis weakly étale overK; andBis a filtered colimit of étaleK-algebras. Under these equivalent conditions, every finitely generatedK-subalgebra ofBis étale overK.
theorem flat_lmul_weaklyEtale_filteredColimitEtale_tfae
(K : Type u) (B : Type v) [Field K] [CommRing B] [Algebra K B] :
[ (Algebra.TensorProduct.lmul' K (S := B)).Flat,
Algebra.WeaklyEtale K B,
∃ (J : Type v) (_ : SmallCategory J) (_ : IsFiltered J)
(F : J ⥤ CommAlgCat.{v} K) (c : Cocone F) (_ : IsColimit c),
Nonempty (c.pt ≅ CommAlgCat.of K B) ∧ ∀ j, Algebra.Etale K (F.obj j) ].TFAE ∧
((Algebra.TensorProduct.lmul' K (S := B)).Flat →
∀ A : Subalgebra K B, A.FG → Algebra.Etale K A)
Tag 092R, a lemma
Tag 092R in the Stacks Project.
isSeparable_and_isAlgebraic_residueField_of_weaklyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/ResidueField.lean, line 86.
If
A → Bis weakly étale and a primeqofBlies over a primepofA, then the canonical residue field extensionκ(p) → κ(q)is separable algebraic.
theorem isSeparable_and_isAlgebraic_residueField_of_weaklyEtale
(A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
(h : Algebra.WeaklyEtale A B) (p : Ideal A) [p.IsPrime]
(q : Ideal B) [q.IsPrime] (hpq : p = q.comap (algebraMap A B)) :
letI := (Ideal.ResidueField.map p q (algebraMap A B) hpq).toAlgebra
Algebra.IsSeparable p.ResidueField q.ResidueField ∧
Algebra.IsAlgebraic p.ResidueField q.ResidueField
Tag 092S, a lemma
Tag 092S in the Stacks Project.
weakDimensionLE_one_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeakDimension/DimensionOne.lean, line 377.
Stacks Tag 092S. For a commutative ring, weak dimension at most one, flatness of all ideals, flatness of all finitely generated ideals, flatness of submodules of flat modules, and the valuation-ring property for all localizations at prime ideals are equivalent.
theorem weakDimensionLE_one_tfae
(A : Type u) [CommRing A]
(derivedTensor :
DerivedCategory (ModuleCat.{u} A) ⥤
DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} A))
(comparison : ∀ N : ModuleCat.{u} A,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N) ⟶
((tensoringRight (ModuleCat.{u} A)).obj N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} A,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ))) :
List.TFAE
[ HasWeakDimensionLE derivedTensor comparison isLeftDerived 1,
∀ I : Ideal A, Module.Flat A I,
∀ I : Ideal A, I.FG → Module.Flat A I,
∀ (M : Type u) [AddCommGroup M] [Module A M],
Module.Flat A M → ∀ N : Submodule A M, Module.Flat A N,
∀ (p : Ideal A) [p.IsPrime],
∃ _ : IsDomain (Localization.AtPrime p),
ValuationRing (Localization.AtPrime p) ]
Tag 092T, a lemma
Tag 092T in the Stacks Project.
weakDimensionLE_one_and_isLocalization_pi_fractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/WeakDimension.lean, line 208.
A product of valuation rings has weak dimension at most one, and the product of their fraction fields is the localization at the componentwise non-zero-divisors.
theorem weakDimensionLE_one_and_isLocalization_pi_fractionRing
(J : Type v) (A : J → Type u) (K : J → Type w)
[∀ j, CommRing (A j)] [∀ j, IsDomain (A j)] [∀ j, ValuationRing (A j)]
[∀ j, Field (K j)] [∀ j, Algebra (A j) (K j)] [∀ j, IsFractionRing (A j) (K j)] :
HasWeakDimensionLEOne (∀ j, A j) ∧
IsLocalization
(.pi Set.univ (fun j ↦ nonZeroDivisors (A j)))
(∀ j, K j)
Tag 092U, a lemma
Tag 092U in the Stacks Project.
exists_isPullback_with_weakDimensionLE_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/WeakDimension.lean, line 276.
A normal domain and its fraction field fit into a cartesian square whose lower-left ring has weak dimension at most one and whose lower map is flat, injective, and a ring epimorphism.
theorem exists_isPullback_with_weakDimensionLE_one
(A : Type u) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
(K : Type v) [Field K] [Algebra A K] [IsFractionRing A K] :
∃ (V L : Type (max u v)) (_ : CommRing V) (_ : CommRing L)
(_ : Algebra A V) (_ : Algebra K L) (_ : Algebra V L)
(_ : Module.Flat V L) (_ : Algebra.IsEpi V L),
HasWeakDimensionLEOne V ∧
Function.Injective (algebraMap V L) ∧
IsPullback
(CommRingCat.ofHom (algebraMap A K).ulift)
(CommRingCat.ofHom
((algebraMap A V).comp ULift.ringEquiv.toRingHom))
(CommRingCat.ofHom
((algebraMap K L).comp ULift.ringEquiv.toRingHom))
(CommRingCat.ofHom (algebraMap V L))
Tag 092V, a lemma
Tag 092V in the Stacks Project.
isIntegrallyClosedIn_of_isEpi_of_flat_of_weakDimensionLE_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/WeakDimension.lean, line 242.
A flat injective epimorphism of commutative rings whose source has weak dimension at most one makes the source integrally closed in the target.
theorem isIntegrallyClosedIn_of_isEpi_of_flat_of_weakDimensionLE_one
{A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
[Module.Flat A B] [Algebra.IsEpi A B]
(hA : HasWeakDimensionLEOne A)
(hinjective : Function.Injective (algebraMap A B)) :
IsIntegrallyClosedIn A B
Tag 092W, a lemma
Tag 092W in the Stacks Project.
isIntegrallyClosedIn_tensorProduct_fractionField_of_weaklyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/WeakDimension.lean, line 740.
A weakly étale algebra over a normal domain is integrally closed in its scalar extension to any fraction field of the domain.
theorem isIntegrallyClosedIn_tensorProduct_fractionField_of_weaklyEtale
(A : Type u) (B : Type v) (K : Type w)
[CommRing A] [CommRing B] [Field K] [Algebra A B] [Algebra A K]
[IsDomain A] [IsIntegrallyClosed A] [IsFractionRing A K]
(hAB : Algebra.WeaklyEtale A B) :
IsIntegrallyClosedIn B (B ⊗[A] K)
Tag 092X, a lemma
Tag 092X in the Stacks Project.
RingHom.exists_henselianLocalRing_of_isIntegral_of_isDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/IntegralDomain.lean, line 262.
An integral homomorphism from a henselian local ring to a domain makes the target a henselian local ring and is a local homomorphism. If the source residue field is separably closed, then the target residue field is separably closed and its extension along the induced residue-field homomorphism is purely inseparable.
theorem RingHom.exists_henselianLocalRing_of_isIntegral_of_isDomain
{A : Type u} {B : Type v} [CommRing A] [CommRing B]
[HenselianLocalRing A] [IsDomain B] (f : A →+* B) (hf : f.IsIntegral) :
∃ (hB : HenselianLocalRing B) (hlocal : IsLocalHom f),
letI : IsLocalRing B := hB.toIsLocalRing
letI : IsLocalHom f := hlocal
IsSepClosed (ResidueField A) →
IsSepClosed (ResidueField B) ∧ (ResidueField.map f).IsPurelyInseparable
Tag 092Z, a theorem
Tag 092Z in the Stacks Project.
bijective_algebraMap_of_weaklyEtale_of_isLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/StrictlyHenselian.lean, line 326.
A local weakly étale algebra over a strictly henselian local ring has bijective structure homomorphism.
theorem bijective_algebraMap_of_weaklyEtale_of_isLocalHom
(A : Type u) (B : Type v) [CommRing A] [HenselianLocalRing A]
[IsSepClosed (ResidueField A)] [CommRing B] [IsLocalRing B] [Algebra A B]
[IsLocalHom (algebraMap A B)] (hAB : Algebra.WeaklyEtale A B) :
Function.Bijective (algebraMap A B)
Sources
Section15.107 Weakly étale algebras over fields#
Section 15.107 of the Stacks Project, Tag 0CKQ. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0CKR, a lemma
Tag 0CKR in the Stacks Project.
structure_of_weaklyEtale_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/Field.lean, line 573. References: EGA IV (18.3.3), “partial”; SGA 1 IX (1.8), “decomposition direction”; SGA 4½ Arcata (2.1.2), “partial”; SGA 4½ Arcata (2.4.2), “more general”.
A weakly étale algebra
Bover a fieldKis reduced and integral. Every finitely generatedK-subalgebra is a finite product of finite separable extensions ofK. Moreover,Bis a field or the zero ring exactly when it has no nontrivial idempotents; if it is a field, then it is a separable algebraic extension. Subalgebras and quotient algebras ofBare weakly étale overK, as is the tensor product ofBwith any weakly étaleK-algebra.
theorem structure_of_weaklyEtale_over_field
(K : Type u) (B : Type v) [Field K] [CommRing B] [Algebra K B]
(hB : Algebra.WeaklyEtale K B) :
IsReduced B ∧
Algebra.IsIntegral K B ∧
(∀ A : Subalgebra K B, A.FG →
∃ (ι : Type v) (_ : Finite ι) (L : ι → Type v) (_ : ∀ i, Field (L i))
(_ : ∀ i, Algebra K (L i)) (_ : A ≃ₐ[K] ∀ i, L i),
∀ i, Module.Finite K (L i) ∧ Algebra.IsSeparable K (L i)) ∧
(((Subsingleton B ∨ IsField B) ↔
∀ e : B, IsIdempotentElem e → e = 0 ∨ e = 1) ∧
(IsField B → Algebra.IsSeparable K B ∧ Algebra.IsAlgebraic K B)) ∧
((∀ S : Subalgebra K B, Algebra.WeaklyEtale K S) ∧
(∀ (Q : Type w) [CommRing Q] [Algebra K Q],
(∃ f : B →ₐ[K] Q, Function.Surjective f) → Algebra.WeaklyEtale K Q)) ∧
(∀ (B' : Type w) [CommRing B'] [Algebra K B'],
Algebra.WeaklyEtale K B' → Algebra.WeaklyEtale K (B ⊗[K] B'))
Tag 0CKS, a lemma
Tag 0CKS in the Stacks Project.
exists_greatest_weaklyEtale_subalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/MaximalSubalgebra.lean, line 136.
An algebra over a field has a greatest weakly étale subalgebra.
theorem exists_greatest_weaklyEtale_subalgebra
(K : Type u) (A : Type v) [Field K] [CommRing A] [Algebra K A] :
∃ Bmax : Subalgebra K A,
Algebra.WeaklyEtale K Bmax ∧
∀ B : Subalgebra K A, Algebra.WeaklyEtale K B → B ≤ Bmax
Tag 0CKT, a lemma
Tag 0CKT in the Stacks Project.
exists_maximalWeaklyEtaleSubalgebraFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/MaximalSubalgebra.lean, line 722.
The maximal weakly étale subalgebra over a field is functorial and commutes with filtered colimits, reduction, and finite products. It pulls back along injective algebra maps, and over an algebra without nontrivial idempotents it is either the zero ring or a separable algebraic field extension.
theorem exists_maximalWeaklyEtaleSubalgebraFunctor
(K : Type u) [Field K] :
∃ (Bmax : CommAlgCat.{v} K ⥤ CommAlgCat.{v} K)
(ι : Bmax ⟶ 𝟭 (CommAlgCat.{v} K)),
(∀ A, Function.Injective (ι.app A)) ∧
(∀ A, Algebra.WeaklyEtale K (Bmax.obj A)) ∧
(∀ (A : CommAlgCat.{v} K) (S : Subalgebra K A),
Algebra.WeaklyEtale K S →
∃ f : CommAlgCat.of K S ⟶ Bmax.obj A,
f ≫ ι.app A = CommAlgCat.ofHom S.val) ∧
(∀ (A' A : CommAlgCat.{v} K) (f : A' ⟶ A), Function.Injective f →
∀ x : A',
(∃ b : Bmax.obj A', ι.app A' b = x) ↔
∃ b : Bmax.obj A, ι.app A b = f x) ∧
PreservesFilteredColimits Bmax ∧
(∀ A : CommAlgCat.{v} K,
IsIso (Bmax.map (CommAlgCat.ofHom (Ideal.Quotient.mkₐ K (nilradical A))))) ∧
(∀ (J : Type v) [Finite J], PreservesLimitsOfShape (Discrete J) Bmax) ∧
(∀ A : CommAlgCat.{v} K,
(∀ e : A, IsIdempotentElem e → e = 0 ∨ e = 1) →
Subsingleton A ∨
(IsField (Bmax.obj A) ∧ Algebra.IsSeparable K (Bmax.obj A) ∧
Algebra.IsAlgebraic K (Bmax.obj A)))
Tag 0CKU, a lemma
Tag 0CKU in the Stacks Project.
maximalWeaklyEtaleSubalgebra_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/WeaklyEtale/MaximalSubalgebra.lean, line 1086.
Extending the base field carries the maximal weakly étale subalgebra to the maximal weakly étale subalgebra of the scalar extension.
theorem maximalWeaklyEtaleSubalgebra_baseChange
(K : Type u) (L : Type v) (A : Type w)
[Field K] [Field L] [CommRing A] [Algebra K L] [Algebra K A]
(B : Subalgebra K A) (hB : Algebra.WeaklyEtale K B)
(hBmax : ∀ C : Subalgebra K A, Algebra.WeaklyEtale K C → C ≤ B) :
let f : L ⊗[K] B →ₐ[K] L ⊗[K] A :=
Algebra.TensorProduct.map (AlgHom.id K L) B.val
Function.Injective f ∧
Algebra.WeaklyEtale L (L ⊗[K] B) ∧
∀ C : Subalgebra L (L ⊗[K] A), Algebra.WeaklyEtale L C →
∀ x : C, ∃ y : L ⊗[K] B, f y = x
Sources
Section15.108 Local irreducibility#
Section 15.108 of the Stacks Project, Tag 06DT. 8 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BPZ, a definition
Tag 0BPZ in the Stacks Project.
IsUnibranch, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Defs.lean, line 62. The attribute's comment: “(1)”. References: EGA 0 (23.2.1), “def. of unibranch”; EGA III (4.3.6), “unibranch local ring”.
A local ring is unibranch if its reduction is a domain and the integral closure of its reduction in its field of fractions is local.
def IsUnibranch (A : Type u) [CommRing A] [IsLocalRing A] : Prop
IsGeometricallyUnibranch, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Defs.lean, line 70. The attribute's comment: “(2)”. References: EGA 0 (23.2.1), “def. of geom. unibranch”.
A local ring is geometrically unibranch if it is unibranch and the residue field of the normalization of its reduction is purely inseparable over its residue field.
noncomputable def IsGeometricallyUnibranch
(A : Type u) [CommRing A] [IsLocalRing A] : Prop
Tag 0C24, a lemma
Tag 0C24 in the Stacks Project.
bijective_maximalIdeals_and_minimalPrimes_of_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Henselization/BranchCorrespondence.lean, line 598.
Let
A'be the integral closure of a local ringAin the total ring of fractions of its reduction, and letAʰbe a henselization ofA. Contraction fromA' ⊗[A] Aʰis bijective on maximal ideals towardA'and on minimal primes towardAʰ. Each minimal prime of the tensor product lies in a unique maximal ideal, and each maximal ideal contains a unique minimal prime.
theorem bijective_maximalIdeals_and_minimalPrimes_of_henselization
(A : Type u) (Ah : Type v) [CommRing A] [IsLocalRing A] [CommRing Ah] [IsLocalRing Ah]
[Algebra A Ah]
[IsLocalRing.IsHenselization A (IsLocalRing.ResidueField A) Ah]
(hmin : (minimalPrimes A).Finite) :
let A' := integralClosure A (FractionRing (A ⧸ nilradical A))
let T := TensorProduct A A' Ah
Set.BijOn
(Ideal.comap (Algebra.TensorProduct.includeLeftRingHom : A' →+* T))
{I : Ideal T | I.IsMaximal} {I : Ideal A' | I.IsMaximal} ∧
Set.BijOn
(Ideal.comap
(Algebra.TensorProduct.includeRight : Ah →ₐ[A] T).toRingHom)
(minimalPrimes T) (minimalPrimes Ah) ∧
(∀ q ∈ minimalPrimes T, ∃! m : Ideal T, m.IsMaximal ∧ q ≤ m) ∧
(∀ m : Ideal T, m.IsMaximal → ∃! q : Ideal T, q ∈ minimalPrimes T ∧ q ≤ m)
Tag 0BQ0, a lemma
Tag 0BQ0 in the Stacks Project.
isUnibranch_iff_henselization_has_unique_minimalPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Henselization/Unibranch.lean, line 132. References: EGA IV (18.6.12), “a) ⇔ c), irreducible”.
A local ring is unibranch if and only if a henselization of it has a unique minimal prime.
theorem isUnibranch_iff_henselization_has_unique_minimalPrime
(A Ah : Type u) [CommRing A] [IsLocalRing A] [CommRing Ah] [IsLocalRing Ah]
[Algebra A Ah]
[IsLocalRing.IsHenselization A (IsLocalRing.ResidueField A) Ah] :
IsUnibranch A ↔ ∃! p : Ideal Ah, p ∈ minimalPrimes Ah
Tag 0C25, a lemma
Tag 0C25 in the Stacks Project.
geometric_branches_of_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Henselization/BranchCorrespondence.lean, line 538.
Let
A'be the integral closure of a local ringAin the total ring of fractions of its reduction, and letAˢʰbe a strict henselization with separably closed residue fieldksepinside an algebraic closurekbar. The residue extension at every maximal ideal ofA'is algebraic, and its embeddings intokbarcanonically parametrize the fibre inSpec (A' ⊗[A] Aˢʰ). Contraction toAˢʰis bijective on minimal primes, and containment gives mutually unique correspondences between minimal and maximal primes of the tensor product.
theorem geometric_branches_of_strictHenselization
(A : Type u) (Ash : Type u') (ksep : Type v) (kbar : Type w)
[CommRing A] [IsLocalRing A] [CommRing Ash] [IsLocalRing Ash] [Algebra A Ash]
[Field ksep] [Algebra (IsLocalRing.ResidueField A) ksep]
[IsSepClosure (IsLocalRing.ResidueField A) ksep]
[IsLocalRing.IsHenselization A ksep Ash]
[Field kbar] [Algebra (IsLocalRing.ResidueField A) kbar]
[IsAlgClosure (IsLocalRing.ResidueField A) kbar]
[Algebra ksep kbar] [IsScalarTower (IsLocalRing.ResidueField A) ksep kbar]
(e : ksep ≃+* IsLocalRing.ResidueField Ash)
(he : ∀ x : A,
e (algebraMap (IsLocalRing.ResidueField A) ksep (IsLocalRing.residue A x)) =
IsLocalRing.residue Ash (algebraMap A Ash x))
(hmin : (minimalPrimes A).Finite) :
let A' := integralClosure A (FractionRing (A ⧸ nilradical A))
let T := TensorProduct A A' Ash
(∀ m' : MaximalSpectrum A',
∃ h : IsLocalRing.maximalIdeal A = m'.asIdeal.comap (algebraMap A A'),
let f := Ideal.quotientMap m'.asIdeal (algebraMap A A') (le_of_eq h)
f.IsIntegral ∧
∃ E : ({σ : (A' ⧸ m'.asIdeal) →+* kbar //
σ.comp f = algebraMap (IsLocalRing.ResidueField A) kbar} ≃
{q : PrimeSpectrum T //
PrimeSpectrum.comap
(Algebra.TensorProduct.includeLeftRingHom : A' →+* T) q =
m'.toPrimeSpectrum}),
∀ σ, ∃ φ : T →+* kbar,
(∀ (a : A') (b : Ash),
φ (a ⊗ₜ[A] b) =
σ.1 (Ideal.Quotient.mk m'.asIdeal a) *
algebraMap ksep kbar (e.symm (IsLocalRing.residue Ash b))) ∧
(E σ).1.asIdeal = RingHom.ker φ ∧
∀ ψ : T →+* kbar,
(∀ (a : A') (b : Ash),
ψ (a ⊗ₜ[A] b) =
σ.1 (Ideal.Quotient.mk m'.asIdeal a) *
algebraMap ksep kbar (e.symm (IsLocalRing.residue Ash b))) →
ψ = φ) ∧
Set.BijOn
(Ideal.comap
(Algebra.TensorProduct.includeRight : Ash →ₐ[A] T).toRingHom)
(minimalPrimes T) (minimalPrimes Ash) ∧
(∀ q ∈ minimalPrimes T, ∃! m : Ideal T, m.IsMaximal ∧ q ≤ m) ∧
(∀ m : Ideal T, m.IsMaximal → ∃! q : Ideal T, q ∈ minimalPrimes T ∧ q ≤ m)
Tag 06DM, a lemma
Tag 06DM in the Stacks Project.
isGeometricallyUnibranch_iff_strictHenselization_has_unique_minimalPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Henselization/Unibranch.lean, line 425. References: EGA IV (18.8.15), “a) ⇔ c), irreducible”.
A local ring is geometrically unibranch if and only if a strict henselization of it has a unique minimal prime.
theorem isGeometricallyUnibranch_iff_strictHenselization_has_unique_minimalPrime
(A Ash : Type u) [CommRing A] [IsLocalRing A] [CommRing Ash] [IsLocalRing Ash]
[Algebra A Ash]
(ksep : Type v) [Field ksep] [Algebra (IsLocalRing.ResidueField A) ksep]
[IsSepClosure (IsLocalRing.ResidueField A) ksep]
[IsLocalRing.IsHenselization A ksep Ash] :
IsGeometricallyUnibranch A ↔
∃! p : Ideal Ash, p ∈ minimalPrimes Ash
Tag 0C26, a definition
Tag 0C26 in the Stacks Project.
numberOfBranches, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Defs.lean, line 96. The attribute's comment: “number of branches”.
The number of branches of a local ring is the extended-natural cardinality of the set of minimal primes of a henselization.
noncomputable def numberOfBranches (A Ah : Type u) [CommRing A] [IsLocalRing A]
[CommRing Ah]
[IsLocalRing Ah] [Algebra A Ah]
[IsLocalRing.IsHenselization A (IsLocalRing.ResidueField A) Ah] : ℕ∞
numberOfGeometricBranches, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Defs.lean, line 105. The attribute's comment: “number of geometric branches”.
The number of geometric branches of a local ring is the extended-natural cardinality of the set of minimal primes of a strict henselization.
noncomputable def numberOfGeometricBranches (A : Type u) (ksep : Type v) (Ash : Type u)
[CommRing A] [IsLocalRing A] [Field ksep] [Algebra (IsLocalRing.ResidueField A) ksep]
[IsSepClosure (IsLocalRing.ResidueField A) ksep] [CommRing Ash] [IsLocalRing Ash]
[Algebra A Ash] [IsLocalRing.IsHenselization A ksep Ash] : ℕ∞
Tag 0C37, a lemma
Tag 0C37 in the Stacks Project.
numberOfBranches_characterizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Henselization/BranchNumbers.lean, line 204.
The numbers of branches and geometric branches of a local ring are infinite if the ring has infinitely many minimal primes, and they equal one exactly for unibranch and geometrically unibranch rings, respectively. If the ring has finitely many minimal primes, its branches are the maximal ideals of the normalization of its reduction, with geometric branches weighted by the separable degrees of the corresponding residue-field extensions.
theorem numberOfBranches_characterizations
(A Ah Ash : Type u) (ksep : Type v)
[CommRing A] [IsLocalRing A]
[CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsLocalRing.IsHenselization A (IsLocalRing.ResidueField A) Ah]
[Field ksep] [Algebra (IsLocalRing.ResidueField A) ksep]
[IsSepClosure (IsLocalRing.ResidueField A) ksep]
[CommRing Ash] [IsLocalRing Ash] [Algebra A Ash]
[IsLocalRing.IsHenselization A ksep Ash] :
((minimalPrimes A).Infinite →
numberOfBranches A Ah = ⊤ ∧
numberOfGeometricBranches A ksep Ash = ⊤) ∧
(numberOfBranches A Ah = 1 ↔ IsUnibranch A) ∧
(numberOfGeometricBranches A ksep Ash = 1 ↔
IsGeometricallyUnibranch A) ∧
((minimalPrimes A).Finite →
let A' := integralClosure A (FractionRing (A ⧸ nilradical A))
numberOfBranches A Ah =
Set.encard {m' : Ideal A' | m'.IsMaximal} ∧
∃ hcontract : ∀ m' : MaximalSpectrum A',
IsLocalRing.maximalIdeal A = m'.asIdeal.comap (algebraMap A A'),
numberOfGeometricBranches A ksep Ash =
ENat.card (Σ m' : MaximalSpectrum A',
letI : Field (A' ⧸ m'.asIdeal) := Ideal.Quotient.field m'.asIdeal
let f := Ideal.quotientMap m'.asIdeal (algebraMap A A')
(le_of_eq (hcontract m'))
letI : Algebra (IsLocalRing.ResidueField A) (A' ⧸ m'.asIdeal) := f.toAlgebra
(Field.sepDegree (IsLocalRing.ResidueField A)
(A' ⧸ m'.asIdeal)).ord.ToType))
Tag 0DQ1, a lemma
Tag 0DQ1 in the Stacks Project.
numberOfBranches_eq_of_isLocalization_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Miscellaneous/SmoothInvariance.lean, line 402.
A local homomorphism of local rings which is a localization of a smooth ring map preserves the number of geometric branches. If its residue-field extension is purely inseparable, it also preserves the number of branches.
The source's two rings carry independent universes, together with their henselizations and strict henselizations:
A,Aʰ,Aˢʰin one andB,Bʰ,Bˢʰin the other, and the two separable closures in two more. The universe work is done byStacksDraft.henselization_tensorProduct_at_unique_primeandStacksDraft.strictHenselization_tensorProduct_at_induced_prime, the source-strength forms of tags 08HU and 08HV, and by the ind-étale layer they are built on, which lets the branch-counting lemmas above be stated with the base and its henselization in independent universes.
theorem numberOfBranches_eq_of_isLocalization_smooth
(A Ah Ash : Type uA) (B Bh Bsh : Type uB) (kAsep : Type vA) (kBsep : Type vB)
[CommRing A] [IsLocalRing A] [CommRing B] [IsLocalRing B] [Algebra A B]
[IsLocalHom (algebraMap A B)]
(hsm : ∃ (C : Type uC) (_ : CommRing C) (_ : Algebra A C) (_ : Algebra C B)
(_ : IsScalarTower A C B) (S : Submonoid C),
Algebra.Smooth A C ∧ IsLocalization S B)
[CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsLocalRing.IsHenselization A (IsLocalRing.ResidueField A) Ah]
[CommRing Bh] [IsLocalRing Bh] [Algebra B Bh]
[IsLocalRing.IsHenselization B (IsLocalRing.ResidueField B) Bh]
[Field kAsep] [Algebra (IsLocalRing.ResidueField A) kAsep]
[IsSepClosure (IsLocalRing.ResidueField A) kAsep]
[CommRing Ash] [IsLocalRing Ash] [Algebra A Ash]
[IsLocalRing.IsHenselization A kAsep Ash]
[Field kBsep] [Algebra (IsLocalRing.ResidueField B) kBsep]
[IsSepClosure (IsLocalRing.ResidueField B) kBsep]
[CommRing Bsh] [IsLocalRing Bsh] [Algebra B Bsh]
[IsLocalRing.IsHenselization B kBsep Bsh] :
numberOfGeometricBranches A kAsep Ash = numberOfGeometricBranches B kBsep Bsh ∧
((IsLocalRing.ResidueField.map (algebraMap A B)).IsPurelyInseparable →
numberOfBranches A Ah = numberOfBranches B Bh)
Sources
Section15.109 Miscellaneous on branches#
Section 15.109 of the Stacks Project, Tag 0GS4. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GS5, a lemma
Tag 0GS5 in the Stacks Project.
comap_ne_bot_of_localization_or_discrete_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/UnibranchEtale.lean, line 153.
Let
A → Bbe a map of domains. Suppose that it is a localization of an étale map; or that it is flat and a localization of an unramified, quasi-finite, or integral map; or that it is flat and its fibers have no nontrivial specializations; or that it maps the generic point to the generic point and its fibers have no nontrivial specializations; or that exactly one point ofSpec(B)maps to the generic point ofSpec(A). Then every nonzero ideal ofBhas nonzero contraction toA.
theorem comap_ne_bot_of_localization_or_discrete_fibers
(A : Type u) (B : Type v) [CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
[Algebra A B]
(h :
(∃ (T : Type (max u v)) (_ : CommRing T) (_ : Algebra A T) (_ : Algebra T B)
(_ : IsScalarTower A T B), Algebra.Etale A T ∧
∃ M : Submonoid T, IsLocalization M B) ∨
(Module.Flat A B ∧
∃ (T : Type (max u v)) (_ : CommRing T) (_ : Algebra A T) (_ : Algebra T B)
(_ : IsScalarTower A T B), Algebra.Unramified A T ∧
∃ M : Submonoid T, IsLocalization M B) ∨
(Module.Flat A B ∧
∃ (T : Type (max u v)) (_ : CommRing T) (_ : Algebra A T) (_ : Algebra T B)
(_ : IsScalarTower A T B), Algebra.QuasiFinite A T ∧
∃ M : Submonoid T, IsLocalization M B) ∨
(Module.Flat A B ∧
∃ (T : Type (max u v)) (_ : CommRing T) (_ : Algebra A T) (_ : Algebra T B)
(_ : IsScalarTower A T B), Algebra.IsIntegral A T ∧
∃ M : Submonoid T, IsLocalization M B) ∨
(Module.Flat A B ∧ NoNontrivialSpecializationsInFibers A B) ∨
((⊥ : Ideal B).comap (algebraMap A B) = ⊥ ∧
NoNontrivialSpecializationsInFibers A B) ∨
(∃! q : Ideal B, q.IsPrime ∧ q.comap (algebraMap A B) = ⊥)) :
∀ J : Ideal B, J ≠ ⊥ → J.comap (algebraMap A B) ≠ ⊥
Tag 0GSC, a lemma
Tag 0GSC in the Stacks Project.
exists_etale_away_of_isGeometricallyUnibranch_of_isUnramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Miscellaneous/UnramifiedNeighborhood.lean, line 251. References: EGA IV (18.10.1), “(i)+(ii) ⇒ étale”.
Let
A → Bbe a ring map from a domain, and letqbe a prime ofBlying over a primepofA. IfAₚis geometrically unibranch, the map is unramified atq, and the canonical mapAₚ → B_qis injective, then some principal localizationB_g, withg ∉ q, is étale overA.
theorem exists_etale_away_of_isGeometricallyUnibranch_of_isUnramifiedAt
{A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A]
(p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p]
(hgeom : IsGeometricallyUnibranch (Localization.AtPrime p))
(hunram : ∃ f : B, f ∉ q ∧ Algebra.Unramified A (Localization.Away f))
(hinj : letI := Localization.AtPrime.algebraOfLiesOver p q
Function.Injective
(algebraMap (Localization.AtPrime p) (Localization.AtPrime q))) :
∃ g : B, g ∉ q ∧ Algebra.Etale A (Localization.Away g)
Tag 0GS6, a lemma
Tag 0GS6 in the Stacks Project.
exists_etale_isLocalization_of_isGeometricallyUnibranch, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/UnibranchEtale.lean, line 336. References: EGA IV (18.10.1), “(i)+(ii) ⇒ étale”; SGA 1 I (9.5), “(ii)”.
Stacks 0GS6. An injective, essentially finite type local map from a geometrically unibranch local domain is a localization of an étale map when its target maximal ideal is extended from the source and its residue-field extension is separable.
theorem exists_etale_isLocalization_of_isGeometricallyUnibranch
(A : Type u) (B : Type v)
[CommRing A] [IsLocalRing A] [IsDomain A]
[CommRing B] [IsLocalRing B] [Algebra A B]
[IsLocalHom (algebraMap A B)] [Algebra.EssFiniteType A B]
(hinjective : Function.Injective (algebraMap A B))
(hunibranch : IsGeometricallyUnibranch A)
(hmaximal : Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A) =
IsLocalRing.maximalIdeal B)
(hseparable : Algebra.IsSeparable (IsLocalRing.ResidueField A)
(IsLocalRing.ResidueField B)) :
∃ (C : Type (max u v)) (_ : CommRing C) (_ : Algebra A C)
(_ : Algebra C B) (_ : IsScalarTower A C B) (M : Submonoid C),
Algebra.Etale A C ∧ IsLocalization M B
Tag 06DU, a lemma
Tag 06DU in the Stacks Project.
minimalPrimes_strictHenselization_tensorProduct_bijOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Miscellaneous/StrictHenselizationTensorProduct.lean, line 905.
The minimal primes of the strict henselization of the localization of
A ⊗[k] Bat the maximal ideal induced by the residue maps correspond bijectively, by contraction, to pairs of minimal primes ofAandB.
theorem minimalPrimes_strictHenselization_tensorProduct_bijOn
(k A B : Type u) [Field k] [IsAlgClosed k]
[CommRing A] [Algebra k A] [HenselianLocalRing A] [IsSepClosed (ResidueField A)]
[CommRing B] [Algebra k B] [HenselianLocalRing B] [IsSepClosed (ResidueField B)]
(resA : A →ₐ[k] k) (resB : B →ₐ[k] k)
(hresA : RingHom.ker resA.toRingHom = maximalIdeal A)
(hresB : RingHom.ker resB.toRingHom = maximalIdeal B)
(R C : Type u) [CommRing R] [IsLocalRing R] [CommRing C] [IsLocalRing C]
[Algebra (A ⊗[k] B) R]
[IsLocalization
(Submonoid.comap
(Algebra.TensorProduct.lift resA resB (fun _ _ ↦ Commute.all _ _)).toRingHom
(nonZeroDivisors k)) R]
[Algebra R C]
(ksep : Type v) [Field ksep] [Algebra (ResidueField R) ksep]
[IsSepClosure (ResidueField R) ksep]
[IsLocalRing.IsHenselization R ksep C] :
Set.BijOn
(fun q : Ideal C ↦
(q.comap ((algebraMap R C).comp
((algebraMap (A ⊗[k] B) R).comp
(Algebra.TensorProduct.includeLeft : A →ₐ[k] A ⊗[k] B).toRingHom)),
q.comap ((algebraMap R C).comp
((algebraMap (A ⊗[k] B) R).comp
(Algebra.TensorProduct.includeRight : B →ₐ[k] A ⊗[k] B).toRingHom))))
(minimalPrimes C) ((minimalPrimes A) ×ˢ (minimalPrimes B))
Sources
Section15.110 Branches of the completion#
Section 15.110 of the Stacks Project, Tag 0C27. 8 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0C28, a lemma
Tag 0C28 in the Stacks Project.
numberOfBranches_le_and_numberOfGeometricBranches_le_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Completion/BranchCounts.lean, line 425.
For a Noetherian local ring
Awith henselizationAʰand strict henselizationAˢʰ, there is a mapAʰ → Âalong which contraction is surjective on minimal primes, ⊗[Aʰ] Aˢʰis a strict henselization ofÂ, and completion decreases neither the number of branches nor the number of geometric branches.
theorem numberOfBranches_le_and_numberOfGeometricBranches_le_completion
(A Ah Ash : Type u)
[CommRing A] [IsLocalRing A] [IsNoetherianRing A]
[CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsHenselization A (ResidueField A) Ah]
(κsep : Type v) [Field κsep] [Algebra (ResidueField A) κsep]
[IsSepClosure (ResidueField A) κsep]
[CommRing Ash] [IsLocalRing Ash] [Algebra A Ash] [Algebra Ah Ash]
[IsScalarTower A Ah Ash] [IsHenselization A κsep Ash]
[IsLocalHom (algebraMap Ah Ash)] :
let Ahat := AdicCompletion (maximalIdeal A) A
∃ hAhatLocal : IsLocalRing Ahat,
letI : IsLocalRing Ahat := hAhatLocal
∃ hAhatMapLocal : IsLocalHom (algebraMap A Ahat),
letI : IsLocalHom (algebraMap A Ahat) := hAhatMapLocal
∃ f : Ah →+* Ahat,
(∀ x : A, f (algebraMap A Ah x) = algebraMap A Ahat x) ∧
Set.SurjOn (fun q => Ideal.comap f q) (minimalPrimes Ahat) (minimalPrimes Ah) ∧
letI : Algebra Ah Ahat := f.toAlgebra
∃ hAhatHenselization : IsHenselization Ahat (ResidueField Ahat) Ahat,
letI : IsHenselization Ahat (ResidueField Ahat) Ahat := hAhatHenselization
numberOfBranches A Ah ≤ numberOfBranches Ahat Ahat ∧
∃ algKhat : Algebra (ResidueField Ahat) κsep,
letI : Algebra (ResidueField Ahat) κsep := algKhat
(∀ x : ResidueField A,
algebraMap (ResidueField Ahat) κsep
(ResidueField.map (algebraMap A Ahat) x) =
algebraMap (ResidueField A) κsep x) ∧
∃ hKsep : IsSepClosure (ResidueField Ahat) κsep,
letI : IsSepClosure (ResidueField Ahat) κsep := hKsep
∃ hTensorLocal : IsLocalRing (Ahat ⊗[Ah] Ash),
letI : IsLocalRing (Ahat ⊗[Ah] Ash) := hTensorLocal
∃ hTensorHenselization : IsHenselization Ahat κsep (Ahat ⊗[Ah] Ash),
letI : IsHenselization Ahat κsep (Ahat ⊗[Ah] Ash) := hTensorHenselization
numberOfGeometricBranches A κsep Ash ≤
numberOfGeometricBranches Ahat κsep (Ahat ⊗[Ah] Ash)
Tag 0C29, a lemma
Tag 0C29 in the Stacks Project.
numberOfBranches_eq_completion_iff_radical_map_minimalPrime_isPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Completion/BranchCounts.lean, line 288.
A Noetherian local ring and its completion have the same number of branches if and only if the radical of the extension of every minimal prime of a henselization to the completion is prime.
theorem numberOfBranches_eq_completion_iff_radical_map_minimalPrime_isPrime
(A Ah : Type u)
[CommRing A] [IsLocalRing A] [IsNoetherianRing A]
[CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsHenselization A (ResidueField A) Ah] :
let Ahat := AdicCompletion (maximalIdeal A) A
∃ hAhatLocal : IsLocalRing Ahat,
letI : IsLocalRing Ahat := hAhatLocal
∃ hAhatMapLocal : IsLocalHom (algebraMap A Ahat),
letI : IsLocalHom (algebraMap A Ahat) := hAhatMapLocal
∃ f : Ah →+* Ahat,
(∀ x : A, f (algebraMap A Ah x) = algebraMap A Ahat x) ∧
∃ hAhatHenselization : IsHenselization Ahat (ResidueField Ahat) Ahat,
letI : IsHenselization Ahat (ResidueField Ahat) Ahat := hAhatHenselization
(numberOfBranches A Ah =
numberOfBranches Ahat Ahat ↔
∀ q ∈ minimalPrimes Ah, (Ideal.map f q).radical.IsPrime)
Tag 0C2A, a lemma
Tag 0C2A in the Stacks Project.
exists_surjective_bijective_away_prod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Idempotent.lean, line 844.
Stacks Tag 0C2A, Lemma 15.110.3. Let
Abe a ring,I ⊆ Aa finitely generated ideal, andA → Ca ring map such that for everyf ∈ Ithe induced mapA_f → C_fis localization at an idempotent. Then there is a surjective ring mapA → C'such that for everyf ∈ Ithe canonical ring mapA_f → (C × C')_fis an isomorphism (here expressed as a bijective ring homomorphism).Note:
C'is constructed as a quotient ofA, so it lives in the universeuofA.
theorem exists_surjective_bijective_away_prod {A : Type u} {C : Type v} [CommRing A] [CommRing C]
[Algebra A C]
(I : Ideal A) (hI : I.FG)
(h : ∀ f ∈ I, IsLocalizationAtIdempotent
(IsLocalization.Away.map (Localization.Away f)
(Localization.Away (algebraMap A C f)) (algebraMap A C) f)) :
∃ (C' : Type u) (_ : CommRing C') (_ : Algebra A C'),
Function.Surjective (algebraMap A C') ∧
∀ f ∈ I, Function.Bijective
(IsLocalization.Away.map (Localization.Away f)
(Localization.Away (algebraMap A (C × C') f)) (algebraMap A (C × C')) f)
Tag 0ALR, a lemma
Tag 0ALR in the Stacks Project.
exists_finiteType_algEquiv_adicCompletion_of_cotangent_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Algebraization.lean, line 521.
Stacks Tag 0ALR. A quotient of the adic completion of a finite-type algebra is itself the adic completion of a finite-type algebra if its conormal module is annihilated by a power of the defining ideal.
theorem exists_finiteType_algEquiv_adicCompletion_of_cotangent_annihilated
(A : Type u) (B : Type v) (C : Type w) [CommRing A] [IsNoetherianRing A]
[CommRing B] [Algebra A B] [Algebra.FiniteType A B]
[CommRing C] [Algebra A C] (I : Ideal A)
(φ : AdicCompletion (I.map (algebraMap A B)) B →ₐ[A] C)
(hφ : Function.Surjective φ) (c : ℕ)
(hJ : I ^ c • (⊤ : Submodule A (RingHom.ker φ.toRingHom).Cotangent) = ⊥) :
∃ (D : Type (max u v w)) (_ : CommRing D) (_ : Algebra A D),
Algebra.FiniteType A D ∧
Nonempty (C ≃ₐ[A] AdicCompletion (I.map (algebraMap A D)) D)
Tag 0C2B, a lemma
Tag 0C2B in the Stacks Project.
exists_minimalPrime_henselization_radical_map_eq_of_quotient_dimension_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Completion/HenselizationToCompletion.lean, line 716.
A minimal prime defining a one-dimensional component of the completion of a Noetherian local ring is the radical of the extension of a minimal prime of its henselization.
theorem exists_minimalPrime_henselization_radical_map_eq_of_quotient_dimension_one
(A : Type u) (Ah : Type v)
[CommRing A] [IsLocalRing A] [IsNoetherianRing A]
[CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsHenselization A (ResidueField A) Ah] :
let Ahat := AdicCompletion (maximalIdeal A) A
∃ f : Ah →+* Ahat,
(∀ x : A, f (algebraMap A Ah x) = algebraMap A Ahat x) ∧
∀ q : Ideal Ahat, q ∈ minimalPrimes Ahat →
ringKrullDim (Ahat ⧸ q) = 1 →
∃ qh : Ideal Ah, qh ∈ minimalPrimes Ah ∧ q = (Ideal.map f qh).radical
Tag 0C2C, a lemma
Tag 0C2C in the Stacks Project.
not_isConnected_puncturedSpectrum_adicCompletion_iff_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Completion/PuncturedSpectrum.lean, line 122.
The punctured spectrum of the completion of a Noetherian local ring is disconnected if and only if the punctured spectrum of its henselization is disconnected.
theorem not_isConnected_puncturedSpectrum_adicCompletion_iff_henselization
(A : Type u) (Ah : Type v)
[CommRing A] [IsLocalRing A] [IsNoetherianRing A]
[CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsHenselization A (ResidueField A) Ah] :
let Ahat := AdicCompletion (maximalIdeal A) A
(¬ _root_.IsConnected {p : PrimeSpectrum Ahat | p.asIdeal ≠ maximalIdeal Ahat}) ↔
¬ _root_.IsConnected {p : PrimeSpectrum Ah | p.asIdeal ≠ maximalIdeal Ah}
Tag 0C2D, a lemma
Tag 0C2D in the Stacks Project.
numberOfBranches_and_numberOfGeometricBranches_eq_adicCompletion_of_dimension_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Completion/BranchCounts.lean, line 680.
Completion preserves the ordinary and the geometric number of branches of a one-dimensional Noetherian local ring.
theorem numberOfBranches_and_numberOfGeometricBranches_eq_adicCompletion_of_dimension_one
(A Ah AhatH Ash AhatSh : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
[CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsHenselization A (ResidueField A) Ah]
[CommRing AhatH] [IsLocalRing AhatH]
[Algebra (AdicCompletion (maximalIdeal A) A) AhatH]
[IsHenselization (AdicCompletion (maximalIdeal A) A)
(ResidueField (AdicCompletion (maximalIdeal A) A)) AhatH]
(ksep : Type v) [Field ksep] [Algebra (ResidueField A) ksep]
[IsSepClosure (ResidueField A) ksep]
[CommRing Ash] [IsLocalRing Ash] [Algebra A Ash] [IsHenselization A ksep Ash]
(khatsep : Type w) [Field khatsep]
[Algebra (ResidueField (AdicCompletion (maximalIdeal A) A)) khatsep]
[IsSepClosure (ResidueField (AdicCompletion (maximalIdeal A) A)) khatsep]
[CommRing AhatSh] [IsLocalRing AhatSh]
[Algebra (AdicCompletion (maximalIdeal A) A) AhatSh]
[IsHenselization (AdicCompletion (maximalIdeal A) A) khatsep AhatSh]
(hdim : ringKrullDim A = 1) :
numberOfBranches A Ah =
numberOfBranches (AdicCompletion (maximalIdeal A) A) AhatH ∧
numberOfGeometricBranches A ksep Ash =
numberOfGeometricBranches
(AdicCompletion (maximalIdeal A) A) khatsep AhatSh
Tag 0C2E, a lemma
Tag 0C2E in the Stacks Project.
isNagataRing_and_numberOfBranches_and_numberOfGeometricBranches_eq_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Branches/Completion/GeometricallyNormalFormalFibres.lean, line 444. References: EGA IV (7.6.1), “A' finite over A”; EGA IV (7.8.3), “(vi) local case”.
A Noetherian local ring whose formal fibres are geometrically normal is Nagata, and its ordinary and geometric branch counts agree with those of its completion.
theorem isNagataRing_and_numberOfBranches_and_numberOfGeometricBranches_eq_adicCompletion
(A Ah AhatH Ash AhatSh : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
[CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsHenselization A (ResidueField A) Ah]
[CommRing AhatH] [IsLocalRing AhatH]
[Algebra (AdicCompletion (maximalIdeal A) A) AhatH]
[IsHenselization (AdicCompletion (maximalIdeal A) A)
(ResidueField (AdicCompletion (maximalIdeal A) A)) AhatH]
(ksep : Type v) [Field ksep] [Algebra (ResidueField A) ksep]
[IsSepClosure (ResidueField A) ksep]
[CommRing Ash] [IsLocalRing Ash] [Algebra A Ash] [IsHenselization A ksep Ash]
(khatsep : Type w) [Field khatsep]
[Algebra (ResidueField (AdicCompletion (maximalIdeal A) A)) khatsep]
[IsSepClosure (ResidueField (AdicCompletion (maximalIdeal A) A)) khatsep]
[CommRing AhatSh] [IsLocalRing AhatSh]
[Algebra (AdicCompletion (maximalIdeal A) A) AhatSh]
[IsHenselization (AdicCompletion (maximalIdeal A) A) khatsep AhatSh]
(hformal : ∀ q : PrimeSpectrum A,
Algebra.IsGeometricallyNormal q.asIdeal.ResidueField
(q.asIdeal.Fiber (AdicCompletion (maximalIdeal A) A))) :
IsNagataRing A ∧
numberOfBranches A Ah =
numberOfBranches (AdicCompletion (maximalIdeal A) A) AhatH ∧
numberOfGeometricBranches A ksep Ash =
numberOfGeometricBranches
(AdicCompletion (maximalIdeal A) A) khatsep AhatSh
Sources
Section15.111 Formally catenary rings#
Section 15.111 of the Stacks Project, Tag 0AW1. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0AW2, a definition
Tag 0AW2 in the Stacks Project.
IsFormallyCatenary, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Formal.lean, line 116. References: EGA IV (7.1.9).
A local ring
Ais formally catenary if, for every minimal primepofA, the spectrum of the quotient of its maximal-ideal-adic completion by the extension ofpis equidimensional.
def IsFormallyCatenary (A : Type*) [CommRing A] [IsLocalRing A] : Prop
Tag 0AW3, a lemma
Tag 0AW3 in the Stacks Project.
not_isUniversallyCatenary_of_not_isFormallyCatenary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Formal.lean, line 1715.
Stacks 0AW3. A Noetherian local ring which is not formally catenary is not universally catenary.
theorem not_isUniversallyCatenary_of_not_isFormallyCatenary
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
(hA : ¬ IsFormallyCatenary A) : ¬ Ring.IsUniversallyCatenary A
Tag 0AW4, a lemma
Tag 0AW4 in the Stacks Project.
flat_local_catenary_equidim_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Equidimensional/FlatLocal.lean, line 557. The attribute's comment: “(1)”. References: EGA IV (7.1.3), “(ii) 'in particular'”.
Stacks 0AW4 (1). For a flat local map
A → Bof Noetherian local rings withBcatenary andSpec(B)equidimensional, the fibreSpec(B / pB)is equidimensional for every primep ⊆ A.
theorem flat_local_catenary_equidim_fibre (A B : Type*) [CommRing A] [CommRing B]
[IsNoetherianRing A] [IsNoetherianRing B] [IsLocalRing A] [IsLocalRing B]
[Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Flat A B]
(hcat : IrreducibleClosedsCodim.IsCatenarySpace (PrimeSpectrum B))
(hequi : SpecEquidimensional B)
(p : Ideal A) [p.IsPrime] :
SpecEquidimensional (B ⧸ p.map (algebraMap A B))
flat_local_catenary_equidim_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Equidimensional/FlatLocal.lean, line 570. The attribute's comment: “(2)”. References: EGA IV (7.1.3), “(i)”; EGA IV (7.8.3), “(x)”; EGA IV (7.8.4), “partial”.
Stacks 0AW4 (2). For a flat local map
A → Bof Noetherian local rings withBcatenary andSpec(B)equidimensional, the baseAis catenary andSpec(A)is equidimensional.
theorem flat_local_catenary_equidim_base (A B : Type*) [CommRing A] [CommRing B]
[IsNoetherianRing A] [IsNoetherianRing B] [IsLocalRing A] [IsLocalRing B]
[Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Flat A B]
(hcat : IrreducibleClosedsCodim.IsCatenarySpace (PrimeSpectrum B))
(hequi : SpecEquidimensional B) :
IrreducibleClosedsCodim.IsCatenarySpace (PrimeSpectrum A) ∧ SpecEquidimensional A
Tag 0AW5, a lemma
Tag 0AW5 in the Stacks Project.
isUniversallyCatenary_of_isFormallyCatenary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Formal.lean, line 652. References: EGA IV (7.1.11), “(i)”.
Stacks 0AW5. A formally catenary Noetherian local ring is universally catenary.
theorem isUniversallyCatenary_of_isFormallyCatenary
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
(hA : IsFormallyCatenary A) : Ring.IsUniversallyCatenary A
Tag 0AW6, a proposition
Tag 0AW6 in the Stacks Project.
isUniversallyCatenary_iff_isFormallyCatenary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Formal.lean, line 1742. References: EGA IV (7.1.11), “(i)”.
Ratliff's theorem (Stacks 0AW6). A Noetherian local ring is universally catenary if and only if it is formally catenary.
theorem isUniversallyCatenary_iff_isFormallyCatenary
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A] :
Ring.IsUniversallyCatenary A ↔ IsFormallyCatenary A
Tag 0C2F, a lemma
Tag 0C2F in the Stacks Project.
StacksDraft.Catenary.isUniversallyCatenary_henselization_and_of_isUnibranch, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Henselization.lean, line 400.
Stacks 0C2F. A Noetherian local ring with geometrically normal formal fibres has a universally catenary henselization, and is itself universally catenary if it is unibranch.
public lemma isUniversallyCatenary_henselization_and_of_isUnibranch
(A : Type u) (Ah : Type v)
[CommRing A] [IsNoetherianRing A] [IsLocalRing A]
[CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsHenselization A (ResidueField A) Ah]
(hformal : ∀ q : PrimeSpectrum A,
Algebra.IsGeometricallyNormal q.asIdeal.ResidueField
(q.asIdeal.Fiber (AdicCompletion (maximalIdeal A) A))) :
Ring.IsUniversallyCatenary Ah ∧ (IsUnibranch A → Ring.IsUniversallyCatenary A)
Sources
Section15.112 Group actions and integral closure#
Section 15.112 of the Stacks Project, Tag 0BRE. 11 tags here are carried by 16 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BRF, a lemma
Tag 0BRF in the Stacks Project.
MulSemiringAction.exists_monic_map_eq_X_sub_C_pow_card, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 1050.
Stacks 0BRF. Let
φ : A → Bbe a surjectiveG-equivariant ring homomorphism for a finite groupG. Everyb ∈ B^Gis matched by a monic polynomialPoverA^Gwhose image under the restrictionA^G → B^Gofφis(X - C b) ^ |G|.The witness is the orbit polynomial
∏_{g ∈ G} (X - C (g • a))of any liftaofb: its coefficients areG-invariant, and each factor maps toX - C b, sinceφ (g • a) = g • b = b.
theorem exists_monic_map_eq_X_sub_C_pow_card
{G : Type*} [Group G] [Finite G]
{A B : Type*} [CommRing A] [CommRing B]
[MulSemiringAction G A] [MulSemiringAction G B]
(φ : A →+*[G] B) (hφ : Function.Surjective φ)
(b : FixedPoints.subring B G) :
∃ P : Polynomial (FixedPoints.subring A G), P.Monic ∧
Polynomial.map
((φ : A →+* B).restrict (FixedPoints.subring A G) (FixedPoints.subring B G)
(by
intro a ha g
change g • φ a = φ a
rw [← map_smul φ, ha g])) P =
(Polynomial.X - Polynomial.C b) ^ Nat.card G
Tag 09EG, a lemma
Tag 09EG in the Stacks Project.
FixedPoints.quotientComparison_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 376.
(Well-definedness of
R^G/I^G ⊆ (R/I)^G.) The canonical comparison mapφis injective, soR^G / I^Gis (isomorphic to) a subring of(R/I)^G.Proof:
φisIdeal.Quotient.liftoftoFixedQuot : R^G → (R/I)^G, so it suffices to showker(toFixedQuot) = I^G = invariantIdeal. Ifa ∈ R^Gmaps to0, thenmk_I (a : R) = 0inR/I, i.e.a ∈ I; anda ∈ R^G, soa ∈ invariantIdeal R G Iby definition (I.comap (R^G).subtype). Conversely the quotient byinvariantIdealalready kills these, so the lifted map is injective.
theorem quotientComparison_injective :
Function.Injective (compMap R G I hcompat)
FixedPoints.compMap_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 461.
(Integrality.) Via the comparison map
φ, the ring(R/I)^Gis an integral extension ofR^G / I^G: every element of(R/I)^Gis a root of a monic polynomial with coefficients in the image ofR^G / I^G.Proof: by
Algebra.IsIntegral.mk, fixb ∈ (R/I)^G. Take the monic witnessPoverR^G/I^GfromcompMap_polyWitness b, withmap φ P = (X - C b)^{|G|}. Then under the algebra structureφ.toAlgebra,aeval b P = (map φ P).eval b = ((X - C b)^\{|G|}).eval b = (b - b)^\{|G|} = 0(usingPolynomial.aeval_def,Polynomial.eval_map,Polynomial.eval_pow,Polynomial.eval_sub,Polynomial.eval_X,Polynomial.eval_C), andPis monic, sobis integral.
theorem compMap_isIntegral :
letI := (compMap R G I hcompat).toAlgebra
Algebra.IsIntegral (FixedPoints.subring R G ⧸ invIdeal R G I)
(FixedPoints.subring (R ⧸ I) G)
FixedPoints.quotientComparison_comap_isHomeomorph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 475.
(Homeomorphism on spectra.) The induced map on prime spectra
Spec(φ) : Spec((R/I)^G) → Spec(R^G/I^G)is a homeomorphism for the Zariski topologies. This isPrimeSpectrum.isHomeomorph_comap(the abstract form of Stacks 09EF) applied to the two facts read off fromquotientComparison_polyWitnessandquotientComparison_injective: everyb ∈ (R/I)^Ghasb ^ |G|in the range ofφ, andker φ = 0is nil.
theorem quotientComparison_comap_isHomeomorph :
IsHomeomorph (PrimeSpectrum.comap (compMap R G I hcompat))
FixedPoints.quotientComparison_residueField_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 504.
(Purely inseparable residue extensions.) For every prime
𝔮 ⊆ (R/I)^Gwith contraction𝔭 = φ⁻¹(𝔮) ⊆ R^G/I^G, the induced extension of residue fieldsκ(𝔭) → κ(𝔮)is purely inseparable. This is the abstract form of Stacks 09EF,isPurelyInseparable_residueField_of_sub_C_pow_witness, applied to the monic witnessquotientComparison_polyWitness.
theorem quotientComparison_residueField_isPurelyInseparable
(q : Ideal (FixedPoints.subring (R ⧸ I) G)) [q.IsPrime] :
letI := (Ideal.ResidueField.map (q.comap (compMap R G I hcompat)) q
(compMap R G I hcompat) rfl).toAlgebra
IsPurelyInseparable (Ideal.ResidueField (q.comap (compMap R G I hcompat)))
(Ideal.ResidueField q)
Tag 0H34, a lemma
Tag 0H34 in the Stacks Project.
Stacks.Invariant.QuotientComparison.charpolyFixed_map_mk_of_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 861.
Stacks 0H34 (tag 0H34 = Lemma 15.112.3). For
x ∈ JR, the characteristic polynomial∏_{σ ∈ G} (T - σ x) = T^n + a₁T^{n-1} + … + aₙhas all its non-leading coefficientsaᵢinJ; equivalently, reducing the coefficients ofcharpolyFixed G xmoduloJgivesX ^ n.Implementation note: the coefficients
aᵢlie inR^G, and what has to be shown is that they lie inJ— the ideal ofR^G— and not merely in the a priori largerJR ∩ R^G. Writingx = Σⱼ fⱼ bⱼwithfⱼ ∈ J ⊆ R^Gandbⱼ ∈ R, invariance offⱼgivesσ x = Σⱼ fⱼ (σ bⱼ), so each elementary symmetric coefficient is a sum of products each carrying a factor∏ fⱼ ∈ J, and symmetrizing over the orbit keeps the remaining cofactor inR^G; henceaᵢ ∈ J · R^G = J.
theorem charpolyFixed_map_mk_of_mem [Fintype G] (J : Ideal (FixedPoints.subring R G))
(x : R) (hx : x ∈ JRideal J) :
Polynomial.map (Ideal.Quotient.mk J) (charpolyFixed G x)
= (Polynomial.X : Polynomial ((FixedPoints.subring R G) ⧸ J)) ^ (Fintype.card G)
Tag 0H35, a lemma
Tag 0H35 in the Stacks Project.
Stacks.Invariant.QuotientComparison.exists_monic_map_eq_X_sub_C_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 898. The attribute's comment: “(1)”.
(Lifting characteristic-polynomial form.) For every
b ∈ (R / JR)^Gthere is a monic polynomialP ∈ (R^G / J)[T]whose image underPolynomial.map (invariantComparison J)equals(X - C b) ^ n, wheren = Fintype.card G.
theorem exists_monic_map_eq_X_sub_C_pow [Fintype G] (J : Ideal (FixedPoints.subring R G))
(b : FixedPoints.subring (R ⧸ JRideal J) G) :
∃ P : Polynomial ((FixedPoints.subring R G) ⧸ J),
P.Monic ∧
P.map (invariantComparison J)
= (Polynomial.X - Polynomial.C b) ^ (Fintype.card G)
Stacks.Invariant.QuotientComparison.X_sub_C_pow_eq_X_pow_of_mem_ker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 928. The attribute's comment: “(2)”.
(Kernel elements are nilpotent-like.) For every
a ∈ ker(invariantComparison J)we have(X - C a) ^ n = X ^ nin(R^G / J)[T], wheren = Fintype.card G.
theorem X_sub_C_pow_eq_X_pow_of_mem_ker [Fintype G] (J : Ideal (FixedPoints.subring R G))
(a : (FixedPoints.subring R G) ⧸ J) (ha : a ∈ RingHom.ker (invariantComparison J)) :
(Polynomial.X - Polynomial.C a) ^ (Fintype.card G)
= (Polynomial.X : Polynomial ((FixedPoints.subring R G) ⧸ J)) ^ (Fintype.card G)
Stacks.Invariant.QuotientComparison.invariantComparison_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 974. The attribute's comment: “final statement, integrality”.
(In particular: integrality.) The comparison map
Φ : R^G / J → (R / JR)^Gis an integral ring map: everyb ∈ (R / JR)^Gis a root of the monic polynomial overR^G / Jsupplied byexists_monic_map_eq_X_sub_C_pow, because that polynomial maps to(X - C b) ^ n, which vanishes atb.
theorem invariantComparison_isIntegral [Fintype G] (J : Ideal (FixedPoints.subring R G)) :
(invariantComparison J).IsIntegral
Stacks.Invariant.QuotientComparison.invariantComparison_comap_isHomeomorph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 986. The attribute's comment: “final statement, homeomorphism on spectra”.
(In particular: homeomorphism on spectra.)
Spec(Φ) : Spec((R / JR)^G) → Spec(R^G / J)is a homeomorphism. This isPrimeSpectrum.isHomeomorph\_comap(Stacks 0BR8) applied to the two facts extracted from parts (1) and (2): everyb ∈ (R / JR)^Ghasb ^ nin the range ofΦ(exists_apply_eq_pow), andker Φis nil (ker_invariantComparison_le_nilradical).
theorem invariantComparison_comap_isHomeomorph [Fintype G] (J : Ideal (FixedPoints.subring R G)) :
IsHomeomorph (PrimeSpectrum.comap (invariantComparison J))
Stacks.Invariant.QuotientComparison.invariantComparison_residueField_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 1000. The attribute's comment: “final statement, purely inseparable residue fields”.
(In particular: purely inseparable residue extensions.) For every prime
𝔮 ⊆ (R / JR)^Gwith contraction𝔭 = Φ⁻¹(𝔮) ⊆ R^G / J, the induced extension of residue fieldsκ(𝔭) → κ(𝔮)is purely inseparable. This is the abstract form of Stacks 09EF (isPurelyInseparable_residueField_of_sub_C_pow_witness, proved with Stacks 09EG) applied to the monic witness of part (1).
theorem invariantComparison_residueField_isPurelyInseparable [Fintype G]
(J : Ideal (FixedPoints.subring R G))
(q : Ideal (FixedPoints.subring (R ⧸ JRideal J) G)) [q.IsPrime] :
letI := (Ideal.ResidueField.map (q.comap (invariantComparison J)) q
(invariantComparison J) rfl).toAlgebra
IsPurelyInseparable (Ideal.ResidueField (q.comap (invariantComparison J)))
(Ideal.ResidueField q)
Tag 0H36, a remark
Tag 0H36 in the Stacks Project.
Stacks.Invariant.QuotientComparison.invariantComparison_bijective_of_isUnit_card, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Quotient.lean, line 1107.
Stacks 0H36. If the order of the finite group
Gacting onRis invertible inR, the canonical comparison mapΦ : R^G / J → (R / JR)^Gis an isomorphism.Injectivity: for
a ∈ ker Φthe identity(X - C a) ^ n = X ^ nofX_sub_C_pow_eq_X_pow_of_mem_kerhas vanishing coefficient in degreen - 1, i.e.n • a = 0, andnis invertible. Surjectivity:n⁻¹ ∑_{g ∈ G} g • ris an invariant lift of any invariant classr̄.
theorem invariantComparison_bijective_of_isUnit_card
{R : Type*} [CommRing R] {G : Type*} [Group G] [Fintype G] [MulSemiringAction G R]
(J : Ideal (FixedPoints.subring R G)) (hG : IsUnit (Fintype.card G : R)) :
Function.Bijective (invariantComparison J)
Tag 0BRG, a lemma
Tag 0BRG in the Stacks Project.
FixedPoints.exists_monic_polynomial_and_pow_eq_of_invariant_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/BaseChange.lean, line 399.
Stacks 0BRG. Invariants in
A ⊗[R^G] Rlift to monic degree-|G|polynomial relations overA; moreover, an element in the kernel of the canonical map fromAto those invariants satisfies(X - C a) ^ |G| = X ^ |G|.Present
Aas a quotient ofMvPolynomial A R^G. Base change alongR^G → RpresentsA ⊗[R^G] Ras the corresponding quotient ofMvPolynomial A R, whose invariant subring isMvPolynomial A R^G(fixedPolynomialEquiv), and the kernel of the base-changed presentation is the extensionJRof the kernelJof the original one (baseChangePresentation_ker_eq_JRideal). Both assertions are therefore the corresponding assertions of Stacks 0H35 forJ, transported along the presentation.
theorem exists_monic_polynomial_and_pow_eq_of_invariant_tensorProduct
(R : Type u) [CommRing R]
(G : Type v) [Group G] [Finite G] [MulSemiringAction G R]
(A : Type w) [CommRing A] [Algebra (FixedPoints.subring R G) A]
[MulSemiringAction G (A ⊗[(FixedPoints.subring R G)] R)]
(smul_tmul : ∀ (g : G) (a : A) (r : R),
g • (a ⊗ₜ[(FixedPoints.subring R G)] r) = a ⊗ₜ[(FixedPoints.subring R G)] (g • r)) :
let ι : A →+* FixedPoints.subring (A ⊗[(FixedPoints.subring R G)] R) G :=
RingHom.codRestrict
(Algebra.TensorProduct.includeLeftRingHom (R := FixedPoints.subring R G))
(FixedPoints.subring (A ⊗[(FixedPoints.subring R G)] R) G)
(fun a g => by
simpa [Algebra.TensorProduct.includeLeftRingHom_apply] using smul_tmul g a 1)
(∀ b : FixedPoints.subring (A ⊗[(FixedPoints.subring R G)] R) G,
∃ P : Polynomial A, P.Monic ∧
Polynomial.map ι P = (Polynomial.X - Polynomial.C b) ^ Nat.card G) ∧
∀ a : A, a ∈ RingHom.ker ι →
(Polynomial.X - Polynomial.C a) ^ Nat.card G =
(Polynomial.X : Polynomial A) ^ Nat.card G
Tag 0BRH, a lemma
Tag 0BRH in the Stacks Project.
FixedPoints.canonicalMap_to_invariants_bijective_of_flat_and_isIntegral_isHomeomorph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/BaseChange.lean, line 500.
Stacks 0BRH. The canonical map from a flat algebra over an invariant ring to the invariants after extension of scalars is bijective. In general, the map is integral, is a homeomorphism on prime spectra, and induces purely inseparable residue field extensions.
The unconditional half follows from Stacks 0BRG: the monic witnesses generate the target over
A, and the kernel is nil, soPrimeSpectrum.isHomeomorph_comap_and_isPurelyInseparable_and_baseChange_of_adjoin_eq_topapplies. In the flat caseA ⊗[R^G] R → ∏_{g ∈ G} (A ⊗[R^G] R)hasAas the equalizer of the two mapsr ↦ (g • r)andr ↦ r, because taking equalizers commutes with a flat base change.
theorem canonicalMap_to_invariants_bijective_of_flat_and_isIntegral_isHomeomorph
(R : Type u) [CommRing R]
(G : Type v) [Group G] [Finite G] [MulSemiringAction G R]
(A : Type w) [CommRing A] [Algebra (FixedPoints.subring R G) A]
[MulSemiringAction G (A ⊗[(FixedPoints.subring R G)] R)]
(smul_tmul : ∀ (g : G) (a : A) (r : R),
g • (a ⊗ₜ[(FixedPoints.subring R G)] r) =
a ⊗ₜ[(FixedPoints.subring R G)] (g • r)) :
let ι : A →+* FixedPoints.subring (A ⊗[(FixedPoints.subring R G)] R) G :=
RingHom.codRestrict
(Algebra.TensorProduct.includeLeftRingHom (R := FixedPoints.subring R G))
(FixedPoints.subring (A ⊗[(FixedPoints.subring R G)] R) G)
(fun a g => by
simpa [Algebra.TensorProduct.includeLeftRingHom_apply] using smul_tmul g a 1)
(Module.Flat (FixedPoints.subring R G) A → Function.Bijective ι) ∧
ι.IsIntegral ∧
IsHomeomorph (PrimeSpectrum.comap ι) ∧
∀ (p : Ideal A) [p.IsPrime]
(q : Ideal (FixedPoints.subring (A ⊗[(FixedPoints.subring R G)] R) G)) [q.IsPrime]
(hpq : p = q.comap ι),
(Ideal.ResidueField.map p q ι hpq).IsPurelyInseparable
Tag 0BRI, a lemma
Tag 0BRI in the Stacks Project.
Declarations registered for the tag:
Algebra.IsInvariant.exists_smul_of_under_eqregistered withadd_to_stacksin StacksFrontier/RingTheory/Invariant/Primes.lean, line 60 (StacksFrontier).
Tag 0BRJ, a lemma
Tag 0BRJ in the Stacks Project.
Declarations registered for the tag:
Ideal.IsFractionRing.normalregistered withadd_to_stacksin StacksFrontier/RingTheory/Invariant/Primes.lean, line 62 (StacksFrontier): “normality, hence algebraicity, of the residue field extension”.IsFractionRing.stabilizerHom_surjectiveregistered withadd_to_stacksin StacksFrontier/RingTheory/Invariant/Primes.lean, line 65 (StacksFrontier): “surjectivity of the decomposition group onto the relative automorphisms”. References: SGA 1 V (1.1), “more general”; SGA 1 V (1.3), “special case”.
Tag 0BRK, a lemma
Tag 0BRK in the Stacks Project.
IsIntegralClosure.exists_smul_of_under_eq_and_residue_normal_stabilizerHom_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Primes.lean, line 337. References: SGA 1 V (1.1), “special case”; SGA 1 V (1.3), “special case”.
In a possibly infinite Galois extension, the primes of an integral closure above a fixed prime form one Galois orbit. The induced residue-field extension is normal, and its decomposition group surjects onto the relative automorphism group.
theorem exists_smul_of_under_eq_and_residue_normal_stabilizerHom_surjective
(A : Type uA) (K : Type uK) (L : Type uL) (B : Type uB)
[CommRing A] [CommRing B] [Field K] [Field L]
[Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L]
[Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
[IsScalarTower A B L] [IsIntegrallyClosed A] [IsIntegralClosure B A L]
[IsGalois K L] :
letI := IsIntegralClosure.MulSemiringAction A K L B
letI : SMulCommClass Gal(L/K) A B :=
⟨fun σ a b ↦ by
simp only [Algebra.smul_def, smul_mul']
congr 1
exact (galRestrict A K L B σ).commutes a⟩
(∀ (Q Q' : Ideal B) [Q.IsPrime] [Q'.IsPrime],
Q.under A = Q'.under A → ∃ σ : Gal(L/K), Q' = σ • Q) ∧
∀ (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P],
∀ (k l : Type*) [Field k] [Field l] [Algebra k l]
[Algebra (A ⧸ P) k] [IsFractionRing (A ⧸ P) k]
[Algebra (B ⧸ Q) l] [IsFractionRing (B ⧸ Q) l]
[Algebra (A ⧸ P) l] [IsScalarTower (A ⧸ P) (B ⧸ Q) l]
[IsScalarTower (A ⧸ P) k l],
Normal k l ∧
Function.Surjective (IsFractionRing.stabilizerHom Gal(L/K) P Q k l)
Tag 0BSX, a lemma
Tag 0BSX in the Stacks Project.
IsIntegralClosure.image_stabilizer_and_inertia_restrictNormalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Invariant/Primes.lean, line 403.
In a tower of possibly infinite Galois extensions, restriction maps the decomposition group and the inertia group at a prime of the larger integral closure onto the corresponding groups at its contraction to the smaller integral closure.
theorem image_stabilizer_and_inertia_restrictNormalHom
(A : Type uA) (K : Type uK) (L : Type uL) (M : Type uM)
(B : Type uB) (C : Type uC)
[CommRing A] [Field K] [Field L] [Field M] [CommRing B] [CommRing C]
[Algebra A K] [Algebra K L] [Algebra L M] [Algebra K M]
[Algebra A L] [Algebra A M] [IsScalarTower A K L] [IsScalarTower K L M]
[IsScalarTower A K M] [IsScalarTower A L M]
[Algebra A B] [Algebra B L] [IsScalarTower A B L]
[Algebra A C] [Algebra C M] [IsScalarTower A C M]
[Algebra B C] [Algebra B M] [IsScalarTower A B C]
[IsScalarTower B L M] [IsScalarTower B C M]
[IsFractionRing A K] [IsFractionRing B L] [IsFractionRing C M]
[IsIntegrallyClosed A] [IsIntegralClosure B A L] [IsIntegralClosure C A M]
[IsGalois K L] [IsGalois K M]
(r : Ideal C) [r.IsPrime] :
letI := IsIntegralClosure.MulSemiringAction A K M C
letI : SMulCommClass Gal(M/K) A C :=
⟨fun σ a c ↦ by
simp only [Algebra.smul_def, smul_mul']
congr 1
exact (galRestrict A K M C σ).commutes a⟩
letI := IsIntegralClosure.MulSemiringAction A K L B
letI : SMulCommClass Gal(L/K) A B :=
⟨fun σ a b ↦ by
simp only [Algebra.smul_def, smul_mul']
congr 1
exact (galRestrict A K L B σ).commutes a⟩
let q := r.under B
let res : Gal(M/K) →* Gal(L/K) := AlgEquiv.restrictNormalHom L
res '' (MulAction.stabilizer Gal(M/K) r : Set Gal(M/K)) =
(MulAction.stabilizer Gal(L/K) q : Set Gal(L/K)) ∧
res '' (r.inertia Gal(M/K) : Set Gal(M/K)) =
(q.inertia Gal(L/K) : Set Gal(L/K))
Sources
Section15.113 Extensions of discrete valuation rings#
Section 15.113 of the Stacks Project, Tag 0EXQ. 9 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09E4, a definition
Tag 09E4 in the Stacks Project.
IsDiscreteValuationRing.IsExtension, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Solution.lean, line 60.
An extension of discrete valuation rings is an injective local algebra map.
class IsExtension (A B : Type*) [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] [CommRing B] [IsDomain B]
[IsDiscreteValuationRing B] [Algebra A B] : Prop extends
FaithfulSMul A B, IsLocalHom (algebraMap A B)
IsDiscreteValuationRing.ramificationIndex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Solution.lean, line 67. References: SGA 7 IX (10.3); SGA 7 IX (9.7).
The ramification index of an extension of discrete valuation rings.
noncomputable abbrev ramificationIndex (A B : Type*) [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] [CommRing B] [IsDomain B]
[IsDiscreteValuationRing B] [Algebra A B] [IsExtension A B] : ℕ
IsDiscreteValuationRing.IsWeaklyUnramified, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Solution.lean, line 74.
An extension of DVRs is weakly unramified when its ramification index is one.
abbrev IsWeaklyUnramified (A B : Type*) [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] [CommRing B] [IsDomain B]
[IsDiscreteValuationRing B] [Algebra A B] [IsExtension A B] : Prop
IsDiscreteValuationRing.residueDegree, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Solution.lean, line 81.
The residue degree of an extension of discrete valuation rings.
noncomputable abbrev residueDegree (A B : Type*) [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] [CommRing B] [IsDomain B]
[IsDiscreteValuationRing B] [Algebra A B] [IsExtension A B] : ℕ
IsDiscreteValuationRing.ramificationIndex_characterization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Solution.lean, line 213. References: SGA 7 IX (10.3), “special case”.
The ramification index is positive, is the unique positive exponent expressing the extended maximal ideal as a power of the maximal ideal upstairs, and is the exponent relating any choices of uniformizers up to a unit.
theorem ramificationIndex_characterization (A B : Type*) [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[Algebra A B] [IsExtension A B] :
1 ≤ ramificationIndex A B ∧
(IsLocalRing.maximalIdeal A).map (algebraMap A B) =
IsLocalRing.maximalIdeal B ^ ramificationIndex A B ∧
(∀ e : ℕ, 1 ≤ e →
(IsLocalRing.maximalIdeal A).map (algebraMap A B) =
IsLocalRing.maximalIdeal B ^ e →
e = ramificationIndex A B) ∧
∀ πA : A, Irreducible πA → ∀ πB : B, Irreducible πB →
∃ u : Bˣ, algebraMap A B πA = (u : B) * πB ^ ramificationIndex A B
Tag 09E5, a lemma
Tag 09E5 in the Stacks Project.
IsDiscreteValuationRing.residueField_finite_and_ramificationIdx_mul_residueDegree_le_finrank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/RamificationIndex.lean, line 213.
Let
A → Bbe an injective local map of discrete valuation rings, with compatible fraction fieldsK → L. IfL / Kis finite, then the residue-field extension is finite and its degree, multiplied by the ramification index ofB / A, is at most[L : K].
theorem residueField_finite_and_ramificationIdx_mul_residueDegree_le_finrank
(A B K L : Type*)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[Algebra A B] [FaithfulSMul A B] [IsLocalHom (algebraMap A B)]
[Field K] [Algebra A K] [IsFractionRing A K]
[Field L] [Algebra B L] [IsFractionRing B L]
[Algebra A L] [Algebra K L]
[IsScalarTower A B L] [IsScalarTower A K L]
[Module.Finite K L] :
Module.Finite (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B) ∧
(IsLocalRing.maximalIdeal B).ramificationIdx A *
Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B) ≤
Module.finrank K L
Tag 0BRL, a lemma
Tag 0BRL in the Stacks Project.
IsDiscreteValuationRing.ramificationIdx_and_inertiaDeg_tower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/RamificationIndex.lean, line 280.
Ramification indices and residue degrees multiply in a tower of extensions of discrete valuation rings.
theorem ramificationIdx_and_inertiaDeg_tower
(A B C : Type*)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
[FaithfulSMul A B] [FaithfulSMul B C]
[IsLocalHom (algebraMap A B)] [IsLocalHom (algebraMap B C)] :
(IsLocalRing.maximalIdeal C).ramificationIdx A =
(IsLocalRing.maximalIdeal B).ramificationIdx A *
(IsLocalRing.maximalIdeal C).ramificationIdx B ∧
(IsLocalRing.maximalIdeal C).inertiaDeg A =
(IsLocalRing.maximalIdeal B).inertiaDeg A *
(IsLocalRing.maximalIdeal C).inertiaDeg B
Tag 09E6, a lemma
Tag 09E6 in the Stacks Project.
Stacks.DiscreteValuationRing.Ramification.ramificationIdx_eq_prime_pow_of_purelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/RamificationIndex.lean, line 113.
Stacks 09E6. Let
A ⊂ Bbe an extension of discrete valuation rings inducing the field extensionK ⊂ L. IfKhas characteristicpwithpprime andL / Kis purely inseparable, then the ramification indexeofBoverAis a power ofp: there ism ≥ 0withe = p ^ m.
theorem ramificationIdx_eq_prime_pow_of_purelyInseparable (A B : Type*) [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B]
[FaithfulSMul A B] [IsLocalHom (algebraMap A B)] (K L : Type*) [Field K] [Algebra A K]
[IsFractionRing A K] [Field L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [Algebra K L]
[IsScalarTower A B L] [IsScalarTower A K L] (p : ℕ) (hp : p.Prime) [CharP K p]
[IsPurelyInseparable K L] : ∃ m : ℕ, ramificationIdx A B = p ^ m
Tag 09E7, a lemma
Tag 09E7 in the Stacks Project.
IsDiscreteValuationRing.formallySmooth_iff_weaklyUnramified_and_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/FormallySmoothExtension.lean, line 200.
An extension of discrete valuation rings is formally smooth for the maximal-ideal-adic topology if and only if it is weakly unramified and its possibly nonalgebraic residue-field extension is separable.
theorem formallySmooth_iff_weaklyUnramified_and_isSeparableExtension
(A : Type u) (B : Type v)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[Algebra A B] [IsExtension A B] :
RingHom.FormallySmoothNAdic.{max u v} (algebraMap A B)
(IsLocalRing.maximalIdeal B) ↔
IsWeaklyUnramified A B ∧
Algebra.IsSeparableExtension (IsLocalRing.ResidueField A)
(IsLocalRing.ResidueField B)
Tag 09E8, a remark
Tag 09E8 in the Stacks Project.
IsDiscreteValuationRing.integralClosure_finite_dedekind_and_degree_eq_sum_ramification_inertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Unramified.lean, line 328.
Let
Abe a discrete valuation ring with fraction fieldK, and letL / Kbe a finite separable extension. The integral closureBofAinLis finite and Noetherian overA, has dimension one, and is Dedekind. Its maximal idealsm iare precisely the primes over the maximal ideal ofA; everyB_(m i)is a discrete valuation ring, and[L : K] = ∑ i, e(m i / m_A) * f(m i / m_A). IfAis henselian—or, in particular, maximal-ideal-adically complete—there is exactly one such maximal ideal.
theorem integralClosure_finite_dedekind_and_degree_eq_sum_ramification_inertia
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[Algebra.IsSeparable K L] [Algebra A L] [IsScalarTower A K L] :
let B := integralClosure A L
Module.Finite A B ∧
IsNoetherianRing B ∧
ringKrullDim B = 1 ∧
IsDedekindDomain B ∧
∃ (n : ℕ) (m : Fin n → Ideal B),
∃ hmax : ∀ i, (m i).IsMaximal,
(∀ q : Ideal B, q.IsMaximal ↔ ∃! i, m i = q) ∧
(∀ i, (m i).LiesOver (IsLocalRing.maximalIdeal A)) ∧
(∀ i, letI : (m i).IsPrime := (hmax i).isPrime
IsDiscreteValuationRing (Localization.AtPrime (m i))) ∧
Module.finrank K L = ∑ i, (m i).ramificationIdx A * (m i).inertiaDeg A ∧
(HenselianLocalRing A → n = 1) ∧
(IsAdicComplete (IsLocalRing.maximalIdeal A) A → n = 1)
Tag 09E9, a definition
Tag 09E9 in the Stacks Project.
IsDiscreteValuationRing.IsUnramifiedWithRespectTo, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Unramified.lean, line 416. The attribute's comment: “(1)”.
An extension is unramified with respect to a discrete valuation ring
Aif, at every maximal ideal of the integral closure lying over the maximal ideal ofA, the ramification index is one and the induced residue field extension is separable.
def IsUnramifiedWithRespectTo
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[Algebra.IsSeparable K L] [Algebra A L] [IsScalarTower A K L] : Prop
IsDiscreteValuationRing.IsTamelyRamifiedWithRespectTo, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Unramified.lean, line 431. The attribute's comment: “(2)”. References: SGA 1 XIII (2.0), “L a field extension”.
An extension is tamely ramified with respect to
Aif every induced residue field extension is separable and, in positive residue characteristic, every ramification index is relatively prime to that characteristic. This isStacks.KummerExtension.IsTamelyRamified.
abbrev IsTamelyRamifiedWithRespectTo
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[Algebra.IsSeparable K L] [Algebra A L] [IsScalarTower A K L] : Prop
IsDiscreteValuationRing.IsTotallyRamifiedWithRespectTo, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Unramified.lean, line 442. The attribute's comment: “(3)”.
An extension is totally ramified with respect to
Aif its integral closure has a unique maximal ideal above that ofAand its induced residue field extension is trivial. This isStacks.KummerExtension.IsTotallyRamified.
abbrev IsTotallyRamifiedWithRespectTo
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[Algebra.IsSeparable K L] [Algebra A L] [IsScalarTower A K L] : Prop
Tag 0EXR, a lemma
Tag 0EXR in the Stacks Project.
IsDiscreteValuationRing.isUnramifiedWithRespectTo_of_tower_and_exists_isGalois_and_common_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Unramified.lean, line 772.
Stacks 0EXR. Unramified finite separable extensions of the fraction field of a discrete valuation ring are closed under passage to intermediate fields, admit finite Galois overextensions which remain unramified, and any two admit a common finite separable overextension which remains unramified.
theorem isUnramifiedWithRespectTo_of_tower_and_exists_isGalois_and_common_extension
(A : Type u) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type v) [Field K] [Algebra A K] [IsFractionRing A K] :
(∀ (L : Type w) [Field L] [Algebra K L] [FiniteDimensional K L]
[Algebra.IsSeparable K L] [Algebra A L] [IsScalarTower A K L]
(M : Type x) [Field M] [Algebra L M] [FiniteDimensional L M]
[Algebra.IsSeparable L M] [Algebra K M] [IsScalarTower K L M]
[Algebra A M] [IsScalarTower A K M],
letI : FiniteDimensional K M := FiniteDimensional.trans K L M
letI : Algebra.IsSeparable K M := Algebra.IsSeparable.trans K L M
IsUnramifiedWithRespectTo A K M →
IsUnramifiedWithRespectTo A K L) ∧
(∀ (L : Type w) [Field L] [Algebra K L] [FiniteDimensional K L]
[Algebra.IsSeparable K L] [Algebra A L] [IsScalarTower A K L],
IsUnramifiedWithRespectTo A K L →
∃ (M : Type (max u v w)) (_ : Field M) (_ : Algebra K M)
(_ : FiniteDimensional K M) (_ : Algebra.IsSeparable K M)
(_ : Algebra A M) (_ : IsScalarTower A K M)
(_ : Algebra L M) (_ : IsScalarTower K L M),
IsGalois K M ∧ IsUnramifiedWithRespectTo A K M) ∧
(∀ (L₁ : Type w) [Field L₁] [Algebra K L₁] [FiniteDimensional K L₁]
[Algebra.IsSeparable K L₁] [Algebra A L₁] [IsScalarTower A K L₁]
(L₂ : Type x) [Field L₂] [Algebra K L₂] [FiniteDimensional K L₂]
[Algebra.IsSeparable K L₂] [Algebra A L₂] [IsScalarTower A K L₂],
IsUnramifiedWithRespectTo A K L₁ →
IsUnramifiedWithRespectTo A K L₂ →
∃ (L : Type (max u v w x)) (_ : Field L) (_ : Algebra K L)
(_ : FiniteDimensional K L) (_ : Algebra.IsSeparable K L)
(_ : Algebra A L) (_ : IsScalarTower A K L)
(_ : Algebra L₁ L) (_ : IsScalarTower K L₁ L)
(_ : Algebra L₂ L) (_ : IsScalarTower K L₂ L),
IsUnramifiedWithRespectTo A K L)
Tag 0EXS, a lemma
Tag 0EXS in the Stacks Project.
IsDiscreteValuationRing.isUnramifiedIn_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Unramified.lean, line 871. References: SGA 1 I (10.4), “(ii) transitivity”.
If
pis unramified inBandCis unramified over every prime ofBlying overp, thenpis unramified inC.
theorem isUnramifiedIn_comp
(A B C : Type*) [CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
(p : Ideal A) (hAB : Algebra.IsUnramifiedIn B p)
(hBC : ∀ (q : Ideal B) (_ : q.IsPrime), q.LiesOver p → Algebra.IsUnramifiedIn C q) :
Algebra.IsUnramifiedIn C p
Sources
Section15.114 Galois extensions and ramification#
Section 15.114 of the Stacks Project, Tag 09E3. 12 tags here are carried by 17 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09EA, a lemma
Tag 09EA in the Stacks Project.
IsDiscreteValuationRing.galAction_transitive_on_maximalIdeals_integralClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Galois.lean, line 157.
For a finite Galois extension
L / K, the canonical action ofGal(L/K)on the integral closure of a discrete valuation ringAinLis transitive on its maximal ideals.
theorem galAction_transitive_on_maximalIdeals_integralClosure
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[IsGalois K L] [Algebra A L] [IsScalarTower A K L] :
let B := integralClosure A L
letI := IsIntegralClosure.MulSemiringAction A K L B
∀ P Q : Ideal B, P.IsMaximal → Q.IsMaximal →
∃ σ : Gal(L/K), σ • P = Q
Tag 09EB, a lemma
Tag 09EB in the Stacks Project.
IsDiscreteValuationRing.exists_uniform_ramificationIdx_inertiaDeg_and_finrank_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Galois.lean, line 182.
In a finite Galois extension of the fraction field of a discrete valuation ring, all primes of the integral closure over the maximal ideal have the same positive ramification index and inertia degree. The field degree is the number of these primes times the two common values.
theorem exists_uniform_ramificationIdx_inertiaDeg_and_finrank_eq
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[IsGalois K L] [Algebra A L] [IsScalarTower A K L] :
let B := integralClosure A L
let p := IsLocalRing.maximalIdeal A
∃ e f : ℕ,
1 ≤ e ∧
1 ≤ f ∧
(∀ P : p.primesOver B, P.1.ramificationIdx A = e ∧ P.1.inertiaDeg A = f) ∧
(p.primesOver B).ncard * e * f = Module.finrank K L
Tag 09EC, a definition
Tag 09EC in the Stacks Project.
IsDiscreteValuationRing.under_eq_maximalIdeal_and_ker_stabilizerHom_eq_inertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Galois.lean, line 235. The attribute's comment: “The decomposition group is MulAction.stabilizer and the inertia group is Ideal.inertia, both of which Mathlib already has for an arbitrary action; what is recorded here is that they are the source's two groups, the ideal below P being the maximal ideal of A so that the extension acted on is κ(P)/κ_A. Stated without the fraction-field, finiteness and Galois hypotheses, which the comparison does not use, so the source's setting is a special case.”. References: SGA 7 I (0.3), “partial”.
The decomposition and the inertia group at a maximal ideal
Pof the integral closureBof a discrete valuation ringAin a field extensionL / K.The decomposition group is the stabilizer
{σ ∈ Gal(L/K) | σ P = P}, and the ideal ofAbelowPis the maximal ideal, so the residue extension the decomposition group acts on really isκ(P) / κ_A. The inertia group is the kernel of that action: it isIdeal.inertia, sitting inside the decomposition group, and an element of the decomposition group lies in it exactly when it acts trivially onκ(P).
theorem under_eq_maximalIdeal_and_ker_stabilizerHom_eq_inertia
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K]
(L : Type*) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
(P : Ideal (integralClosure A L)) [P.IsMaximal] :
let B := integralClosure A L
let D := MulAction.stabilizer Gal(L/K) P
let I := P.inertia Gal(L/K)
(∀ σ : Gal(L/K), σ ∈ D ↔ σ • P = P) ∧
P.under A = IsLocalRing.maximalIdeal A ∧
I ≤ D ∧
(Ideal.Quotient.stabilizerHom P (P.under A) Gal(L/K)).ker = I.subgroupOf D ∧
(∀ σ : D, σ ∈ (Ideal.Quotient.stabilizerHom P (P.under A) Gal(L/K)).ker ↔
∀ b : B, Ideal.Quotient.mk P ((σ : Gal(L/K)) • b) = Ideal.Quotient.mk P b)
Declarations registered for the tag:
MulAction.stabilizerregistered withadd_to_stacksin StacksFrontier/RingTheory/DiscreteValuationRing/Galois.lean, line 102 (StacksFrontier): “(1), the decomposition group”. References: SGA 1 V (6.13); SGA 3 I (2.3.3), “special case”; SGA 3 VIIB (2.5.A); SGA 3 XXI (6.7.2), “more general”; SGA 5 IIIB (5.13), “more general”; SGA 5 X (4.2).Ideal.inertiaregistered withadd_to_stacksin StacksFrontier/RingTheory/DiscreteValuationRing/Galois.lean, line 110 (StacksFrontier): “(2), the inertia group”. References: SGA 7 I (0.3); SGA 7 XIII (0.2).Ideal.Quotient.stabilizerHomregistered withadd_to_stacksin StacksFrontier/RingTheory/DiscreteValuationRing/Galois.lean, line 114 (StacksFrontier): “The action of the decomposition group on the residue algebra”.Ideal.Quotient.ker_stabilizerHomregistered withadd_to_stacksin StacksFrontier/RingTheory/DiscreteValuationRing/Galois.lean, line 117 (StacksFrontier): “The inertia group as the kernel of the residue-algebra action”.
Tag 09ED, a lemma
Tag 09ED in the Stacks Project.
IsDiscreteValuationRing.residueField_normal_and_stabilizerHom_surjective_of_isGalois, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Galois.lean, line 263. References: SGA 1 V (1.1), “special case”; SGA 1 V (1.3), “special case”.
In a finite Galois extension of the fraction field of a discrete valuation ring, every residue extension at a maximal ideal of the integral closure is normal, and its decomposition group surjects onto the relative automorphism group. Separability of one such residue extension is equivalent to separability of all of them; when this holds, the fixed residue extension is Galois and the same canonical map is surjective onto its Galois group.
theorem residueField_normal_and_stabilizerHom_surjective_of_isGalois
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[IsGalois K L] [Algebra A L] [IsScalarTower A K L]
(P : Ideal (integralClosure A L)) [P.IsMaximal] :
let B := integralClosure A L
let p := P.under A
letI : Field (A ⧸ p) := Ideal.Quotient.field p
letI : Field (B ⧸ P) := Ideal.Quotient.field P
Normal (A ⧸ p) (B ⧸ P) ∧
Function.Surjective (Ideal.Quotient.stabilizerHom P p Gal(L/K)) ∧
((∃ (Q : Ideal B) (_hQ : Q.IsMaximal),
let q := Q.under A
letI : Field (A ⧸ q) := Ideal.Quotient.field q
letI : Field (B ⧸ Q) := Ideal.Quotient.field Q
Algebra.IsSeparable (A ⧸ q) (B ⧸ Q)) ↔
(∀ (Q : Ideal B) (_hQ : Q.IsMaximal),
let q := Q.under A
letI : Field (A ⧸ q) := Ideal.Quotient.field q
letI : Field (B ⧸ Q) := Ideal.Quotient.field Q
Algebra.IsSeparable (A ⧸ q) (B ⧸ Q))) ∧
((∃ (Q : Ideal B) (_hQ : Q.IsMaximal),
let q := Q.under A
letI : Field (A ⧸ q) := Ideal.Quotient.field q
letI : Field (B ⧸ Q) := Ideal.Quotient.field Q
Algebra.IsSeparable (A ⧸ q) (B ⧸ Q)) →
IsGalois (A ⧸ p) (B ⧸ P) ∧
Function.Surjective (Ideal.Quotient.stabilizerHom P p Gal(L/K)))
Tag 09EE, a lemma
Tag 09EE in the Stacks Project.
IsDiscreteValuationRing.exists_wildInertia_exact_and_tameInertia_equiv_rootsOfUnity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Galois.lean, line 847. References: SGA 1 XIII (2.0), “inertia structure”; SGA 7 I (0.3), “finite Galois case”.
The inertia group at a maximal ideal of the integral closure in a finite Galois extension has a canonical wild–tame exact sequence. Wild inertia consists precisely of the elements of inertia acting trivially on the maximal ideal modulo its square; it is normal in the decomposition group and is a
p-group in positive residue characteristic (and trivial in characteristic zero). The tame quotient is cyclic of prime-to-porder and is canonically isomorphic to the corresponding roots of unity in the residue field. If the residue extension is separable, wild inertia is also the kernel of the action onB / P².
theorem exists_wildInertia_exact_and_tameInertia_equiv_rootsOfUnity
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[IsGalois K L] [Algebra A L] [IsScalarTower A K L]
(P : Ideal (integralClosure A L)) [P.IsMaximal] :
let B := integralClosure A L
letI := IsIntegralClosure.MulSemiringAction A K L B
let D := MulAction.stabilizer Gal(L/K) P
let I := P.inertia Gal(L/K)
let inclusion : I →* D := I.subtype.codRestrict D
(fun σ ↦ Ideal.inertia_le_stabilizer (M := Gal(L/K)) P σ.property)
let e := P.ramificationIdx A
let p := ringChar (IsLocalRing.ResidueField A)
∃ W : Subgroup I, ∃ _hW : W.Normal,
(W.map inclusion).Normal ∧
(∀ σ : I, σ ∈ W ↔ ∀ b : B, b ∈ P → (σ : Gal(L/K)) • b - b ∈ P ^ 2) ∧
(∀ σ : D, σ ∈ W.map inclusion ↔
(σ : Gal(L/K)) ∈ I ∧ ∀ b : B, b ∈ P → σ • b - b ∈ P ^ 2) ∧
(0 < p → IsPGroup p W) ∧
(p = 0 → W = ⊥) ∧
(letI : Field (A ⧸ P.under A) := Ideal.Quotient.field (P.under A)
Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) →
∀ σ : D, σ ∈ W.map inclusion ↔ ∀ b : B, σ • b - b ∈ P ^ 2) ∧
∃ θ : I →* rootsOfUnity e (B ⧸ P),
Function.Injective W.subtype ∧
Function.MulExact W.subtype θ ∧
Function.Surjective θ ∧
IsCyclic (rootsOfUnity e (B ⧸ P)) ∧
Nat.card (rootsOfUnity e (B ⧸ P)) = e / p ^ e.factorization p ∧
(∀ (σ : I) (x a : B), x ∈ P → x ∉ P ^ 2 →
Ideal.Quotient.mk P a = (θ σ).1.1 →
(σ : Gal(L/K)) • x - a * x ∈ P ^ 2) ∧
∀ θ' : I →* rootsOfUnity e (B ⧸ P),
(∀ (σ : I) (x a : B), x ∈ P → x ∉ P ^ 2 →
Ideal.Quotient.mk P a = (θ' σ).1.1 →
(σ : Gal(L/K)) • x - a * x ∈ P ^ 2) →
θ' = θ
Tag 0BU3, an equation
Tag 0BU3 in the Stacks Project.
IsDiscreteValuationRing.exists_uniformizerRatioMap_to_rootsOfUnity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Galois.lean, line 992.
Let a group act on a discrete valuation ring, trivially on its residue field. Suppose an invariant element is a unit times the
e-th power of a uniformizer. For every group element, its action on the uniformizer differs from the uniformizer by a unit; the residues of these units aree-th roots of unity and hence define a map to the group of such roots.
theorem exists_uniformizerRatioMap_to_rootsOfUnity
(C : Type u) [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
(I : Type v) [Group I] [MulSemiringAction I C]
(e : ℕ) (π a : C) (u : Cˣ)
(hπ : Irreducible π)
(ha : a = (u : C) * π ^ e)
(ha_fixed : ∀ σ : I, σ • a = a)
(hres : ∀ (σ : I) (x : C),
Ideal.Quotient.mk (IsLocalRing.maximalIdeal C) (σ • x) =
Ideal.Quotient.mk (IsLocalRing.maximalIdeal C) x) :
∃ (θ : I → rootsOfUnity e (C ⧸ IsLocalRing.maximalIdeal C))
(θunit : I → Cˣ),
(∀ σ : I, (θunit σ : C) * π = σ • π) ∧
∀ σ : I,
(θ σ : (C ⧸ IsLocalRing.maximalIdeal C)ˣ) =
Units.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal C)) (θunit σ)
Tag 0BU4, a definition
Tag 0BU4 in the Stacks Project.
IsDiscreteValuationRing.inertiaCharacter, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/Character.lean, line 176.
Stacks Project, Tag 0BU4. The canonical character from inertia to the roots of unity of order the ramification index in the residue field.
noncomputable def inertiaCharacter
IsDiscreteValuationRing.wildInertiaGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/Character.lean, line 180. References: SGA 1 XIII (2.0), “partial”.
Stacks Project, Tag 0BU4. The wild inertia group at
P.
noncomputable def wildInertiaGroup
IsDiscreteValuationRing.tameInertiaGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/Character.lean, line 188. References: SGA 7 I (0.3).
Stacks Project, Tag 0BU4. The tame inertia group, namely inertia modulo wild inertia.
abbrev tameInertiaGroup
IsDiscreteValuationRing.tameInertiaMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/Character.lean, line 192.
Stacks Project, Tag 0BU4. The quotient map from inertia to tame inertia.
noncomputable def tameInertiaMap : P.inertia Gal(L/K) →* tameInertiaGroup A K L P
IsDiscreteValuationRing.tameInertiaEquivRootsOfUnity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/Character.lean, line 205. References: SGA 7 I (0.3), “finite Galois case”.
Stacks Project, Tag 0BU4. The canonical isomorphism from tame inertia to the roots of unity induced by the inertia character.
noncomputable def tameInertiaEquivRootsOfUnity :
tameInertiaGroup A K L P ≃*
rootsOfUnity (P.ramificationIdx A) (integralClosure A L ⧸ P)
Tag 0BU5, a lemma
Tag 0BU5 in the Stacks Project.
IsDiscreteValuationRing.inertiaCharacter_conj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/Character.lean, line 238. References: SGA 7 I (0.3), “finite Galois case”.
Stacks Tag 0BU5. The inertia character is equivariant for conjugation by the decomposition group: conjugating an inertia element by a decomposition element has character equal to the image of the original character under the induced residue-field automorphism.
theorem inertiaCharacter_conj
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[IsGalois K L] [Algebra A L] [IsScalarTower A K L]
(P : Ideal (integralClosure A L)) [P.IsMaximal] :
let B := integralClosure A L
letI := IsIntegralClosure.MulSemiringAction A K L B
let D := MulAction.stabilizer Gal(L/K) P
let I := P.inertia Gal(L/K)
let e := P.ramificationIdx A
let conjugate : D → I → I := fun τ σ ↦
⟨(τ : Gal(L/K)) * (σ : Gal(L/K)) * (τ : Gal(L/K))⁻¹, by
rw [Ideal.mem_inertia]
intro x
have hσ := (Ideal.mem_inertia.mp σ.property) ((τ : Gal(L/K))⁻¹ • x)
have hτ := Ideal.smul_mem_pointwise_smul (τ : Gal(L/K)) _ P hσ
rw [τ.property] at hτ
simpa only [mul_smul, smul_sub, smul_inv_smul] using hτ⟩
∀ (θ : I →* rootsOfUnity e (B ⧸ P)),
(∀ (σ : I) (x a : B), x ∈ P → x ∉ P ^ 2 →
Ideal.Quotient.mk P a = (θ σ).1.1 →
(σ : Gal(L/K)) • x - a * x ∈ P ^ 2) →
∀ (τ : D) (σ : I),
θ (conjugate τ σ) =
(Ideal.quotientEquiv P P
((MulSemiringAction.toRingEquiv Gal(L/K) B) (τ : Gal(L/K)))
τ.property.symm).toMulEquiv.restrictRootsOfUnity e (θ σ)
Tag 09EH, a lemma
Tag 09EH in the Stacks Project.
IsDiscreteValuationRing.inertia_fixedSubalgebra_isIntegralClosure_and_etale_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/InvariantRing.lean, line 229. References: SGA 7 I (0.3), “partial”.
Stacks Tag 09EH. The subring of the integral closure fixed by the inertia group is the integral closure in the fixed field, and its localization at the prime below the chosen maximal ideal is étale over the original discrete valuation ring.
theorem inertia_fixedSubalgebra_isIntegralClosure_and_etale_localization
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[IsGalois K L] [Algebra A L] [IsScalarTower A K L]
(P : Ideal (integralClosure A L)) [P.IsMaximal] :
let B := integralClosure A L
letI := IsIntegralClosure.MulSemiringAction A K L B
letI : SMulCommClass Gal(L/K) A B :=
⟨fun g a b ↦ by
simp only [Algebra.smul_def]
change galRestrict A K L B g (algebraMap A B a * b) =
algebraMap A B a * galRestrict A K L B g b
rw [map_mul, AlgEquiv.commutes]⟩
let I := P.inertia Gal(L/K)
let B' := FixedPoints.subalgebra A B I
let L' := IntermediateField.fixedField I
let inclusion : B' →ₐ[A] L := (integralClosure A L).val.comp B'.val
let iota : B' →ₐ[A] L' :=
inclusion.codRestrict (L'.toSubalgebra.restrictScalars A) (fun b ↦ by
change (inclusion b : L) ∈ L'
rw [IntermediateField.mem_fixedField_iff]
intro g hg
exact (algebraMap_galRestrict_apply A g (b : B)).symm.trans
(congrArg (algebraMap B L) (b.property ⟨g, hg⟩)))
letI := iota.toAlgebra
IsIntegralClosure B' A L' ∧
Algebra.Etale A (Localization.AtPrime (P.under B'))
Tag 0BU6, a remark
Tag 0BU6 in the Stacks Project.
IsDiscreteValuationRing.decomposition_inertia_wildInertia_tower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/DecompositionTower.lean, line 622.
Stacks Tag 0BU6. The fixed fields, invariant rings, contracted primes, localized rings, and residue fields attached to the wild inertia, inertia, and decomposition groups of a maximal ideal in a finite Galois extension form the standard ramification tower.
theorem decomposition_inertia_wildInertia_tower
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[IsGalois K L] [Algebra A L] [IsScalarTower A K L]
(m : Ideal (integralClosure A L)) [m.IsMaximal] :
let B := integralClosure A L
letI := IsIntegralClosure.MulSemiringAction A K L B
letI : SMulCommClass Gal(L/K) A B :=
⟨fun g a b ↦ by
simp only [Algebra.smul_def]
change galRestrict A K L B g (algebraMap A B a * b) =
algebraMap A B a * galRestrict A K L B g b
rw [map_mul, AlgEquiv.commutes]⟩
let D := MulAction.stabilizer Gal(L/K) m
let I := m.inertia Gal(L/K)
let hID : I ≤ D := Ideal.inertia_le_stabilizer (M := Gal(L/K)) m
let iID : I →* D := I.subtype.codRestrict D (fun σ ↦ hID σ.property)
∃ (P : Subgroup I) (hP : P.Normal),
let PG : Subgroup Gal(L/K) := P.map I.subtype
let PD : Subgroup D := P.map iID
(∀ σ : D, σ ∈ PD ↔ (σ : Gal(L/K)) ∈ I ∧
∀ b : B, b ∈ m → (σ : Gal(L/K)) • b - b ∈ m ^ 2) ∧
let ID : Subgroup D := I.subgroupOf D
let LD := IntermediateField.fixedField D
let LI := IntermediateField.fixedField I
let LP := IntermediateField.fixedField PG
let BD := FixedPoints.subalgebra A B D
let BI := FixedPoints.subalgebra A B I
let BP := FixedPoints.subalgebra A B PG
let hPGI : PG ≤ I := fun σ hσ ↦ by
obtain ⟨τ, -, rfl⟩
Tag 0BU7, a lemma
Tag 0BU7 in the Stacks Project.
IsDiscreteValuationRing.surjective_restrictions_commute_with_residue_and_inertiaCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/GaloisTower.lean, line 197.
Stacks Project, Tag 0BU7. In a tower of finite Galois extensions of the fraction field of a discrete valuation ring, restriction surjects on decomposition, inertia, and wild inertia groups. The induced maps commute with residue-field automorphisms and with the canonical inertia characters; on roots of unity the latter vertical map is the
e' / e-power map.
theorem surjective_restrictions_commute_with_residue_and_inertiaCharacter
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
[IsGalois K L] [Algebra A L] [IsScalarTower A K L]
(M : Type*) [Field M] [Algebra K M] [FiniteDimensional K M]
[IsGalois K M] [Algebra L M] [IsScalarTower K L M]
[Algebra A M] [IsScalarTower A K M] [IsScalarTower A L M]
(r : Ideal (integralClosure A M)) [r.IsMaximal] :
let B := integralClosure A L
let C := integralClosure A M
let fBC : B →ₐ[A] C := (IsScalarTower.toAlgHom A L M).mapIntegralClosure
letI : Algebra B C := fBC.toRingHom.toAlgebra
letI : IsScalarTower A B C :=
IsScalarTower.of_algebraMap_eq fun x ↦ (fBC.commutes x).symm
letI : Algebra.IsIntegral B C :=
⟨fun x ↦ IsIntegral.tower_top (IsIntegralClosure.isIntegral A M x)⟩
letI : MulSemiringAction Gal(M/K) C :=
IsIntegralClosure.MulSemiringAction A K M C
letI : MulSemiringAction Gal(L/K) B :=
IsIntegralClosure.MulSemiringAction A K L B
let q := r.under B
let p := r.under A
letI : r.LiesOver q := ⟨rfl⟩
letI : q.LiesOver p := ⟨r.under_under.symm⟩
letI : Field (A ⧸ p) := Ideal.Quotient.field p
letI : Field (B ⧸ q) := Ideal.Quotient.field q
letI : Field (C ⧸ r) := Ideal.Quotient.field r
letI : Algebra (B ⧸ q) (C ⧸ r) := Ideal.Quotient.algebraOfLiesOver r q
letI : Algebra (A ⧸ p) (B ⧸ q) := Ideal.Quotient.algebraOfLiesOver q p
letI : Algebra (A ⧸ p) (C ⧸ r) := Ideal.Quotient.algebraOfLiesOver r p
let res : Gal(M/K) →* Gal(L/K) := AlgEquiv.restrictNormalHom L
let D' := MulAction.stabilizer Gal(M/K) r
let D := MulAction.stabilizer Gal(L/K) q
let e' := r.ramificationIdx A
let e := q.ramificationIdx A
∃ (resD : D' →* D)
(resI : r.inertia Gal(M/K) →* q.inertia Gal(L/K))
(resP : wildInertiaGroup A K M r →*
wildInertiaGroup A K L q),
Function.Surjective resD ∧ Function.Surjective resI ∧ Function.Surjective resP ∧
(∀ σ, ((resD σ : D) : Gal(L/K)) = res ((σ : D') : Gal(M/K))) ∧
(∀ σ, (resI σ).1 = res σ.1) ∧
(∀ σ, (resP σ).1.1 = res σ.1.1) ∧
e ∣ e' ∧
∃ (residueRestriction : Gal((C ⧸ r)/(A ⧸ p)) →* Gal((B ⧸ q)/(A ⧸ p)))
(rootRestriction : rootsOfUnity e' (C ⧸ r) →* rootsOfUnity e (B ⧸ q)),
(∀ τ b, algebraMap (B ⧸ q) (C ⧸ r) (residueRestriction τ b) =
τ (algebraMap (B ⧸ q) (C ⧸ r) b)) ∧
(∀ ζ, algebraMap (B ⧸ q) (C ⧸ r) (rootRestriction ζ).1.1 =
(ζ ^ (e' / e)).1.1) ∧
(∀ σ b, algebraMap (B ⧸ q) (C ⧸ r)
(Ideal.Quotient.mk q ((resD σ).1 • b)) =
Ideal.Quotient.mk r (σ.1 • fBC b)) ∧
∀ σ, rootRestriction (inertiaCharacter A K M r σ) =
inertiaCharacter A K L q (resI σ)
Tag 0BU8, a remark
Tag 0BU8 in the Stacks Project.
IsDiscreteValuationRing.canonicalInertiaCharacter, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/GaloisTower.lean, line 486.
Stacks Project, Tag 0BU8. The canonical inertia character, obtained by raising the ordinary inertia character to the residue-characteristic-primary part of the ramification index.
noncomputable def canonicalInertiaCharacter :
P.inertia Gal(L/K) →*
rootsOfUnity (tameRamificationIndex A L P) (integralClosure A L ⧸ P)
IsDiscreteValuationRing.canonicalInertiaCharacter_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Inertia/GaloisTower.lean, line 518. References: SGA 7 I (0.3), “finite Galois case”.
Stacks Project, Tag 0BU8. The scaled inertia character identifies tame inertia with the roots of unity of order
|I_t|. Its order is the prime-to-residue-characteristic part of the ramification index, it is equivariant under the decomposition group, and these canonical characters form the stated power-map square in every finite Galois tower.
theorem canonicalInertiaCharacter_spec :
let B := integralClosure A L
letI := IsIntegralClosure.MulSemiringAction A K L B
let D := MulAction.stabilizer Gal(L/K) P
let I := P.inertia Gal(L/K)
let e := P.ramificationIdx A
let p := ringChar (IsLocalRing.ResidueField A)
let q := wildRamificationFactor A L P
let n := tameRamificationIndex A L P
let conjugate : D → I → I := fun τ σ ↦
⟨(τ : Gal(L/K)) * (σ : Gal(L/K)) * (τ : Gal(L/K))⁻¹, by
rw [Ideal.mem_inertia]
intro x
have hσ := (Ideal.mem_inertia.mp σ.property) ((τ : Gal(L/K))⁻¹ • x)
have hτ := Ideal.smul_mem_pointwise_smul (τ : Gal(L/K)) _ P hσ
rw [τ.property] at hτ
simpa only [mul_smul, smul_sub, smul_inv_smul] using hτ⟩
e = q * n ∧
(p = 0 → q = 1) ∧
(0 < p → ∃ a : ℕ, q = p ^ a) ∧
rootsOfUnity e (B ⧸ P) = rootsOfUnity n (B ⧸ P) ∧
Nat.card (tameInertiaGroup A K L P) = n ∧
∃ θcan : tameInertiaGroup A K L P ≃* rootsOfUnity n (B ⧸ P),
(∀ σ : I, θcan (tameInertiaMap A K L P σ) =
canonicalInertiaCharacter A K L P σ) ∧
(∀ (τ : D) (σ : I),
canonicalInertiaCharacter A K L P (conjugate τ σ) =
(Ideal.quotientEquiv P P
((MulSemiringAction.toRingEquiv Gal(L/K) B) (τ : Gal(L/K)))
τ.property.symm).toMulEquiv.restrictRootsOfUnity n
(canonicalInertiaCharacter A K L P σ)) ∧
∀ (M : Type*) [Field M] [Algebra K M] [FiniteDimensional K M]
[IsGalois K M] [Algebra L M] [IsScalarTower K L M]
[Algebra A M] [IsScalarTower A K M] [IsScalarTower A L M]
(r : Ideal (integralClosure A M)) [r.IsMaximal],
let C := integralClosure A M
let fBC : B →ₐ[A] C := (IsScalarTower.toAlgHom A L M).mapIntegralClosure
letI : Algebra B C := fBC.toRingHom.toAlgebra
letI : IsScalarTower A B C :=
IsScalarTower.of_algebraMap_eq fun x ↦ (fBC.commutes x).symm
letI : Algebra.IsIntegral B C :=
⟨fun x ↦ IsIntegral.tower_top (IsIntegralClosure.isIntegral A M x)⟩
letI : MulSemiringAction Gal(M/K) C :=
IsIntegralClosure.MulSemiringAction A K M C
let Q := r.under B
let pA := r.under A
letI : r.LiesOver Q := ⟨rfl⟩
letI : Q.LiesOver pA := ⟨r.under_under.symm⟩
letI : Field (A ⧸ pA) := Ideal.Quotient.field pA
letI : Field (B ⧸ Q) := Ideal.Quotient.field Q
letI : Field (C ⧸ r) := Ideal.Quotient.field r
letI : Algebra (B ⧸ Q) (C ⧸ r) := Ideal.Quotient.algebraOfLiesOver r Q
let _e' := r.ramificationIdx A
let n' := tameRamificationIndex A M r
let n := tameRamificationIndex A L Q
let res : Gal(M/K) →* Gal(L/K) := AlgEquiv.restrictNormalHom L
∃ (resI : r.inertia Gal(M/K) →* Q.inertia Gal(L/K))
(rootRestriction : rootsOfUnity n' (C ⧸ r) →* rootsOfUnity n (B ⧸ Q)),
(∀ σ, (resI σ).1 = res σ.1) ∧
n ∣ n' ∧
(∀ ζ, algebraMap (B ⧸ Q) (C ⧸ r) (rootRestriction ζ).1.1 =
(ζ ^ (n' / n)).1.1) ∧
∀ σ, rootRestriction (canonicalInertiaCharacter A K M r σ) =
canonicalInertiaCharacter A K L Q (resI σ)
Sources
Section15.115 Krasner's lemma#
Section 15.115 of the Stacks Project, Tag 0BU9. 3 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09EI, a lemma
Tag 09EI in the Stacks Project.
krasner_lemma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Krasner.lean, line 295.
Krasner's lemma (Stacks Tag 09EI). Let
Abe a complete local Noetherian domain of Krull dimension1with maximal idealm. Ifαis a root ofPthat is not a root ofP', then for everycthere is annsuch that any polynomialQwhose coefficients all lie inm ^ nmakesP + Qhave a rootβwithβ - α ∈ m ^ c.
theorem krasner_lemma
(A : Type*) [CommRing A] [IsDomain A] [IsLocalRing A] [IsNoetherianRing A]
(hdim : ringKrullDim A = 1)
[IsAdicComplete (maximalIdeal A) A]
(P : A[X]) (α : A)
(hroot : P.eval α = 0)
(hderiv : (derivative P).eval α ≠ 0) :
∀ c : ℕ, ∃ n : ℕ, ∀ Q : A[X], (∀ i, Q.coeff i ∈ (maximalIdeal A) ^ n) →
∃ β : A, (P + Q).eval β = 0 ∧ β - α ∈ (maximalIdeal A) ^ c
Tag 09EJ, a lemma
Tag 09EJ in the Stacks Project.
Krasner.exists_finite_separable_extension_tensorProduct_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Krasner.lean, line 851.
Stacks 09EJ. Let
Abe a Noetherian local ring whose completion at its maximal ideal is a one-dimensional domain. A finite separable extension of the fraction field of the completion is obtained by scalar extension from a finite separable extension of the fraction field ofA.
theorem exists_finite_separable_extension_tensorProduct_equiv
{A K Khat M : Type*} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
[IsDomain (AdicCompletion (IsLocalRing.maximalIdeal A) A)]
(hAhat_dim : ringKrullDim (AdicCompletion (IsLocalRing.maximalIdeal A) A) = 1)
[Field K] [Algebra A K] [IsFractionRing A K]
[Field Khat]
[Algebra (AdicCompletion (IsLocalRing.maximalIdeal A) A) Khat]
[IsFractionRing (AdicCompletion (IsLocalRing.maximalIdeal A) A) Khat]
[Field M] [Algebra Khat M] [FiniteDimensional Khat M]
[Algebra.IsSeparable Khat M] :
let Ahat := AdicCompletion (IsLocalRing.maximalIdeal A) A
letI : Algebra A Khat :=
((algebraMap Ahat Khat).comp (algebraMap A Ahat)).toAlgebra
letI : Algebra K Khat :=
(IsFractionRing.lift (A := A) (K := K) (L := Khat) (g := algebraMap A Khat)
((IsFractionRing.injective Ahat Khat).comp
(by
dsimp only [Ahat]
exact AdicCompletion.of_injective (IsLocalRing.maximalIdeal A) A))).toAlgebra
∃ L : IntermediateField K (AlgebraicClosure K),
FiniteDimensional K L ∧ Algebra.IsSeparable K L ∧
Nonempty (TensorProduct K Khat L ≃ₐ[Khat] M)
Tag 09EK, a definition
Tag 09EK in the Stacks Project.
IsDiscreteValuationRing.HasMixedCharacteristic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/MixedCharacteristic.lean, line 52.
A discrete valuation ring has mixed characteristic
(0, p)ifpis positive, its residue field has characteristicp, and its fraction field has characteristic zero.
abbrev HasMixedCharacteristic (A : Type*) [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] (p : ℕ) : Prop
IsDiscreteValuationRing.integerLocalization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/MixedCharacteristic.lean, line 58.
The localization
ℤ_(p)associated to a mixed-characteristic discrete valuation ring.
noncomputable abbrev integerLocalization (A : Type*) [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] {p : ℕ} (h : HasMixedCharacteristic A p) : Type
IsDiscreteValuationRing.mixedCharacteristicRingHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/MixedCharacteristic.lean, line 67.
The canonical map
ℤ_(p) → Aattached to a mixed-characteristic discrete valuation ring.
noncomputable def mixedCharacteristicRingHom (A : Type*) [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] {p : ℕ} (h : HasMixedCharacteristic A p) :
integerLocalization A h →+* A
IsDiscreteValuationRing.absoluteRamificationIndex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/MixedCharacteristic.lean, line 93.
The absolute ramification index of a mixed-characteristic discrete valuation ring, namely the ramification index of its canonical extension
ℤ_(p) → A.
noncomputable def absoluteRamificationIndex (A : Type*) [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] {p : ℕ} (h : HasMixedCharacteristic A p) : ℕ
IsDiscreteValuationRing.hasMixedCharacteristic_iff_mixedCharZero_and_integerLocalization_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/MixedCharacteristic.lean, line 102.
For a discrete valuation ring, the residue-field formulation of mixed characteristic agrees with Mathlib's
MixedCharZero; moreover, the maximal ideal lies over(p)and the canonical map fromℤ_(p)is an injective local homomorphism whose source is a discrete valuation ring.
theorem hasMixedCharacteristic_iff_mixedCharZero_and_integerLocalization_extension
(A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (p : ℕ) :
(HasMixedCharacteristic A p ↔
0 < p ∧ CharP (IsLocalRing.ResidueField A) p ∧ MixedCharZero A p) ∧
∀ h : HasMixedCharacteristic A p,
(IsLocalRing.maximalIdeal A).under ℤ = Ideal.span {(p : ℤ)} ∧
Function.Injective (mixedCharacteristicRingHom A h) ∧
IsLocalHom (mixedCharacteristicRingHom A h) ∧
IsDiscreteValuationRing (integerLocalization A h)
Sources
Section15.116 Abhyankar's lemma and tame ramification#
Section 15.116 of the Stacks Project, Tag 0EXT. 9 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09EM, a remark
Tag 09EM in the Stacks Project.
IsDiscreteValuationRing.integralClosures_after_finite_fraction_field_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/BaseChangeClosure.lean, line 744.
The integral closures attached to a finite extension
K₁/Kand an extension of discrete valuation ringsA → Bhave the product, spectral, local, henselian, inseparable, separable, and Nagata properties listed in Stacks Project, Tag 09EM.
theorem integralClosures_after_finite_fraction_field_extension
(A : Type uA) (B : Type uB) (K : Type uK) (L : Type uL)
(K₁ : Type uK₁) (L₁ : Type uL₁) (A₁ : Type uA₁) (B₁ : Type uB₁)
[CommRing A] [CommRing B] [Field K] [Field L] [Field K₁]
[CommRing L₁] [CommRing A₁] [CommRing B₁]
[IsDomain A] [IsDomain B] [IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[Algebra A B] [IsExtension A B]
[Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L] [Algebra K K₁]
[Algebra A K₁] [Algebra K L₁] [Algebra B L₁] [Algebra L L₁] [Algebra K₁ L₁]
[Algebra A A₁] [Algebra B B₁] [Algebra A B₁] [Algebra A₁ B₁] [Algebra B₁ L₁]
[IsScalarTower A B L] [IsScalarTower A K L] [IsScalarTower A K K₁]
[IsScalarTower K L L₁] [IsScalarTower K K₁ L₁] [IsScalarTower B L L₁]
[IsScalarTower A B B₁] [IsScalarTower A A₁ B₁] [IsScalarTower B B₁ L₁]
[IsFractionRing A K] [IsFractionRing B L] [Module.Finite K K₁]
(eL₁ : L₁ ≃ₐ[K] ((L ⊗[K] K₁) ⧸ nilradical (L ⊗[K] K₁)))
(eA₁ : A₁ ≃ₐ[A] integralClosure A K₁)
(eB₁ : B₁ ≃ₐ[B] integralClosure B L₁)
(eL₁_left : ∀ x : L,
eL₁ (algebraMap L L₁ x) = Ideal.Quotient.mk _
((Algebra.TensorProduct.includeLeft : L →ₐ[K] L ⊗[K] K₁) x))
(eL₁_right : ∀ x : K₁,
eL₁ (algebraMap K₁ L₁ x) = Ideal.Quotient.mk _
((Algebra.TensorProduct.includeRight : K₁ →ₐ[K] L ⊗[K] K₁) x))
(eB₁_coe : ∀ x : B₁, ((eB₁ x : integralClosure B L₁) : L₁) = algebraMap B₁ L₁ x)
(hfieldSquare : ∀ x : K, algebraMap L L₁ (algebraMap K L x) =
algebraMap K₁ L₁ (algebraMap K K₁ x))
(hringSquare : ∀ x : A₁, algebraMap B₁ L₁ (algebraMap A₁ B₁ x) =
algebraMap K₁ L₁ ((eA₁ x : integralClosure A K₁) : K₁)) :
IsNonemptyFiniteProductOfFiniteFieldExtensions L L₁ ∧
IsDedekindDomain A₁ ∧
IsFiniteProductOfDedekindDomains B₁ ∧
(∃ π : A,
IsLocalRing.maximalIdeal A = Ideal.span {π} ∧
IsRegular (algebraMap A (B ⊗[A] A₁) π) ∧
(∃ e : Localization.Away (algebraMap A (B ⊗[A] A₁) π) ≃+* (L ⊗[K] K₁),
(∀ b : B, e (algebraMap (B ⊗[A] A₁) _
((Algebra.TensorProduct.includeLeft : B →ₐ[A] B ⊗[A] A₁) b)) =
(Algebra.TensorProduct.includeLeft : L →ₐ[K] L ⊗[K] K₁) (algebraMap B L b)) ∧
(∀ a : A₁, e (algebraMap (B ⊗[A] A₁) _
((Algebra.TensorProduct.includeRight : A₁ →ₐ[A] B ⊗[A] A₁) a)) =
(Algebra.TensorProduct.includeRight : K₁ →ₐ[K] L ⊗[K] K₁)
((eA₁ a : integralClosure A K₁) : K₁))) ∧
∃ g : (B ⊗[A] A₁) →+* B₁,
g.IsIntegral ∧ RingHom.ker g ≤ nilradical (B ⊗[A] A₁) ∧
Function.Surjective (PrimeSpectrum.comap g) ∧
(∀ b : B, g ((Algebra.TensorProduct.includeLeft : B →ₐ[A] B ⊗[A] A₁) b) =
algebraMap B B₁ b) ∧
(∀ a : A₁, g ((Algebra.TensorProduct.includeRight : A₁ →ₐ[A] B ⊗[A] A₁) a) =
algebraMap A₁ B₁ a)) ∧
Function.Surjective (PrimeSpectrum.comap (algebraMap A₁ B₁)) ∧
Finite (MaximalSpectrum A₁) ∧
Nonempty (MaximalSpectrum A₁) ∧
(∀ p : MaximalSpectrum A₁,
Finite {q : MaximalSpectrum B₁ //
q.asIdeal.comap (algebraMap A₁ B₁) = p.asIdeal} ∧
Nonempty {q : MaximalSpectrum B₁ //
q.asIdeal.comap (algebraMap A₁ B₁) = p.asIdeal}) ∧
(∀ p : Ideal A₁, p.IsMaximal →
∃ q : Ideal B₁, q.IsMaximal ∧ q.comap (algebraMap A₁ B₁) = p) ∧
(∀ q : Ideal B₁, q.IsMaximal →
(q.comap (algebraMap A₁ B₁)).IsMaximal ∧
∃ (_ : q.IsPrime) (_ : (q.comap (algebraMap A₁ B₁)).IsPrime),
(∃ _ : IsDomain (Localization (q.comap (algebraMap A₁ B₁)).primeCompl),
IsDiscreteValuationRing (Localization (q.comap (algebraMap A₁ B₁)).primeCompl)) ∧
(∃ _ : IsDomain (Localization q.primeCompl),
IsDiscreteValuationRing (Localization q.primeCompl)) ∧
∃ φ : Localization (q.comap (algebraMap A₁ B₁)).primeCompl →+*
Localization q.primeCompl,
Function.Injective φ ∧ IsLocalHom φ ∧
∀ x : A₁, φ (algebraMap A₁ _ x) = algebraMap B₁ _ (algebraMap A₁ B₁ x)) ∧
(HenselianLocalRing A → ∃ _ : IsDomain A₁, IsDiscreteValuationRing A₁) ∧
(IsAdicComplete (IsLocalRing.maximalIdeal A) A →
∃ _ : IsDomain A₁, IsDiscreteValuationRing A₁) ∧
(HenselianLocalRing B →
IsFiniteProductOfDiscreteValuationRings B₁) ∧
(IsAdicComplete (IsLocalRing.maximalIdeal B) B →
IsFiniteProductOfDiscreteValuationRings B₁) ∧
(IsPurelyInseparable K K₁ →
(∃ _ : IsDomain A₁, IsDiscreteValuationRing A₁) ∧
(∃ _ : IsDomain B₁, IsDiscreteValuationRing B₁)) ∧
(Algebra.IsSeparable K K₁ →
IsReduced (L ⊗[K] K₁) ∧
IsNonemptyFiniteProductOfFiniteSeparableFieldExtensions L L₁ ∧
Module.Finite A A₁ ∧ Module.Finite B B₁) ∧
(IsNagataRing A → Module.Finite A A₁) ∧
(IsNagataRing B → Module.Finite B B₁)
Tag 09EV, a lemma
Tag 09EV in the Stacks Project.
Stacks.KummerExtension.intermediateField_eq_adjoin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Kummer/IntermediateFields.lean, line 406. The attribute's comment: “(6)”.
If
nis prime to the residue characteristic ofA, then every intermediate fieldK ⊆ L ⊆ K_1is of the formL = K[pi^{1/d}]for some positive divisord | n:Lis generated overKby thed-th root(pi')^{n/d}ofpi, and[L : K] = dand[K_1 : L] = n / d.
theorem intermediateField_eq_adjoin [Fact (Irreducible (kummerPoly K π n))]
(hn : 2 ≤ n) (hπ : Irreducible π)
(hcop : ringChar (A ⧸ IsLocalRing.maximalIdeal A) = 0 ∨
Nat.Coprime (ringChar (A ⧸ IsLocalRing.maximalIdeal A)) n)
(L : IntermediateField K (K1 K π n)) :
∃ d : ℕ, 0 < d ∧ d ∣ n ∧
L = IntermediateField.adjoin K {(piRoot K π n) ^ (n / d)} ∧
Module.finrank K L = d ∧
Module.finrank L (K1 K π n) = n / d
Stacks.KummerExtension.isDiscreteValuationRing_A1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Kummer/Ramification.lean, line 184. The attribute's comment: “(3)”.
A_1is a discrete valuation ring.
theorem isDiscreteValuationRing_A1 [Fact (Irreducible (kummerPoly K π n))]
(hn : 2 ≤ n) (hπ : Irreducible π) :
IsDiscreteValuationRing (A1 K π n)
Stacks.KummerExtension.exists_ramificationIdx_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Kummer/Ramification.lean, line 221. The attribute's comment: “(4)”.
A_1has a unique maximal idealmlying overm_A, and the ramification index ofmoverm_Aisn.
theorem exists_ramificationIdx_eq (hn : 2 ≤ n) (hπ : Irreducible π) :
∃ m : Ideal (A1 K π n), m.IsMaximal ∧
m.LiesOver (IsLocalRing.maximalIdeal A) ∧
(∀ m' : Ideal (A1 K π n), m'.IsMaximal →
m'.LiesOver (IsLocalRing.maximalIdeal A) → m' = m) ∧
Ideal.ramificationIdx' (IsLocalRing.maximalIdeal A) m = n
Stacks.KummerExtension.isTotallyRamified_K1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Kummer/Ramification.lean, line 284. The attribute's comment: “(5)”.
K_1 / Kis totally ramified with respect toA, whatever the residue characteristic ofA.
theorem isTotallyRamified_K1 [Fact (Irreducible (kummerPoly K π n))]
(hn : 2 ≤ n) (hπ : Irreducible π) :
IsTotallyRamified A K (K1 K π n)
Stacks.KummerExtension.isTamelyRamified_K1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Kummer/Ramification.lean, line 371. The attribute's comment: “(6)”.
If
nis prime to the residue characteristic ofA, thenK_1 / Kis tamely ramified with respect toA.
theorem isTamelyRamified_K1 [Fact (Irreducible (kummerPoly K π n))]
[Algebra.IsSeparable K (K1 K π n)]
(hn : 2 ≤ n) (hπ : Irreducible π)
(hcop : ringChar (A ⧸ IsLocalRing.maximalIdeal A) = 0 ∨
Nat.Coprime (ringChar (A ⧸ IsLocalRing.maximalIdeal A)) n) :
IsTamelyRamified A K (K1 K π n)
Stacks.KummerExtension.finrank_K1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Kummer/RingOfIntegers.lean, line 396. The attribute's comment: “(1)”.
[K_1 : K] = n.
theorem finrank_K1 (hn : 2 ≤ n) (hπ : Irreducible π) :
Module.finrank K (K1 K π n) = n
Stacks.KummerExtension.integralClosure_eq_adjoin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Kummer/RingOfIntegers.lean, line 555. The attribute's comment: “(2)”.
The integral closure
A_1ofAinK_1is theA-subalgebraA[pi'] = A[pi^{1/n}]generated bypi'.
theorem integralClosure_eq_adjoin (hn : 2 ≤ n) (hπ : Irreducible π) :
(A1 K π n) = Algebra.adjoin A {piRoot K π n}
Tag 09EQ, a lemma
Tag 09EQ in the Stacks Project.
IsDiscreteValuationRing.formallySmooth_localizations_after_finite_fraction_field_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Abhyankar/FiniteFractionFieldExtension.lean, line 348.
Formal smoothness of an extension of discrete valuation rings persists at every local factor after a finite extension of the fraction field. The integral closure upstairs is the reduced tensor product, and it is the unreduced tensor product whenever
L ⊗_K K₁is reduced.
theorem formallySmooth_localizations_after_finite_fraction_field_extension
(A : Type uA) (B : Type uB) (K : Type uK) (L : Type uL)
(K₁ : Type uK₁) (L₁ : Type uL₁) (A₁ : Type uA₁) (B₁ : Type uB₁)
[CommRing A] [CommRing B] [Field K] [Field L] [Field K₁]
[CommRing L₁] [CommRing A₁] [CommRing B₁]
[IsDomain A] [IsDomain B] [IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[Algebra A B] [IsExtension A B]
[Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L] [Algebra K K₁]
[Algebra A K₁] [Algebra K L₁] [Algebra B L₁] [Algebra L L₁] [Algebra K₁ L₁]
[Algebra A A₁] [Algebra B B₁] [Algebra A B₁] [Algebra A₁ B₁] [Algebra B₁ L₁]
[IsScalarTower A B L] [IsScalarTower A K L] [IsScalarTower A K K₁]
[IsScalarTower K L L₁] [IsScalarTower K K₁ L₁] [IsScalarTower B L L₁]
[IsScalarTower A B B₁] [IsScalarTower A A₁ B₁] [IsScalarTower B B₁ L₁]
[IsFractionRing A K] [IsFractionRing B L] [Module.Finite K K₁]
(eL₁ : L₁ ≃ₐ[K] ((L ⊗[K] K₁) ⧸ nilradical (L ⊗[K] K₁)))
(eA₁ : A₁ ≃ₐ[A] integralClosure A K₁)
(eB₁ : B₁ ≃ₐ[B] integralClosure B L₁)
(eL₁_left : ∀ x : L,
eL₁ (algebraMap L L₁ x) = Ideal.Quotient.mk _
((Algebra.TensorProduct.includeLeft : L →ₐ[K] L ⊗[K] K₁) x))
(eL₁_right : ∀ x : K₁,
eL₁ (algebraMap K₁ L₁ x) = Ideal.Quotient.mk _
((Algebra.TensorProduct.includeRight : K₁ →ₐ[K] L ⊗[K] K₁) x))
(eB₁_coe : ∀ x : B₁, ((eB₁ x : integralClosure B L₁) : L₁) = algebraMap B₁ L₁ x)
(hfieldSquare : ∀ x : K, algebraMap L L₁ (algebraMap K L x) =
algebraMap K₁ L₁ (algebraMap K K₁ x))
(hringSquare : ∀ x : A₁, algebraMap B₁ L₁ (algebraMap A₁ B₁ x) =
algebraMap K₁ L₁ ((eA₁ x : integralClosure A K₁) : K₁))
(hformal : RingHom.FormallySmoothNAdic.{max uA uB} (algebraMap A B)
(IsLocalRing.maximalIdeal B)) :
(∃ eB : B₁ ≃ₐ[B] ((B ⊗[A] A₁) ⧸ nilradical (B ⊗[A] A₁)),
(∀ x : A₁, eB (algebraMap A₁ B₁ x) = Ideal.Quotient.mk _
((Algebra.TensorProduct.includeRight : A₁ →ₐ[A] B ⊗[A] A₁) x))) ∧
(IsReduced (L ⊗[K] K₁) →
(∃ eL : L₁ ≃ₐ[L] (L ⊗[K] K₁),
(∀ x : L₁, Ideal.Quotient.mk _ (eL x) = eL₁ x) ∧
(∀ x : K₁, eL (algebraMap K₁ L₁ x) =
(Algebra.TensorProduct.includeRight : K₁ →ₐ[K] L ⊗[K] K₁) x)) ∧
(∃ eB : B₁ ≃ₐ[B] (B ⊗[A] A₁),
(∀ x : A₁, eB (algebraMap A₁ B₁ x) =
(Algebra.TensorProduct.includeRight : A₁ →ₐ[A] B ⊗[A] A₁) x))) ∧
(∀ q : Ideal B₁, q.IsMaximal →
(q.comap (algebraMap A₁ B₁)).IsMaximal ∧
∃ (_ : q.IsPrime) (_ : (q.comap (algebraMap A₁ B₁)).IsPrime),
(∃ _ : IsDomain (Localization (q.comap (algebraMap A₁ B₁)).primeCompl),
IsDiscreteValuationRing
(Localization (q.comap (algebraMap A₁ B₁)).primeCompl)) ∧
(∃ _ : IsDomain (Localization q.primeCompl),
IsDiscreteValuationRing (Localization q.primeCompl)) ∧
∃ φ : Localization (q.comap (algebraMap A₁ B₁)).primeCompl →+*
Localization q.primeCompl,
Function.Injective φ ∧ IsLocalHom φ ∧
(∀ x : A₁, φ (algebraMap A₁ _ x) =
algebraMap B₁ _ (algebraMap A₁ B₁ x)) ∧
RingHom.FormallySmoothNAdic.{max uA₁ uB₁} φ
(IsLocalRing.maximalIdeal (Localization q.primeCompl)))
Tag 0BRM, a lemma
Tag 0BRM in the Stacks Project.
IsDiscreteValuationRing.formallySmooth_localizations_of_ramificationIndex_dvd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Abhyankar/AbhyankarLemma.lean, line 97.
Abhyankar's lemma. A tamely ramified extension of discrete valuation rings becomes formally smooth at every local factor after a finite fraction-field extension whose local ramification index is divisible by the original one.
theorem formallySmooth_localizations_of_ramificationIndex_dvd
(A : Type u) (B : Type v) (K : Type w) (L : Type x) (K₁ : Type y)
[CommRing A] [CommRing B] [Field K] [Field L] [Field K₁]
[IsDomain A] [IsDomain B] [IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[Algebra A B] [IsExtension A B]
[Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L] [Algebra K K₁]
[Algebra A K₁]
[IsScalarTower A B L] [IsScalarTower A K L] [IsScalarTower A K K₁]
[IsFractionRing A K] [IsFractionRing B L] [Module.Finite K K₁]
(htame : ringChar (IsLocalRing.ResidueField A) = 0 ∨
Nat.Coprime (ringChar (IsLocalRing.ResidueField A))
(ramificationIndex A B) ∧
Algebra.IsSeparableExtension (IsLocalRing.ResidueField A)
(IsLocalRing.ResidueField B)) :
∃ (n : ℕ) (E : Fin n → Type (max u v w x y))
(_ : ∀ i, Field (E i))
(_ : ∀ i, Algebra K (E i))
(_ : ∀ i, Algebra L (E i))
(_ : ∀ i, Algebra K₁ (E i))
(_ : ∀ i, Algebra B (E i))
(_ : ∀ i, IsScalarTower K L (E i))
(_ : ∀ i, IsScalarTower K K₁ (E i))
(_ : ∀ i, Module.Finite L (E i))
(decomp : ((L ⊗[K] K₁) ⧸ nilradical (L ⊗[K] K₁)) ≃ₐ[K] ∀ i, E i),
0 < n ∧
(∀ i (z : L),
decomp (Ideal.Quotient.mk _
((Algebra.TensorProduct.includeLeft : L →ₐ[K] L ⊗[K] K₁) z)) i =
algebraMap L (E i) z) ∧
(∀ i (z : K₁),
decomp (Ideal.Quotient.mk _
((Algebra.TensorProduct.includeRight : K₁ →ₐ[K] L ⊗[K] K₁) z)) i =
algebraMap K₁ (E i) z) ∧
(∀ i (z : B), algebraMap B (E i) z =
algebraMap L (E i) (algebraMap B L z)) ∧
∀ i, let A₁ := integralClosure A K₁
let B₁ := integralClosure B (E i)
∃ f : A₁ →+* B₁,
(∀ z : A₁, ((f z : B₁) : E i) =
algebraMap K₁ (E i) ((z : A₁) : K₁)) ∧
(∀ z : A, f (algebraMap A A₁ z) =
algebraMap B B₁ (algebraMap A B z)) ∧
∀ p : Ideal A₁, p.IsMaximal →
ramificationIndex A B ∣ p.ramificationIdx A →
∀ q : Ideal B₁, q.IsMaximal → q.comap f = p →
∃ (_ : q.IsPrime) (_ : p.IsPrime),
(∃ _ : IsDomain (Localization p.primeCompl),
IsDiscreteValuationRing (Localization p.primeCompl)) ∧
(∃ _ : IsDomain (Localization q.primeCompl),
IsDiscreteValuationRing (Localization q.primeCompl)) ∧
∃ φ : Localization p.primeCompl →+* Localization q.primeCompl,
Function.Injective φ ∧ IsLocalHom φ ∧
(∀ z : A₁, φ (algebraMap A₁ _ z) =
algebraMap B₁ _ (f z)) ∧
RingHom.FormallySmoothNAdic φ
(IsLocalRing.maximalIdeal (Localization q.primeCompl))
Tag 0EXU, a lemma
Tag 0EXU in the Stacks Project.
IsDiscreteValuationRing.isTamelyRamified_tower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/TameRamification.lean, line 307.
Tame ramification composes in a tower of finite separable extensions when the upper extension is tamely ramified at every maximal localization of the intermediate integral closure.
theorem isTamelyRamified_tower
(A : Type u) (K : Type v) (L : Type w) (M : Type x)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Field L] [Field M]
[Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M]
[Algebra A L] [IsScalarTower A K L]
[Algebra A M] [IsScalarTower A K M] [IsScalarTower A L M]
[Module.Finite K L] [Algebra.IsSeparable K L]
[Module.Finite L M] [Algebra.IsSeparable L M]
(hLK : Stacks.KummerExtension.IsTamelyRamified A K L)
(hML : ∀ (m : Ideal (integralClosure A L)) (hm : m.IsMaximal),
letI : m.IsPrime := hm.isPrime
letI : IsFractionRing (integralClosure A L) L :=
integralClosure.isFractionRing_of_finite_extension K L
letI : Algebra (Localization.AtPrime m) L :=
IsLocalization.localizationAlgebraOfSubmonoidLe _ _ m.primeCompl
(nonZeroDivisors (integralClosure A L)) m.primeCompl_le_nonZeroDivisors
letI : Algebra (Localization.AtPrime m) M :=
((algebraMap L M).comp (algebraMap (Localization.AtPrime m) L)).toAlgebra
letI : IsScalarTower (Localization.AtPrime m) L M :=
IsScalarTower.of_algebraMap_eq fun _ => rfl
Stacks.KummerExtension.IsTamelyRamified (Localization.AtPrime m) L M) :
letI : Module.Finite K M := Module.Finite.trans L M
letI : Algebra.IsSeparable K M := Algebra.IsSeparable.trans K L M
Stacks.KummerExtension.IsTamelyRamified A K M
Tag 0EXV, a lemma
Tag 0EXV in the Stacks Project.
IsDiscreteValuationRing.isTamelyRamified_of_isTamelyRamified_tower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/TameRamification.lean, line 398. References: SGA 1 XIII (2.0.3), “subalgebra of tame”.
Every intermediate extension of a finite separable extension tamely ramified with respect to a discrete valuation ring is itself tamely ramified.
theorem isTamelyRamified_of_isTamelyRamified_tower
(A : Type u) (K : Type v) (L : Type w) (M : Type x)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Field L] [Field M]
[Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M]
[Algebra A L] [IsScalarTower A K L]
[Algebra A M] [IsScalarTower A K M] [IsScalarTower A L M]
[Module.Finite K L] [Algebra.IsSeparable K L]
[Module.Finite L M] [Algebra.IsSeparable L M]
(hM : letI : Module.Finite K M := Module.Finite.trans L M
letI : Algebra.IsSeparable K M := Algebra.IsSeparable.trans K L M
Stacks.KummerExtension.IsTamelyRamified A K M) :
Stacks.KummerExtension.IsTamelyRamified A K L
Tag 0EXW, a lemma
Tag 0EXW in the Stacks Project.
IsDiscreteValuationRing.isTamelyRamifiedWithRespectTo_tfae_hasUnramifiedKummerOverfield, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Abhyankar/TameRamificationKummer.lean, line 764.
A finite separable extension of the fraction field of a discrete valuation ring is tamely ramified if and only if it embeds into an unramified extension after some Kummer base change; equivalently, such an unramified overfield exists after every prime-to-residue-characteristic multiple of one fixed exponent.
theorem isTamelyRamifiedWithRespectTo_tfae_hasUnramifiedKummerOverfield
(A : Type u) (K : Type v) (L : Type w)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Field L]
[Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L]
[FiniteDimensional K L] [Algebra.IsSeparable K L]
(π : A) (hπ : Irreducible π) :
List.TFAE
[ IsTamelyRamifiedWithRespectTo A K L,
∃ e : ℕ, HasUnramifiedKummerOverfield A K L π hπ e,
∃ e₀ : ℕ, 1 ≤ e₀ ∧ IsUnit (e₀ : IsLocalRing.ResidueField A) ∧
∀ d : ℕ, 1 ≤ d → IsUnit (d : IsLocalRing.ResidueField A) →
HasUnramifiedKummerOverfield A K L π hπ (d * e₀) ]
Tag 0EXX, a lemma
Tag 0EXX in the Stacks Project.
IsDiscreteValuationRing.exists_isGalois_and_common_extension_isTamelyRamifiedWithRespectTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Abhyankar/TameGaloisClosure.lean, line 249.
Stacks 0EXX. Every finite separable extension of the fraction field of a discrete valuation ring which is tamely ramified with respect to the ring is contained in a finite Galois extension with the same property. Any two such extensions are contained in a common finite separable extension which is again tamely ramified.
theorem exists_isGalois_and_common_extension_isTamelyRamifiedWithRespectTo
(A : Type u) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(K : Type v) [Field K] [Algebra A K] [IsFractionRing A K] :
(∀ (L : Type w) [Field L] [Algebra K L] [FiniteDimensional K L]
[Algebra.IsSeparable K L] [Algebra A L] [IsScalarTower A K L],
IsTamelyRamifiedWithRespectTo A K L →
∃ (M : Type (max u v w)) (_ : Field M) (_ : Algebra K M)
(_ : FiniteDimensional K M) (_ : Algebra.IsSeparable K M)
(_ : Algebra A M) (_ : IsScalarTower A K M)
(_ : Algebra L M) (_ : IsScalarTower K L M),
IsGalois K M ∧ IsTamelyRamifiedWithRespectTo A K M) ∧
(∀ (L₁ : Type w) [Field L₁] [Algebra K L₁] [FiniteDimensional K L₁]
[Algebra.IsSeparable K L₁] [Algebra A L₁] [IsScalarTower A K L₁]
(L₂ : Type x) [Field L₂] [Algebra K L₂] [FiniteDimensional K L₂]
[Algebra.IsSeparable K L₂] [Algebra A L₂] [IsScalarTower A K L₂],
IsTamelyRamifiedWithRespectTo A K L₁ →
IsTamelyRamifiedWithRespectTo A K L₂ →
∃ (L : Type (max u v w x)) (_ : Field L) (_ : Algebra K L)
(_ : FiniteDimensional K L) (_ : Algebra.IsSeparable K L)
(_ : Algebra A L) (_ : IsScalarTower A K L)
(_ : Algebra L₁ L) (_ : IsScalarTower K L₁ L)
(_ : Algebra L₂ L) (_ : IsScalarTower K L₂ L),
IsTamelyRamifiedWithRespectTo A K L)
Tag 0EXY, a lemma
Tag 0EXY in the Stacks Project.
IsDiscreteValuationRing.exists_algEquiv_pi_field_and_ramification_goes_up, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Abhyankar/RamificationGoesUp.lean, line 783. References: SGA 1 XIII (2.0.3), “tame after DVR extension”; SGA 1 XIII (2.0.2), “⇒: tameness ascends”.
Stacks 0EXY. A finite separable field extension remains a finite product of fields after scalar extension along an extension of discrete valuation rings. If the original extension is unramified, respectively tamely ramified, then every resulting field factor has the same property over the larger discrete valuation ring.
theorem exists_algEquiv_pi_field_and_ramification_goes_up
(A : Type u) (B : Type v) (K : Type w) (L : Type x) (K' : Type y)
[CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
[IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[Field K] [Field L] [Field K']
[Algebra A B] [IsExtension A B]
[Algebra A K] [IsFractionRing A K]
[Algebra B L] [IsFractionRing B L]
[Algebra K L] [Algebra A L]
[IsScalarTower A B L] [IsScalarTower A K L]
[Algebra K K'] [Algebra A K'] [IsScalarTower A K K']
[Module.Finite K K'] [Algebra.IsSeparable K K'] :
∃ (n : ℕ) (E : Fin n → Type (max u v w x y))
(_ : ∀ i, Field (E i))
(_ : ∀ i, Algebra L (E i))
(_ : ∀ i, Algebra B (E i))
(_ : ∀ i, IsScalarTower B L (E i))
(_ : ∀ i, Module.Finite L (E i))
(_ : ∀ i, Algebra.IsSeparable L (E i)),
0 < n ∧
Nonempty ((L ⊗[K] K') ≃ₐ[L] ∀ i, E i) ∧
(IsUnramifiedWithRespectTo A K K' →
∀ i, IsUnramifiedWithRespectTo B L (E i)) ∧
(IsTamelyRamifiedWithRespectTo A K K' →
∀ i, IsTamelyRamifiedWithRespectTo B L (E i))
Sources
Section15.117 Eliminating ramification#
Section 15.117 of the Stacks Project, Tag 09EL. 19 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09EN, a definition
Tag 09EN in the Stacks Project.
IsDiscreteValuationRing.IntegralClosureBaseChange.IsWeakSolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Solution.lean, line 144. The attribute's comment: “(1), weak solution”.
Every localization arising from the base change has ramification index one.
def IsWeakSolution
{A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
{K₁ : Type uK₁}
[CommRing A] [CommRing B] [Field K] [Field L] [Field K₁]
[IsDomain A] [IsDomain B] [IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L]
[Algebra K L] [Algebra K K₁] [Algebra A K₁]
[IsExtension A B] [IsFractionRing A K] [IsFractionRing B L]
[IsScalarTower A B L] [IsScalarTower A K L] [IsScalarTower A K K₁]
[Module.Finite K K₁]
(D : IntegralClosureBaseChange A B K L K₁) : Prop
IsDiscreteValuationRing.IntegralClosureBaseChange.IsSolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Solution.lean, line 163. The attribute's comment: “(2), solution”.
Every localization arising from the base change is formally smooth for the adic topology defined by the maximal ideal of the target localization.
def IsSolution.{v}
{A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
{K₁ : Type uK₁}
[CommRing A] [CommRing B] [Field K] [Field L] [Field K₁]
[IsDomain A] [IsDomain B] [IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L]
[Algebra K L] [Algebra K K₁] [Algebra A K₁]
[IsExtension A B] [IsFractionRing A K] [IsFractionRing B L]
[IsScalarTower A B L] [IsScalarTower A K L] [IsScalarTower A K K₁]
[Module.Finite K K₁]
(D : IntegralClosureBaseChange.{uA, uB, uK, uL, uK₁, uL₁, uA₁, uB₁}
A B K L K₁) : Prop
IsDiscreteValuationRing.IntegralClosureBaseChange.IsSeparableSolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Solution.lean, line 188. The attribute's comment: “separable solution”.
A solution whose finite extension
K₁/Kis separable.
def IsSeparableSolution.{v}
{A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
{K₁ : Type uK₁}
[CommRing A] [CommRing B] [Field K] [Field L] [Field K₁]
[IsDomain A] [IsDomain B] [IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L]
[Algebra K L] [Algebra K K₁] [Algebra A K₁]
[IsExtension A B] [IsFractionRing A K] [IsFractionRing B L]
[IsScalarTower A B L] [IsScalarTower A K L] [IsScalarTower A K K₁]
[Module.Finite K K₁]
(D : IntegralClosureBaseChange.{uA, uB, uK, uL, uK₁, uL₁, uA₁, uB₁}
A B K L K₁) : Prop
Tag 09EP, an example
Tag 09EP in the Stacks Project.
IsDiscreteValuationRing.weakSolution_isInseparable_and_inseparable_isSolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/WeakSolution/Inseparability.lean, line 925.
For
k[[x]] → k[[x^(1/p)]]in positive characteristicp, every weak solution is inseparable, while every finite inseparable extension ofk((x))is a solution.
theorem weakSolution_isInseparable_and_inseparable_isSolution
(p : ℕ) [Fact p.Prime]
(k : Type uk) (A : Type uA) (B : Type uB) (K : Type uK) (L : Type uL)
[Field k] [PerfectField k] [CharP k p]
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[Field K] [Field L]
[Algebra k A] [Algebra k B] [Algebra k K] [Algebra k L]
[Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L]
[IsScalarTower k A B] [IsScalarTower k A K] [IsScalarTower k B L]
[IsScalarTower k K L] [IsScalarTower A B L] [IsScalarTower A K L]
[IsExtension A B] [IsFractionRing A K] [IsFractionRing B L]
(eA : A ≃ₐ[k] PowerSeries k) (eB : B ≃ₐ[k] PowerSeries k)
(eK : K ≃ₐ[k] LaurentSeries k) (eL : L ≃ₐ[k] LaurentSeries k)
(hAB : ∀ a : A, eB (algebraMap A B a) =
PowerSeries.subst (PowerSeries.X ^ p) (eA a))
(_hAK : ∀ a : A, eK (algebraMap A K a) = (eA a : LaurentSeries k))
(_hBL : ∀ b : B, eL (algebraMap B L b) = (eB b : LaurentSeries k)) :
(∀ (K₁ : Type uK₁) [Field K₁] [Algebra K K₁] [Algebra A K₁]
[IsScalarTower A K K₁] [Module.Finite K K₁]
(D : IntegralClosureBaseChange.{uA, uB, uK, uL, uK₁, uL₁, uA₁, uB₁}
A B K L K₁),
D.IsWeakSolution → ¬ Algebra.IsSeparable K K₁) ∧
∀ (K₁ : Type uK₁) [Field K₁] [Algebra K K₁] [Algebra A K₁]
[IsScalarTower A K K₁] [Module.Finite K K₁],
¬ Algebra.IsSeparable K K₁ →
∃ D : IntegralClosureBaseChange.{uA, uB, uK, uL, uK₁,
max uL uK₁, uK₁, max uL uK₁} A B K L K₁,
D.IsSolution.{uA, uB, uK, uL, uK₁, max uL uK₁, uK₁, max uL uK₁, v}
Tag 09ER, a lemma
Tag 09ER in the Stacks Project.
IsDiscreteValuationRing.isField_tensorProduct_and_isDVR_baseChange_of_totallyRamified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/WeakSolution/TotallyRamified.lean, line 273.
A finite separable extension totally ramified with respect to the lower discrete valuation ring preserves a weakly unramified extension after tensor-product base change. The tensor product is canonically the integral closure in the base-changed fraction field.
theorem isField_tensorProduct_and_isDVR_baseChange_of_totallyRamified
(A : Type uA) (B : Type uB) (K : Type uK) (L : Type uL) (K₁ : Type uK₁)
[CommRing A] [CommRing B] [Field K] [Field L] [Field K₁]
[IsDomain A] [IsDomain B] [IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[Algebra A B] [FaithfulSMul A B] [IsLocalHom (algebraMap A B)]
[Algebra A K] [Algebra B L] [Algebra A L] [Algebra K L]
[IsScalarTower A B L] [IsScalarTower A K L]
[IsFractionRing A K] [IsFractionRing B L]
[Algebra K K₁] [Algebra A K₁] [IsScalarTower A K K₁]
[FiniteDimensional K K₁] [Algebra.IsSeparable K K₁]
(hweak : Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A) =
IsLocalRing.maximalIdeal B)
(htot : IsTotallyRamifiedWithRespectTo A K K₁) :
let A₁ := integralClosure A K₁
let B₁ := B ⊗[A] A₁
let L₁ := L ⊗[K] K₁
let C₁ := integralClosure B L₁
∃ hL₁ : IsField L₁,
letI := hL₁.toField
∃ hA₁ : IsDiscreteValuationRing A₁,
letI := hA₁
∃ hBdom : IsDomain B₁,
letI := hBdom
∃ hB₁ : IsDiscreteValuationRing B₁,
letI := hB₁
let f : A₁ →+* B₁ := Algebra.TensorProduct.includeRight.toRingHom
Function.Injective f ∧
Ideal.map f (IsLocalRing.maximalIdeal A₁) = IsLocalRing.maximalIdeal B₁ ∧
∃ hCdom : IsDomain C₁,
letI := hCdom
∃ hC₁ : IsDiscreteValuationRing C₁,
letI := hC₁
∃ _ : IsFractionRing C₁ L₁,
∃ e : B₁ ≃ₐ[B] C₁,
(∀ a : A₁,
((e ((Algebra.TensorProduct.includeRight : A₁ →ₐ[A] B₁) a) : C₁)
: L₁) =
(Algebra.TensorProduct.includeRight : K₁ →ₐ[K] L₁) (a : K₁)) ∧
let f' : A₁ →+* C₁ :=
e.toRingHom.comp Algebra.TensorProduct.includeRight.toRingHom
Function.Injective f' ∧
Ideal.map f' (IsLocalRing.maximalIdeal A₁) =
IsLocalRing.maximalIdeal C₁
Tag 09ES, a lemma
Tag 09ES in the Stacks Project.
IsDiscreteValuationRing.weakSolutions_and_solutions_go_down_and_compose, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/EppSolution.lean, line 1213.
Weak solutions and solutions descend along a tower of extensions of discrete valuation rings. Conversely, they compose provided every field factor of the intermediate reduced tensor product is respectively a weak solution or a solution for the upper extension.
theorem weakSolutions_and_solutions_go_down_and_compose
(A : Type uA) (B : Type uB) (C : Type uC)
(K : Type uK) (L : Type uL) (M : Type uM) (K₁ : Type uK₁)
[CommRing A] [CommRing B] [CommRing C]
[IsDomain A] [IsDomain B] [IsDomain C]
[IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[IsDiscreteValuationRing C]
[Field K] [Field L] [Field M] [Field K₁]
[Algebra A B] [Algebra B C] [Algebra A C]
[Algebra A K] [Algebra A L] [Algebra A M]
[Algebra B L] [Algebra B M] [Algebra C M]
[Algebra K L] [Algebra K M] [Algebra L M]
[Algebra K K₁] [Algebra A K₁]
[IsExtension A B] [IsExtension B C]
[IsExtension A C]
[IsFractionRing A K] [IsFractionRing B L] [IsFractionRing C M]
[IsScalarTower A B C] [IsScalarTower A B L] [IsScalarTower A B M]
[IsScalarTower B C M] [IsScalarTower A C M]
[IsScalarTower A K L] [IsScalarTower A K M] [IsScalarTower K L M]
[IsScalarTower B L M] [IsScalarTower A K K₁] [Module.Finite K K₁]
(DAB : IntegralClosureBaseChange.{uA, uB, uK, uL, uK₁, uL₁, uA₁, uB₁}
A B K L K₁)
(DAC : IntegralClosureBaseChange.{uA, uC, uK, uM, uK₁, uM₁, uA₂, uC₁}
A C K M K₁) :
letI := DAB.commRingL₁
letI := DAB.algebraLL₁
((DAC.IsWeakSolution → DAB.IsWeakSolution) ∧
(DAC.IsSolution.{uA, uC, uK, uM, uK₁, uM₁, uA₂, uC₁, max uA₂ uC₁} →
DAB.IsSolution.{uA, uB, uK, uL, uK₁, uL₁, uA₁, uB₁, max uA₁ uB₁})) ∧
∀ (n : ℕ) (E : Fin n → Type uE)
[∀ i, Field (E i)] [∀ i, Algebra L (E i)] [∀ i, Algebra B (E i)]
[∀ i, IsScalarTower B L (E i)] [∀ i, Module.Finite L (E i)],
0 < n → Nonempty (DAB.L₁ ≃ₐ[L] ∀ i, E i) →
∀ DBC : ∀ i, IntegralClosureBaseChange.{uB, uC, uL, uM, uE, uN₁, uB₂, uC₂}
B C L M (E i),
((DAB.IsWeakSolution ∧ ∀ i, (DBC i).IsWeakSolution) →
DAC.IsWeakSolution) ∧
((DAB.IsSolution.{uA, uB, uK, uL, uK₁, uL₁, uA₁, uB₁, max uA₁ uB₁} ∧
∀ i, (DBC i).IsSolution.{uB, uC, uL, uM, uE, uN₁, uB₂, uC₂, max uB₂ uC₂}) →
DAC.IsSolution.{uA, uC, uK, uM, uK₁, uM₁, uA₂, uC₁, max uA₂ uC₁})
Tag 09EU, a lemma
Tag 09EU in the Stacks Project.
IsDiscreteValuationRing.normal_extension_acts_transitively_on_maximalSpectrum_integralClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/WeakSolution/GaloisAction.lean, line 397.
After a finite normal extension
K₁/K, the automorphisms ofK₁overKact compatibly on the reduced base changeL₁, on the integral closureA₁ofAinK₁, and on the integral closureB₁ofBinL₁. The resulting action on the maximal ideals ofB₁is transitive.
theorem normal_extension_acts_transitively_on_maximalSpectrum_integralClosure
(A B K L K₁ L₁ A₁ B₁ : Type u)
[CommRing A] [CommRing B] [Field K] [Field L] [Field K₁]
[CommRing L₁] [CommRing A₁] [CommRing B₁]
[IsDomain A] [IsDomain B] [IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[Algebra A B] [FaithfulSMul A B] [IsLocalHom (algebraMap A B)]
[Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L] [Algebra K K₁]
[Algebra A K₁] [Algebra K L₁] [Algebra B L₁] [Algebra L L₁] [Algebra K₁ L₁]
[Algebra A A₁] [Algebra B B₁] [Algebra A B₁] [Algebra A₁ B₁] [Algebra B₁ L₁]
[IsScalarTower A B L] [IsScalarTower A K L] [IsScalarTower A K K₁]
[IsScalarTower K L L₁] [IsScalarTower K K₁ L₁] [IsScalarTower B L L₁]
[IsScalarTower A B B₁] [IsScalarTower A A₁ B₁] [IsScalarTower B B₁ L₁]
[IsFractionRing A K] [IsFractionRing B L] [Module.Finite K K₁] [Normal K K₁]
(eL₁ : L₁ ≃ₐ[K] ((L ⊗[K] K₁) ⧸ nilradical (L ⊗[K] K₁)))
(eA₁ : A₁ ≃ₐ[A] integralClosure A K₁)
(eB₁ : B₁ ≃ₐ[B] integralClosure B L₁)
(eL₁_left : ∀ x : L,
eL₁ (algebraMap L L₁ x) = Ideal.Quotient.mk _
((Algebra.TensorProduct.includeLeft : L →ₐ[K] L ⊗[K] K₁) x))
(eL₁_right : ∀ x : K₁,
eL₁ (algebraMap K₁ L₁ x) = Ideal.Quotient.mk _
((Algebra.TensorProduct.includeRight : K₁ →ₐ[K] L ⊗[K] K₁) x))
(eB₁_coe : ∀ x : B₁, ((eB₁ x : integralClosure B L₁) : L₁) = algebraMap B₁ L₁ x)
(_hfieldSquare : ∀ x : K, algebraMap L L₁ (algebraMap K L x) =
algebraMap K₁ L₁ (algebraMap K K₁ x))
(hringSquare : ∀ x : A₁, algebraMap B₁ L₁ (algebraMap A₁ B₁ x) =
algebraMap K₁ L₁ ((eA₁ x : integralClosure A K₁) : K₁)) :
∃ (ρL₁ : (K₁ ≃ₐ[K] K₁) →* (L₁ ≃ₐ[L] L₁))
(ρA₁ : (K₁ ≃ₐ[K] K₁) →* (A₁ ≃ₐ[A] A₁))
(ρB₁ : (K₁ ≃ₐ[K] K₁) →* (B₁ ≃ₐ[B] B₁)),
(∀ (g : K₁ ≃ₐ[K] K₁) (x : K₁),
ρL₁ g (algebraMap K₁ L₁ x) = algebraMap K₁ L₁ (g x)) ∧
(∀ (g : K₁ ≃ₐ[K] K₁) (x : A₁),
(((eA₁ (ρA₁ g x) : integralClosure A K₁) : K₁)) =
g ((eA₁ x : integralClosure A K₁) : K₁)) ∧
(∀ (g : K₁ ≃ₐ[K] K₁) (x : B₁),
algebraMap B₁ L₁ (ρB₁ g x) = ρL₁ g (algebraMap B₁ L₁ x)) ∧
(∀ (g : K₁ ≃ₐ[K] K₁) (x : A₁),
ρB₁ g (algebraMap A₁ B₁ x) = algebraMap A₁ B₁ (ρA₁ g x)) ∧
∀ q q' : MaximalSpectrum B₁, ∃ g : K₁ ≃ₐ[K] K₁,
q'.asIdeal = q.asIdeal.comap (ρB₁ g).symm.toRingHom
Tag 09EW, a lemma
Tag 09EW in the Stacks Project.
Stacks.EisensteinExtension.exists_totallyRamifiedExtension_with_uniformizer_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Kummer/Eisenstein.lean, line 636.
Let
Abe a discrete valuation ring with fraction fieldKand residue characteristicp > 0, with uniformizerπ, and letn > 1. For every powerqofpthere is a separable extensionL / Kof degreeq, totally ramified with respect toAwith ramification indexq, whose integral closureBofAis a discrete valuation ring with a uniformizerπ_Bsatisfyingπ_B^q = π + π^n bandπ_B^q = π + π_B^{nq} b'for someb, b'inB.
theorem exists_totallyRamifiedExtension_with_uniformizer_eq
(A : Type u) (K : Type v) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Algebra A K] [IsFractionRing A K]
(π : A) (hπ : Irreducible π) (p n q : ℕ)
(hp : 0 < p)
(_hres : ringChar (A ⧸ IsLocalRing.maximalIdeal A) = p)
(hn : 1 < n) (hq : ∃ r : ℕ, q = p ^ r) :
∃ (L : Type v) (_ : Field L) (_ : Algebra K L) (_ : Algebra A L)
(_ : IsScalarTower A K L) (_ : Module.Finite K L)
(_ : Algebra.IsSeparable K L)
(_ : IsDiscreteValuationRing (integralClosure A L)),
Module.finrank K L = q ∧
Stacks.KummerExtension.IsTotallyRamified A K L ∧
Ideal.ramificationIdx' (IsLocalRing.maximalIdeal A)
(IsLocalRing.maximalIdeal (integralClosure A L)) = q ∧
∃ πB b b' : integralClosure A L,
Irreducible πB ∧
πB ^ q = algebraMap A (integralClosure A L) π +
(algebraMap A (integralClosure A L) π) ^ n * b ∧
πB ^ q = algebraMap A (integralClosure A L) π + πB ^ (n * q) * b'
Tag 09EX, a lemma
Tag 09EX in the Stacks Project.
Stacks.DiscreteValuationRing.AdjoinPthRoot.statement1_not_pth_power, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/AdjoinPthRoot.lean, line 184. The attribute's comment: “(1)”.
If the residue class
abarofais not ap-th power in the residue fieldkappa_A, thenais not ap-th power inK.
theorem statement1_not_pth_power
(ha : ¬ ∃ b : IsLocalRing.ResidueField A, IsLocalRing.residue A a = b ^ p) :
¬ ∃ b : K, algebraMap A K a = b ^ p
Stacks.DiscreteValuationRing.AdjoinPthRoot.statement2_integralClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/AdjoinPthRoot.lean, line 451. The attribute's comment: “(2)”.
The integral closure of
AinK[a^{1/p}]equalsA[a^{1/p}] = A[alpha].
theorem statement2_integralClosure
(ha : ¬ ∃ b : IsLocalRing.ResidueField A, IsLocalRing.residue A a = b ^ p) :
integralClosure A (FieldExt (A := A) (K := K) p a)
= ringExt (A := A) (K := K) p a
Stacks.DiscreteValuationRing.AdjoinPthRoot.statement3_dvr_weaklyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/AdjoinPthRoot.lean, line 480. The attribute's comment: “(3)”.
The ring
A[a^{1/p}] = A[alpha]is a discrete valuation ring, and the extensionA ⊆ A[a^{1/p}]is weakly unramified: every uniformizer (irreducible element) ofAmaps to a uniformizer (irreducible element) ofA[a^{1/p}].
theorem statement3_dvr_weaklyUnramified
(ha : ¬ ∃ b : IsLocalRing.ResidueField A, IsLocalRing.residue A a = b ^ p) :
haveI : Fact (Irreducible (polyK (A := A) (K := K) p a)) :=
⟨statement1_irreducible p a ha⟩
letI B := ringExt (A := A) (K := K) p a
haveI : IsDomain B := inferInstance
IsDiscreteValuationRing B
∧ (∀ ϖ : A, Irreducible ϖ → Irreducible (algebraMap A B ϖ))
Tag 09EY, a lemma
Tag 09EY in the Stacks Project.
IsDiscreteValuationRing.weaklyUnramified_or_adjoin_root_or_after_totallyRamified_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/PurelyInseparable.lean, line 900.
For a weakly unramified extension
A → Bof discrete valuation rings withBNagata, followed by a purely inseparable extension of fraction fields of prime degreep, either the composite extension is weakly unramified, the upper DVR is generated by ap-th root of a uniformizer ofA, or a separable totally ramified degree-pbase change makes both maps between the resulting integral closures weakly unramified.
theorem weaklyUnramified_or_adjoin_root_or_after_totallyRamified_baseChange
(A B C K L M : Type u)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
[Field K] [Field L] [Field M]
[Algebra A B] [Algebra B C] [Algebra A C]
[FaithfulSMul A B] [FaithfulSMul B C]
[IsScalarTower A B C]
[IsLocalHom (algebraMap A B)] [IsLocalHom (algebraMap B C)]
[Algebra A K] [Algebra B L] [Algebra C M]
[Algebra A L] [Algebra A M] [Algebra B M]
[Algebra K L] [Algebra K M] [Algebra L M]
[IsScalarTower A B L] [IsScalarTower B C M]
[IsScalarTower A C M] [IsScalarTower B L M]
[IsScalarTower A K L] [IsScalarTower K L M]
[IsScalarTower A B M] [IsScalarTower A K M]
[IsFractionRing A K] [IsFractionRing B L] [IsFractionRing C M]
(p : ℕ) [Fact p.Prime] [FiniteDimensional L M] [IsPurelyInseparable L M]
(hdegree : Module.finrank L M = p)
(π : A) (hπ : Irreducible π)
(hNagata : IsNagataRing B)
(hweak : Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A) =
IsLocalRing.maximalIdeal B) :
Ideal.map (algebraMap A C) (IsLocalRing.maximalIdeal A) =
IsLocalRing.maximalIdeal C ∨
(∃ x : C, x ^ p = algebraMap A C π ∧ Algebra.adjoin B {x} = ⊤) ∨
∃ (K₁ : Type u) (_ : Field K₁) (_ : Algebra K K₁) (_ : Algebra A K₁)
(_ : IsScalarTower A K K₁) (_ : FiniteDimensional K K₁)
(_ : Algebra.IsSeparable K K₁),
Module.finrank K K₁ = p ∧
IsDiscreteValuationRing.IsTotallyRamifiedWithRespectTo A K K₁ ∧
let L₁ := L ⊗[K] K₁
let M₁ := M ⊗[K] K₁
let A₁ := integralClosure A K₁
let B₁ := integralClosure B L₁
let C₁ := integralClosure C M₁
IsField L₁ ∧ IsField M₁ ∧
∃ hA₁ : IsDiscreteValuationRing A₁,
letI := hA₁
∃ hB₁dom : IsDomain B₁,
letI := hB₁dom
∃ hB₁ : IsDiscreteValuationRing B₁,
letI := hB₁
∃ hC₁dom : IsDomain C₁,
letI := hC₁dom
∃ hC₁ : IsDiscreteValuationRing C₁,
letI := hC₁
∃ (g : L₁ →+* M₁) (f : A₁ →+* B₁) (f' : B₁ →+* C₁),
Function.Injective f ∧ Function.Injective f' ∧
(∀ l : L, g
((Algebra.TensorProduct.includeLeft : L →ₐ[K] L₁) l) =
(Algebra.TensorProduct.includeLeft : M →ₐ[K] M₁)
(algebraMap L M l)) ∧
(∀ k : K₁, g
((Algebra.TensorProduct.includeRight : K₁ →ₐ[K] L₁) k) =
(Algebra.TensorProduct.includeRight : K₁ →ₐ[K] M₁) k) ∧
(∀ a : A₁, ((f a : B₁) : L₁) =
(Algebra.TensorProduct.includeRight : K₁ →ₐ[K] L₁) (a : K₁)) ∧
(∀ b : B₁, ((f' b : C₁) : M₁) = g (b : L₁)) ∧
Ideal.map f (IsLocalRing.maximalIdeal A₁) =
IsLocalRing.maximalIdeal B₁ ∧
Ideal.map f' (IsLocalRing.maximalIdeal B₁) =
IsLocalRing.maximalIdeal C₁
Tag 09EZ, a lemma
Tag 09EZ in the Stacks Project.
IsLocalRing.exists_residueField_section_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalRing/ResidueSection.lean, line 51.
A local ring of prime characteristic with nilpotent maximal ideal has a coefficient field, and it can be extended compatibly across a local homomorphism whose target also has nilpotent maximal ideal and whose residue field extension is separable.
theorem exists_residueField_section_compatible
{p : ℕ} [Fact p.Prime]
(A : Type u) [CommRing A] [IsLocalRing A] [CharP A p]
(hA : IsNilpotent (IsLocalRing.maximalIdeal A)) :
∃ σ : IsLocalRing.ResidueField A →+* A,
(IsLocalRing.residue A).comp σ = RingHom.id _ ∧
∀ (A' : Type v) [CommRing A'] [IsLocalRing A'] [Algebra A A']
[IsLocalHom (algebraMap A A')],
IsNilpotent (IsLocalRing.maximalIdeal A') →
Algebra.IsSeparableExtension (IsLocalRing.ResidueField A)
(IsLocalRing.ResidueField A') →
∃ σ' : IsLocalRing.ResidueField A' →+* A',
(IsLocalRing.residue A').comp σ' = RingHom.id _ ∧
(algebraMap A A').comp σ =
σ'.comp (algebraMap (IsLocalRing.ResidueField A)
(IsLocalRing.ResidueField A'))
Tag 09F0, a lemma
Tag 09F0 in the Stacks Project.
IsDiscreteValuationRing.isGalois_and_ramification_cases_of_adjoin_root_artinSchreier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/ArtinSchreier/RamificationCases.lean, line 689.
Let
Abe a discrete valuation ring with fraction fieldKof characteristicp > 0. IfL = K[z]andz ^ p - z = ξ, thenL / Kis Galois and is either trivial, unramified of degreep, totally ramified of ramification indexp, or weakly unramified with purely inseparable residue extension of degreep.Moreover, for a uniformizer
πofA, an integralξgives one of the first two cases; a pole of order prime topgives the totally ramified case; and a pole whose positive order is divisible bypand whose leading coefficient is not ap-th power in the residue field gives the weakly unramified, residually inseparable case.
theorem isGalois_and_ramification_cases_of_adjoin_root_artinSchreier
(A : Type uA) (K : Type uK) (L : Type uL)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Algebra A K] [IsFractionRing A K]
[Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
(p : ℕ) (hp : p.Prime) [CharP K p]
(ξ : K) (z : L)
(hz : z ^ p - z = algebraMap K L ξ)
(hgen : Algebra.adjoin K {z} = ⊤)
(π : A) (hπ : Irreducible π) :
∃ hfin : Module.Finite K L,
letI := hfin
let B := integralClosure A L
let mA := IsLocalRing.maximalIdeal A
let trivial : Prop := Function.Surjective (algebraMap K L)
let unramified : Prop :=
Module.finrank K L = p ∧
∀ m : Ideal B, m.IsMaximal → ∃ _ : m.LiesOver mA,
Ideal.ramificationIdx' mA m = 1 ∧
@Algebra.IsSeparable (A ⧸ mA) (B ⧸ m) _ _
(Ideal.Quotient.algebraOfLiesOver m mA)
let totallyRamified : Prop :=
Stacks.KummerExtension.IsTotallyRamified A K L ∧
∀ m : Ideal B, m.IsMaximal → m.LiesOver mA →
Ideal.ramificationIdx' mA m = p
let residuallyInseparable : Prop :=
∃ hDVR : IsDiscreteValuationRing B,
letI := hDVR
let mB := IsLocalRing.maximalIdeal B
∃ _ : mB.LiesOver mA,
Ideal.ramificationIdx' mA mB = 1 ∧
letI := Ideal.Quotient.algebraOfLiesOver mB mA
IsPurelyInseparable (A ⧸ mA) (B ⧸ mB) ∧
Module.finrank (A ⧸ mA) (B ⧸ mB) = p
IsGalois K L ∧
(trivial ∨ unramified ∨ totallyRamified ∨ residuallyInseparable) ∧
((∃ a : A, ξ = algebraMap A K a) → trivial ∨ unramified) ∧
(∀ (n : ℕ) (a : A), 0 < n → ¬p ∣ n → IsUnit a →
ξ = (algebraMap A K π)⁻¹ ^ n * algebraMap A K a → totallyRamified) ∧
(∀ (n : ℕ) (a : A), 0 < n → p ∣ n →
(¬∃ b : IsLocalRing.ResidueField A, IsLocalRing.residue A a = b ^ p) →
ξ = (algebraMap A K π)⁻¹ ^ n * algebraMap A K a →
residuallyInseparable)
Tag 09F1, a lemma
Tag 09F1 in the Stacks Project.
IsDiscreteValuationRing.exists_isGalois_totallyRamified_isWeakSolution_of_charP, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/ArtinSchreier/CharPSolution.lean, line 690.
In equal characteristic
p, a weakly unramified extensionA ⊆ Bfollowed by a degree-pGalois extension of fraction fields admits a finite Galois base extension which is totally ramified overAand is a weak solution forA → C, provided the image of the residue field ofAin that ofBis the intersection of all sets ofp ^ n-th powers forn ≥ 1.This is Tag 09F1 as stated. The two consequences of
hresiduethat the proof consumes are isolated inexists_isGalois_totallyRamified_isWeakSolution_of_charP_of_perfectCore_le, which is strictly more general: it drops the inclusionimage ⊆ perfectCoreentirely, keeping only perfectness ofκ_AandperfectCore κ_B p ⊆ image.
theorem exists_isGalois_totallyRamified_isWeakSolution_of_charP
(A : Type uA) (B : Type uB) (C : Type uC)
(K : Type uK) (L : Type uL) (M : Type uM)
[CommRing A] [CommRing B] [CommRing C]
[IsDomain A] [IsDomain B] [IsDomain C]
[IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[IsDiscreteValuationRing C]
[Field K] [Field L] [Field M]
[Algebra A B] [Algebra B C] [Algebra A C]
[Algebra A K] [Algebra B L] [Algebra C M]
[Algebra K L] [Algebra L M] [Algebra K M]
[Algebra A L] [Algebra B M] [Algebra A M]
[IsScalarTower A B C] [IsScalarTower A B L] [IsScalarTower A K L]
[IsScalarTower B C M] [IsScalarTower B L M]
[IsScalarTower A C M] [IsScalarTower A K M] [IsScalarTower K L M]
[IsExtension A B] [IsExtension B C]
[IsExtension A C]
[IsFractionRing A K] [IsFractionRing B L] [IsFractionRing C M]
(p : ℕ) (hp : p.Prime) [CharP K p]
[FiniteDimensional L M] [IsGalois L M]
(hdegree : Module.finrank L M = p)
(hweak : IsWeaklyUnramified A B)
(hresidue : ∀ x : IsLocalRing.ResidueField B,
(∃ a : IsLocalRing.ResidueField A,
algebraMap (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B) a = x) ↔
∀ n : ℕ, 1 ≤ n → ∃ y : IsLocalRing.ResidueField B, y ^ (p ^ n) = x) :
∃ (K₁ : Type uK) (_ : Field K₁) (_ : Algebra K K₁) (_ : Algebra A K₁)
(_ : IsScalarTower A K K₁) (_ : Module.Finite K K₁) (_ : IsGalois K K₁),
IsTotallyRamifiedWithRespectTo A K K₁ ∧
∃ D : IntegralClosureBaseChange.{uA, uC, uK, uM, uK,
max uM uK, uK, max uM uK} A C K M K₁,
D.IsWeakSolution
Tag 09F2, a lemma
Tag 09F2 in the Stacks Project.
main_statement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/NumberTheory/Cyclotomic/OneAddPow/QuotientPolynomial.lean, line 768.
Lemma 15.117.13 (Stacks tag 09F2). Let
pbe prime,Aa commutative ring containing a primitivep-th root of unityζ(encoded byf : ℤ[ζ_p] → A), andw = 1 - ζ. Then there is ONE common polynomialP ∈ A[z]such that:
- (Statement 1, integrality)
Pis the quotient((1 + w z)^p - 1)/w^poverA:w^p · P = (1 + wz)^p - 1inA[z],P = ∑_{0 < i ≤ p} c_i z^i, andw^{p-i} · c_i = (p choose i)for0 < i ≤ p(predicateintProp). In particularPis monic of degreep. The corresponding statement in(A[w⁻¹])[z](predicatequotChar) is recorded too, but it is weaker — vacuous whenwis nilpotent, seequotChar_of_isNilpotent— so it isintPropthat carries the assertion "P ∈ A[z]";- (Statement 1, shape)
P(z) = z^p - z + ∑_{0 < i < p} a_i z^iwitha_i ∈ (w)(predicateshapeProp);- (Statement 2, functional equation)
P(z_1 + z_2 + w z_1 z_2) = P(z_1) + P(z_2) + w^p P(z_1) P(z_2)inA[z_1, z_2](predicatefuncEq).Bundling all of them into a single existential guarantees they hold for the same
P.
theorem main_statement :
∃ P : A[X], intProp f P ∧ quotChar f P ∧ shapeProp f P ∧ funcEq f P
Tag 09F3, a lemma
Tag 09F3 in the Stacks Project.
isGalois_and_ramification_cases_of_adjoin_root_cyclotomic_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/NumberTheory/Cyclotomic/OneAddPow/RamificationCases.lean, line 511.
Let
Abe a mixed-characteristic discrete valuation ring containing a primitivep-th root of unity, and letPbe the cyclotomic quotient polynomial of Tag 09F2. IfL = K[z]withP(z) = ξ, thenL / Kis Galois and is either trivial, unramified of degreep, totally ramified with ramification indexp, or weakly unramified with purely inseparable residue extension of degreep.Moreover, for a uniformizer
πofA, an integralξgives one of the first two cases; a pole of positive order not divisible bypgives the totally ramified case; and a pole whose order is divisible bypand whose leading coefficient is not ap-th power in the residue field gives the weakly unramified, residually inseparable case.
theorem isGalois_and_ramification_cases_of_adjoin_root_cyclotomic_quotient
(A : Type uA) (K : Type uK) (L : Type uL)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Algebra A K] [IsFractionRing A K] [CharZero K]
[Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
(p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField A) p]
(f : CyclotomicRing p ℤ ℚ →+* A) (P : Polynomial A)
(hP : intProp f P ∧ quotChar f P ∧ shapeProp f P ∧ funcEq f P)
(ξ : K) (z : L)
(hz : Polynomial.aeval z P = algebraMap K L ξ)
(hgen : Algebra.adjoin K {z} = ⊤)
(π : A) (hπ : Irreducible π) :
∃ hfin : Module.Finite K L,
letI := hfin
let B := integralClosure A L
let mA := IsLocalRing.maximalIdeal A
let trivial : Prop := Function.Surjective (algebraMap K L)
let unramified : Prop :=
Module.finrank K L = p ∧
∀ m : Ideal B, m.IsMaximal → ∃ _ : m.LiesOver mA,
Ideal.ramificationIdx' mA m = 1 ∧
@Algebra.IsSeparable (A ⧸ mA) (B ⧸ m) _ _
(Ideal.Quotient.algebraOfLiesOver m mA)
let totallyRamified : Prop :=
Stacks.KummerExtension.IsTotallyRamified A K L ∧
∀ m : Ideal B, m.IsMaximal → m.LiesOver mA →
Ideal.ramificationIdx' mA m = p
let residuallyInseparable : Prop :=
∃ hDVR : IsDiscreteValuationRing B,
letI := hDVR
let mB := IsLocalRing.maximalIdeal B
∃ _ : mB.LiesOver mA,
Ideal.ramificationIdx' mA mB = 1 ∧
letI := Ideal.Quotient.algebraOfLiesOver mB mA
IsPurelyInseparable (A ⧸ mA) (B ⧸ mB) ∧
Module.finrank (A ⧸ mA) (B ⧸ mB) = p
IsGalois K L ∧
(trivial ∨ unramified ∨ totallyRamified ∨ residuallyInseparable) ∧
((∃ a : A, ξ = algebraMap A K a) → trivial ∨ unramified) ∧
(∀ (n : ℕ) (a : A), 0 < n → ¬p ∣ n → IsUnit a →
ξ = (algebraMap A K π)⁻¹ ^ n * algebraMap A K a → totallyRamified) ∧
(∀ (n : ℕ) (a : A), 0 < n → p ∣ n →
(¬∃ b : IsLocalRing.ResidueField A, IsLocalRing.residue A a = b ^ p) →
ξ = (algebraMap A K π)⁻¹ ^ n * algebraMap A K a →
residuallyInseparable)
Tag 09F4, a lemma
Tag 09F4 in the Stacks Project.
Stacks.DegreePExtensionLevel.exists_totallyRamified_galoisExtension_isWeakSolution_or_finiteLevel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/ExtensionLevel/FiniteLevel.lean, line 859.
In mixed characteristic, a weakly unramified tower followed by a Galois extension of prime degree admits a finite, totally ramified base extension. This base extension is either a weak solution for the full tower or makes the canonical tensor-product extension a degree-
pextension of finite level.
theorem exists_totallyRamified_galoisExtension_isWeakSolution_or_finiteLevel
(A B C K L M : Type u)
[CommRing A] [CommRing B] [CommRing C]
[IsDomain A] [IsDomain B] [IsDomain C]
[IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[IsDiscreteValuationRing C]
[Field K] [Field L] [Field M]
[Algebra A B] [Algebra B C] [Algebra A C]
[Algebra A K] [Algebra B L] [Algebra C M]
[Algebra K L] [Algebra L M] [Algebra K M]
[Algebra A L] [Algebra A M] [Algebra B M]
[IsScalarTower A B C] [IsScalarTower A B L]
[IsScalarTower B C M] [IsScalarTower B L M]
[IsScalarTower A C M] [IsScalarTower A K L]
[IsScalarTower A K M] [IsScalarTower K L M]
[IsDiscreteValuationRing.IsExtension A B] [IsDiscreteValuationRing.IsExtension B C]
[IsDiscreteValuationRing.IsExtension A C]
[IsFractionRing A K] [IsFractionRing B L] [IsFractionRing C M]
(p : ℕ) [Fact p.Prime] [CharZero K]
[CharP (IsLocalRing.ResidueField A) p]
(hweak : IsDiscreteValuationRing.IsWeaklyUnramified A B)
(f : CyclotomicRing p ℤ ℚ →+* B)
[FiniteDimensional L M] [IsGalois L M]
(hdegree : Module.finrank L M = p) :
∃ (K₁ : Type u) (_ : Field K₁) (_ : Algebra K K₁) (_ : Algebra A K₁)
(_ : IsScalarTower A K K₁) (_ : Module.Finite K K₁),
IsDiscreteValuationRing.IsTotallyRamifiedWithRespectTo A K K₁ ∧
((∃ D : IsDiscreteValuationRing.IntegralClosureBaseChange.{u, u, u, u, u, u, u, u} A C K M
K₁,
D.IsWeakSolution) ∨
let L₁ := L ⊗[K] K₁
let M₁ := M ⊗[K] K₁
∃ (hL₁ : IsField L₁) (hM₁ : IsField M₁),
letI := hL₁.toField
letI := hM₁.toField
let ι : L₁ →ₐ[K] M₁ :=
Algebra.TensorProduct.map (IsScalarTower.toAlgHom K L M) (AlgHom.id K K₁)
letI : Algebra L₁ M₁ := ι.toRingHom.toAlgebra
let B₁ := integralClosure B L₁
∃ (hB₁ : IsDiscreteValuationRing B₁) (hfrac : IsFractionRing B₁ L₁)
(hfin : Module.Finite L₁ M₁),
letI := hB₁
letI := hfrac
letI := hfin
∃ P : Polynomial B,
intProp f P ∧ quotChar f P ∧ shapeProp f P ∧ funcEq f P ∧
IsDegreePExtensionOfFiniteLevel B₁ L₁ M₁ p
((algebraMap B B₁).comp f) (P.map (algebraMap B B₁)))
Tag 09F5, a lemma
Tag 09F5 in the Stacks Project.
Stacks.DiscreteValuationRing.EppLevelInduction.exists_totallyRamified_isWeakSolution_or_extensionLevel_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/ExtensionLevel/LevelLowering.lean, line 850.
The traditional Tag 09F5 interface. The global residue-field hypothesis identifies the perfect core with the image of the base residue field, so the finite-support alternative in
exists_totallyRamified_isWeakSolution_or_extensionLevel_le_or_finiteSupport_of_uniformizeris impossible.
theorem exists_totallyRamified_isWeakSolution_or_extensionLevel_le
(A B C K L M : Type u)
[CommRing A] [CommRing B] [CommRing C]
[IsDomain A] [IsDomain B] [IsDomain C]
[IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[IsDiscreteValuationRing C]
[Field K] [Field L] [Field M]
[Algebra A B] [Algebra B C] [Algebra A C]
[Algebra A K] [Algebra B L] [Algebra C M]
[Algebra K L] [Algebra L M] [Algebra K M]
[Algebra A L] [Algebra A M] [Algebra B M]
[IsScalarTower A B C] [IsScalarTower A B L]
[IsScalarTower B C M] [IsScalarTower B L M]
[IsScalarTower A C M] [IsScalarTower A K L]
[IsScalarTower A K M] [IsScalarTower K L M]
[IsDiscreteValuationRing.IsExtension A B] [IsDiscreteValuationRing.IsExtension B C]
[IsDiscreteValuationRing.IsExtension A C]
[IsFractionRing A K] [IsFractionRing B L] [IsFractionRing C M]
(p : ℕ) [Fact p.Prime] [CharZero K]
[CharP (IsLocalRing.ResidueField A) p]
(hweak : IsDiscreteValuationRing.IsWeaklyUnramified A B)
(f : CyclotomicRing p ℤ ℚ →+* B) (P : Polynomial B)
(hP : intProp f P ∧ quotChar f P ∧ shapeProp f P ∧ funcEq f P)
[Module.Finite L M]
(hfinite : Stacks.DegreePExtensionLevel.IsDegreePExtensionOfFiniteLevel B L M p f P)
(l : ℚ)
(hlevel : ∃ (π : B) (e₁ : ℕ) (he₁ : 0 < e₁)
(hne : (Stacks.DegreePExtensionLevel.extensionLevelNumerators B L M P π).Nonempty),
Irreducible π ∧ Associated (wElt f) (π ^ e₁) ∧
l = Stacks.DegreePExtensionLevel.extensionLevel B L M P π e₁ he₁ hne)
(hl : 0 < l)
(hresidue : ∀ x : IsLocalRing.ResidueField B,
(∃ a : IsLocalRing.ResidueField A,
algebraMap (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B) a = x) ↔
∀ n : ℕ, 1 ≤ n → ∃ y : IsLocalRing.ResidueField B, y ^ (p ^ n) = x) :
∃ (K₁ : Type u) (_ : Field K₁) (_ : Algebra K K₁) (_ : Algebra A K₁)
(_ : IsScalarTower A K K₁) (_ : Module.Finite K K₁)
(_ : Algebra.IsSeparable K K₁),
IsDiscreteValuationRing.IsTotallyRamifiedWithRespectTo A K K₁ ∧
((∃ D : IsDiscreteValuationRing.IntegralClosureBaseChange.{u, u, u, u, u, u, u, u}
A C K M K₁, D.IsWeakSolution) ∨
let L₁ := L ⊗[K] K₁
let M₁ := M ⊗[K] K₁
∃ (hL₁ : IsField L₁) (hM₁ : IsField M₁),
letI := hL₁.toField
letI := hM₁.toField
let ι : L₁ →ₐ[K] M₁ :=
Algebra.TensorProduct.map (IsScalarTower.toAlgHom K L M) (AlgHom.id K K₁)
letI : Algebra L₁ M₁ := ι.toRingHom.toAlgebra
let B₁ := integralClosure B L₁
∃ (hB₁ : IsDiscreteValuationRing B₁) (hfrac : IsFractionRing B₁ L₁)
(hfin : Module.Finite L₁ M₁),
letI := hB₁
letI := hfrac
letI := hfin
let f₁ := (algebraMap B B₁).comp f
let P₁ := P.map (algebraMap B B₁)
Stacks.DegreePExtensionLevel.IsDegreePExtensionOfFiniteLevel B₁ L₁ M₁ p f₁ P₁ ∧
∃ (π₁ : B₁) (e₁ : ℕ) (he₁ : 0 < e₁)
(hne : (Stacks.DegreePExtensionLevel.extensionLevelNumerators B₁ L₁ M₁ P₁
π₁).Nonempty),
Irreducible π₁ ∧ Associated (wElt f₁) (π₁ ^ e₁) ∧
Stacks.DegreePExtensionLevel.extensionLevel B₁ L₁ M₁ P₁ π₁ e₁ he₁ hne ≤
max 0 (max (l - 1) (2 * l - (p : ℚ))))
Tag 09F6, an equation
Tag 09F6 in the Stacks Project.
IsDiscreteValuationRing.eval_sub_pow_sub_mem_uniformizer_zpow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/EliminateRamification.lean, line 163.
For the Kummer polynomial
Passociated to a primitivep-th root of unity, ifw = 1 - ζhas ordere₁andπ ^ n P(z)is integral, thenP(z) ≡ z ^ p - zmoduloπ ^ (e₁ - n) B.
theorem eval_sub_pow_sub_mem_uniformizer_zpow
(B : Type uB) (K : Type uK)
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[Field K] [Algebra B K] [IsFractionRing B K]
(p : ℕ) [Fact p.Prime]
(f : CyclotomicRing p ℤ ℚ →+* B) (P : Polynomial B)
(hP : shapeProp f P)
(π : B) (hπ : Irreducible π) (e₁ n : ℕ)
(hw : Associated (wElt f) (π ^ e₁)) (z : K)
(hz : ∃ b : B,
(algebraMap B K π) ^ n * P.eval₂ (algebraMap B K) z = algebraMap B K b) :
∃ b : B,
P.eval₂ (algebraMap B K) z - (z ^ p - z) =
(algebraMap B K π) ^ ((e₁ : ℤ) - n) * algebraMap B K b
Tag 09F7, an equation
Tag 09F7 in the Stacks Project.
IsDiscreteValuationRing.add_mul_correction_sModEq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/EliminateRamification.lean, line 219.
Stacks 09F7. The correction term in the finite-level group law vanishes modulo
π ^ (-2n + p e₁) B.
theorem add_mul_correction_sModEq
{B K : Type*} [CommRing B] [IsDomain B] [Field K]
[Algebra B K] [IsFractionRing B K]
{p n e₁ : ℕ} {π w : B} {ξ₁ ξ₂ : K}
(hw : Associated w (π ^ e₁))
(hξ₁ : ξ₁ ∈ FractionalIdeal.spanSingleton B⁰
((algebraMap B K π) ^ (-(n : ℤ))))
(hξ₂ : ξ₂ ∈ FractionalIdeal.spanSingleton B⁰
((algebraMap B K π) ^ (-(n : ℤ)))) :
SModEq (FractionalIdeal.spanSingleton B⁰
((algebraMap B K π) ^ (-(2 : ℤ) * n + p * e₁ : ℤ)) : Submodule B K)
(ξ₁ + ξ₂ + (algebraMap B K w) ^ p * ξ₁ * ξ₂) (ξ₁ + ξ₂)
Tag 09F8, a lemma
Tag 09F8 in the Stacks Project.
IsDiscreteValuationRing.exists_finite_extension_isWeakSolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/EppAlgClosedResidue/IntermediateFieldInduction.lean, line 681.
Epp's theorem in the complete case: under the residue-field intersection hypothesis, every finite extension at the top of a weakly unramified tower admits a finite base extension which is a weak solution for the full tower.
theorem exists_finite_extension_isWeakSolution
(A : Type uA) (B : Type uB) (C : Type uC)
(K : Type uK) (L : Type uL) (M : Type uM)
[CommRing A] [CommRing B] [CommRing C]
[IsDomain A] [IsDomain B] [IsDomain C]
[IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[IsDiscreteValuationRing C]
[Field K] [Field L] [Field M]
[Algebra A B] [Algebra B C] [Algebra A C]
[Algebra A K] [Algebra B L] [Algebra C M]
[Algebra K L] [Algebra L M] [Algebra K M]
[Algebra A L] [Algebra B M] [Algebra A M]
[IsScalarTower A B C] [IsScalarTower A B L] [IsScalarTower A K L]
[IsScalarTower B C M] [IsScalarTower B L M]
[IsScalarTower A C M] [IsScalarTower A K M] [IsScalarTower K L M]
[IsDiscreteValuationRing.IsExtension A B] [IsDiscreteValuationRing.IsExtension B C]
[IsDiscreteValuationRing.IsExtension A C]
[IsFractionRing A K] [IsFractionRing B L] [IsFractionRing C M]
(p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField A) p]
[IsAlgClosed (IsLocalRing.ResidueField A)]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
[IsAdicComplete (IsLocalRing.maximalIdeal B) B]
(hweak : IsDiscreteValuationRing.IsWeaklyUnramified A B)
[Module.Finite L M]
(hresidue : ∀ x : IsLocalRing.ResidueField B,
(∃ a : IsLocalRing.ResidueField A,
algebraMap (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B) a = x) ↔
∀ n : ℕ, 1 ≤ n → ∃ y : IsLocalRing.ResidueField B, y ^ (p ^ n) = x) :
∃ (K₁ : Type uK) (_ : Field K₁) (_ : Algebra K K₁) (_ : Algebra A K₁)
(_ : IsScalarTower A K K₁) (_ : Module.Finite K K₁),
∃ D : IsDiscreteValuationRing.IntegralClosureBaseChange.{uA, uC, uK, uM, uK,
max uM uK, uK, max uM uK} A C K M K₁,
D.IsWeakSolution
Tag 09F9, a theorem
Tag 09F9 in the Stacks Project.
Stacks.EppTheorem.exists_finite_extension_isWeakSolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/EppTheorem.lean, line 26.
Epp's theorem when all input types lie in one universe.
theorem exists_finite_extension_isWeakSolution
(A B K L : Type u)
[CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
[IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
[Field K] [Field L]
[Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L]
[IsScalarTower A B L] [IsScalarTower A K L]
[IsExtension A B] [IsFractionRing A K] [IsFractionRing B L]
(hEpp : ∀ p : ℕ, p.Prime → CharP (ResidueField A) p →
∀ [ExpChar (ResidueField B) p], EppCondition A B p) :
∃ (K₁ : Type u) (_ : Field K₁) (_ : Algebra K K₁) (_ : Algebra A K₁)
(_ : IsScalarTower A K K₁) (_ : Module.Finite K K₁),
∃ D : IntegralClosureBaseChange.{u, u, u, u, u, u, u, u} A B K L K₁,
D.IsWeakSolution
Sources
Section15.118 Eliminating ramification, II#
Section 15.118 of the Stacks Project, Tag 0GLQ. 9 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GLR, a lemma
Tag 0GLR in the Stacks Project.
IsDiscreteValuationRing.exists_isSolution_of_tower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/SolutionTower.lean, line 590.
A finite extension of a solution for an extension of discrete valuation rings is again a solution.
theorem exists_isSolution_of_tower
(A : Type uA) (B : Type uB) (K : Type uK) (L : Type uL)
(K₁ : Type uK₁) (K₂ : Type uK₂)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[Field K] [Field L] [Field K₁] [Field K₂]
[Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L]
[Algebra K K₁] [Algebra K₁ K₂] [Algebra K K₂]
[Algebra A K₁] [Algebra A K₂]
[IsScalarTower A B L] [IsScalarTower A K L]
[IsScalarTower A K K₁] [IsScalarTower A K K₂]
[IsScalarTower K K₁ K₂] [IsScalarTower A K₁ K₂]
[IsExtension A B]
[IsFractionRing A K] [IsFractionRing B L]
[Module.Finite K K₁] [Module.Finite K₁ K₂]
(hsolution :
∃ D₁ : IntegralClosureBaseChange.{uA, uB, uK, uL, uK₁,
max uL uK₁, uK₁, max uL uK₁} A B K L K₁,
D₁.IsSolution.{uA, uB, uK, uL, uK₁, max uL uK₁, uK₁, max uL uK₁,
max uL uK₁}) :
letI : Module.Finite K K₂ := Module.Finite.trans K₁ K₂
∃ D₂ : IntegralClosureBaseChange.{uA, uB, uK, uL, uK₂,
max uL uK₂, uK₂, max uL uK₂} A B K L K₂,
D₂.IsSolution.{uA, uB, uK, uL, uK₂, max uL uK₂, uK₂, max uL uK₂,
max uL uK₂}
Tag 0GLS, a lemma
Tag 0GLS in the Stacks Project.
IsNagataRing.of_isSeparable_fractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Descent.lean, line 463.
Let
A → Bbe an extension of discrete valuation rings, and letK → Lbe the induced extension of their fraction fields. IfBis Nagata andL/Kis separable, thenAis Nagata.
theorem of_isSeparable_fractionRing
(A B K L : Type u) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B]
[IsDiscreteValuationRing A] [IsDiscreteValuationRing B] [Algebra A B]
[IsDiscreteValuationRing.IsExtension A B]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra B L] [IsFractionRing B L] [Algebra A L] [Algebra K L]
[IsScalarTower A B L] [IsScalarTower A K L]
(hB : IsNagataRing B) (hsep : Algebra.IsSeparableExtension K L) :
IsNagataRing A
Tag 0GLT, a lemma
Tag 0GLT in the Stacks Project.
exists_bound_finite_extension_ringEquiv_mod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FiniteExtension/ModPow/QuotientEquiv.lean, line 241.
Stacks 0GLT. Let
A' ⊂ Abe an extension of rings andf ∈ A', withAfinite overA',fa nonzerodivisor onA, andA'_f = A_f. Then there isn₀ > 0such that for alln ≥ n₀: for every ringB', every nonzerodivisorg ∈ B', and every ring isomorphismφ' : A'/f^n A' ≃ B'/g^n B'sending the class offto the class ofg, there exist a finite ring extensionB' ⊂ Band a ring isomorphismφ : A/fA ≃ B/gBcompatible withφ', i.e. making the square of reduction maps commute.
theorem exists_bound_finite_extension_ringEquiv_mod
(A' : Type u) (A : Type v) [CommRing A'] [CommRing A] [Algebra A' A]
(hinj : Function.Injective (algebraMap A' A))
(f : A')
[Module.Finite A' A]
(hnzd : algebraMap A' A f ∈ nonZeroDivisors A)
(hloc : LocalizationEq A' A f) :
∃ n₀ : ℕ, 0 < n₀ ∧ ∀ n : ℕ, n₀ ≤ n →
∀ (B' : Type w) [CommRing B'] (g : B') (_ : g ∈ nonZeroDivisors B')
(hn : 1 ≤ n)
(φ' : (A' ⧸ Ideal.span {f ^ n}) ≃+* (B' ⧸ Ideal.span {g ^ n})),
φ' (Ideal.Quotient.mk _ f) = Ideal.Quotient.mk _ g →
∃ (B : Type w) (_ : CommRing B) (_ : Algebra B' B),
Function.Injective (algebraMap B' B) ∧
Module.Finite B' B ∧
∃ φ : (A ⧸ Ideal.span {algebraMap A' A f}) ≃+*
(B ⧸ Ideal.span {algebraMap B' B g}),
(φ : (A ⧸ Ideal.span {algebraMap A' A f}) →+* _).comp
(reductionMap A' A f n hn)
= (reductionMap B' B g n hn).comp
(φ' : (A' ⧸ Ideal.span {f ^ n}) →+* _)
Tag 0GLU, a remark
Tag 0GLU in the Stacks Project.
exists_compatible_finite_extensions_of_quotient_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FiniteExtension/ModPow/QuotientEquiv.lean, line 469.
Stacks 0GLU. The construction of
exists_bound_finite_extension_ringEquiv_modis functorial. Given a commutative square of finite injective ring extensions satisfying its hypotheses, and a compatible square of isomorphisms modulo a sufficiently large common power, the two constructed finite extensions admit a map extending the given map of base rings. Both the square of extensions and the square of the resulting isomorphisms modulo the nonzerodivisors commute. As in the constructionB = g^{-t} N ⊆ B'_gofbSubalg, each extension becomes an isomorphism after inverting the corresponding image ofg, and this image is a nonzerodivisor in the constructed ring.
theorem exists_compatible_finite_extensions_of_quotient_equiv
(A₁' : Type u₁) (A₁ : Type v₁) (A₂' : Type u₂) (A₂ : Type v₂)
[CommRing A₁'] [CommRing A₁] [CommRing A₂'] [CommRing A₂]
[Algebra A₁' A₁] [Algebra A₂' A₂]
(iA₁ : Function.Injective (algebraMap A₁' A₁))
(iA₂ : Function.Injective (algebraMap A₂' A₂))
(a' : A₁' →+* A₂') (a : A₁ →+* A₂)
(ha : a.comp (algebraMap A₁' A₁) = (algebraMap A₂' A₂).comp a')
(f : A₁')
(hfin₁ : Module.Finite A₁' A₁) (hfin₂ : Module.Finite A₂' A₂)
(hnzd₁ : algebraMap A₁' A₁ f ∈ nonZeroDivisors A₁)
(hnzd₂ : algebraMap A₂' A₂ (a' f) ∈ nonZeroDivisors A₂)
(hloc₁ : LocalizationEq A₁' A₁ f)
(hloc₂ : LocalizationEq A₂' A₂ (a' f)) :
∃ (n₀₁ : ℕ) (_ : 0 < n₀₁) (n₀₂ : ℕ) (_ : 0 < n₀₂),
∀ (n : ℕ) (hnmax : max n₀₁ n₀₂ ≤ n),
∀ (B₁' : Type w₁) (B₂' : Type w₂) [CommRing B₁'] [CommRing B₂']
(b' : B₁' →+* B₂') (g : B₁')
(_ : g ∈ nonZeroDivisors B₁') (_ : b' g ∈ nonZeroDivisors B₂')
(φ₁' : (A₁' ⧸ Ideal.span {f ^ n}) ≃+* (B₁' ⧸ Ideal.span {g ^ n}))
(φ₂' : (A₂' ⧸ Ideal.span {(a' f) ^ n}) ≃+*
(B₂' ⧸ Ideal.span {(b' g) ^ n})),
φ₂'.toRingHom.comp
(Ideal.quotientMap (Ideal.span {(a' f) ^ n}) a' (by
apply Ideal.span_le.2
rintro _ rfl
change a' (f ^ n) ∈ Ideal.span {(a' f) ^ n}
rw [map_pow]
exact Ideal.subset_span (Set.mem_singleton _))) =
(Ideal.quotientMap (Ideal.span {(b' g) ^ n}) b' (by
apply Ideal.span_le.2
rintro _ rfl
change b' (g ^ n) ∈ Ideal.span {(b' g) ^ n}
rw [map_pow]
exact Ideal.subset_span (Set.mem_singleton _))).comp φ₁'.toRingHom →
φ₁' (Ideal.Quotient.mk _ f) = Ideal.Quotient.mk _ g →
∃ (B₁ : Type w₁) (_ : CommRing B₁) (_ : Algebra B₁' B₁)
(B₂ : Type w₂) (_ : CommRing B₂) (_ : Algebra B₂' B₂),
Function.Injective (algebraMap B₁' B₁) ∧ Module.Finite B₁' B₁ ∧
Function.Injective (algebraMap B₂' B₂) ∧ Module.Finite B₂' B₂ ∧
LocalizationEq B₁' B₁ g ∧ LocalizationEq B₂' B₂ (b' g) ∧
algebraMap B₁' B₁ g ∈ nonZeroDivisors B₁ ∧
algebraMap B₂' B₂ (b' g) ∈ nonZeroDivisors B₂ ∧
∃ (b : B₁ →+* B₂)
(hb : b.comp (algebraMap B₁' B₁) = (algebraMap B₂' B₂).comp b')
(φ₁ : (A₁ ⧸ Ideal.span {algebraMap A₁' A₁ f}) ≃+*
(B₁ ⧸ Ideal.span {algebraMap B₁' B₁ g}))
(φ₂ : (A₂ ⧸ Ideal.span {algebraMap A₂' A₂ (a' f)}) ≃+*
(B₂ ⧸ Ideal.span {algebraMap B₂' B₂ (b' g)})),
φ₂.toRingHom.comp
(Ideal.quotientMap (Ideal.span {algebraMap A₂' A₂ (a' f)}) a (by
apply Ideal.span_le.2
rintro _ rfl
change a (algebraMap A₁' A₁ f) ∈
Ideal.span {algebraMap A₂' A₂ (a' f)}
rw [show a (algebraMap A₁' A₁ f) =
algebraMap A₂' A₂ (a' f) from DFunLike.congr_fun ha f]
exact Ideal.subset_span (Set.mem_singleton _))) =
(Ideal.quotientMap (Ideal.span {algebraMap B₂' B₂ (b' g)}) b (by
apply Ideal.span_le.2
rintro _ rfl
change b (algebraMap B₁' B₁ g) ∈
Ideal.span {algebraMap B₂' B₂ (b' g)}
rw [show b (algebraMap B₁' B₁ g) =
algebraMap B₂' B₂ (b' g) from DFunLike.congr_fun hb g]
exact Ideal.subset_span (Set.mem_singleton _))).comp
φ₁.toRingHom ∧
φ₁.toRingHom.comp (reductionMap A₁' A₁ f n (by omega)) =
(reductionMap B₁' B₁ g n (by omega)).comp φ₁'.toRingHom ∧
φ₂.toRingHom.comp (reductionMap A₂' A₂ (a' f) n (by omega)) =
(reductionMap B₂' B₂ (b' g) n (by omega)).comp φ₂'.toRingHom
Tag 0GLV, a lemma
Tag 0GLV in the Stacks Project.
IsDiscreteValuationRing.exists_isSeparable_solution_of_isPurelyInseparable_finrank_eq_prime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/SeparableSolution/InseparableStep.lean, line 45.
Let
A → Bbe an extension of discrete valuation rings with separable fraction-field extensionL/K, whereKhas prime characteristicp, and suppose thatBis Nagata. IfK → K₁ → K₂is a tower of finite extensions,K₂is a solution forA → B, andK₂/K₁is purely inseparable of degreep, then some separable extensionK₃/K₁is a solution forA → B.
theorem exists_isSeparable_solution_of_isPurelyInseparable_finrank_eq_prime
(A : Type uA) (B : Type uB) (K : Type uK) (L : Type uL)
(K₁ : Type uK₁) (K₂ : Type uK₂)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[Field K] [Field L] [Field K₁] [Field K₂]
[Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L]
[Algebra K K₁] [Algebra K₁ K₂] [Algebra K K₂]
[Algebra A K₁] [Algebra A K₂]
[IsScalarTower A B L] [IsScalarTower A K L]
[IsScalarTower A K K₁] [IsScalarTower A K K₂]
[IsScalarTower K K₁ K₂] [IsScalarTower A K₁ K₂]
[IsExtension A B]
[IsFractionRing A K] [IsFractionRing B L]
[Module.Finite K K₁] [Module.Finite K₁ K₂]
(p : ℕ) (hp : p.Prime) [CharP K p]
(hsep : Algebra.IsSeparableExtension K L)
(hB : IsNagataRing B)
(hsolution :
letI : Module.Finite K K₂ := Module.Finite.trans K₁ K₂
∃ D₂ : IntegralClosureBaseChange.{uA, uB, uK, uL, uK₂,
max uL uK₂, uK₂, max uL uK₂} A B K L K₂,
D₂.IsSolution.{uA, uB, uK, uL, uK₂, max uL uK₂, uK₂, max uL uK₂,
max uL uK₂})
(hpi : IsPurelyInseparable K₁ K₂)
(hdegree : Module.finrank K₁ K₂ = p) :
∃ (K₃ : Type uK₁) (_ : Field K₃) (_ : Algebra K₁ K₃) (_ : Algebra K K₃)
(_ : Algebra A K₃) (_ : IsScalarTower K K₁ K₃) (_ : IsScalarTower A K K₃)
(_ : IsScalarTower A K₁ K₃) (_ : Module.Finite K K₃),
Algebra.IsSeparable K₁ K₃ ∧
∃ D₃ : IntegralClosureBaseChange.{uA, uB, uK, uL, uK₁,
max uL uK₁, uK₁, max uL uK₁} A B K L K₃,
D₃.IsSolution.{uA, uB, uK, uL, uK₁, max uL uK₁, uK₁, max uL uK₁,
max uL uK₁}
Tag 0BRN, a lemma
Tag 0BRN in the Stacks Project.
IsDiscreteValuationRing.exists_isSeparableSolution_of_exists_isSolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/SeparableSolution/InseparableStep.lean, line 784.
Let
A → Bbe an extension of discrete valuation rings with separable fraction-field extensionL/K. IfBis Nagata and there is a solution forA → B, then there is a separable solution forA → B.
theorem exists_isSeparableSolution_of_exists_isSolution
(A : Type uA) (B : Type uB) (K : Type uK) (L : Type uL)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[Field K] [Field L]
[Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L]
[IsScalarTower A B L] [IsScalarTower A K L]
[IsExtension A B]
[IsFractionRing A K] [IsFractionRing B L]
(hsep : Algebra.IsSeparableExtension K L)
(hB : IsNagataRing B)
(hsolution :
∃ (K₂ : Type uE) (_ : Field K₂) (_ : Algebra K K₂) (_ : Algebra A K₂)
(_ : IsScalarTower A K K₂) (_ : Module.Finite K K₂),
∃ D₂ : IntegralClosureBaseChange.{uA, uB, uK, uL, uE,
max uL uE, uE, max uL uE} A B K L K₂,
D₂.IsSolution.{uA, uB, uK, uL, uE,
max uL uE, uE, max uL uE, max uL uE}) :
∃ (K₁ : Type uE) (_ : Field K₁) (_ : Algebra K K₁) (_ : Algebra A K₁)
(_ : IsScalarTower A K K₁) (_ : Module.Finite K K₁),
∃ D₁ : IntegralClosureBaseChange.{uA, uB, uK, uL, uE,
max uL uE, uE, max uL uE} A B K L K₁,
D₁.IsSeparableSolution.{uA, uB, uK, uL, uE,
max uL uE, uE, max uL uE, max uL uE}
Tag 09IH, a lemma
Tag 09IH in the Stacks Project.
IsDiscreteValuationRing.integralClosure_reducedTensorProduct_isNoetherian_and_spec_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/EliminateRamificationII.lean, line 430.
Let
A → Bbe an essentially finite type extension of discrete valuation rings with fraction fieldsK → L. IfK'/Kis algebraic and the integral closureA'ofAinK'is Noetherian, then the integral closureB'ofBin the reduction ofL ⊗[K] K'is Noetherian. The canonical mapSpec(B') → Spec(A')is surjective and all corresponding residue field extensions are finitely generated.
theorem integralClosure_reducedTensorProduct_isNoetherian_and_spec_surjective
(A : Type uA) (B : Type uB) (K : Type uK) (L : Type uL)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[Algebra A B] [FaithfulSMul A B] [IsLocalHom (algebraMap A B)]
[Field K] [Algebra A K] [IsFractionRing A K]
[Field L] [Algebra B L] [IsFractionRing B L]
[Algebra A L] [Algebra K L]
[IsScalarTower A B L] [IsScalarTower A K L]
[Algebra.EssFiniteType A B]
(K' : Type v) [Field K'] [Algebra K K'] [Algebra.IsAlgebraic K K']
[Algebra A K'] [IsScalarTower A K K']
[IsNoetherianRing (integralClosure A K')] :
let L' := (L ⊗[K] K') ⧸ nilradical (L ⊗[K] K')
let A' := integralClosure A K'
let B' := integralClosure B L'
IsNoetherianRing B' ∧
∃ f : A' →+* B',
(∀ x : A',
((B').val (f x) : L') =
algebraMap (L ⊗[K] K') L'
(Algebra.TensorProduct.includeRight (x : K'))) ∧
Function.Surjective (PrimeSpectrum.comap f) ∧
∀ q : PrimeSpectrum B',
(Ideal.ResidueField.map (q.asIdeal.comap f) q.asIdeal f rfl).EssFiniteType
Tag 09II, a proposition
Tag 09II in the Stacks Project.
Stacks.EliminateRamification.exists_finite_extension_isSolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/EliminateRamificationTheorem.lean, line 90.
Tag 09II. An essentially finite type extension of discrete valuation rings admits a finite base-field extension which is a solution.
theorem exists_finite_extension_isSolution
(A : Type uA) (B : Type uB) (K : Type uK) (L : Type uL)
[CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
[IsDiscreteValuationRing A] [IsDiscreteValuationRing B] [Field K] [Field L]
[Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L]
[IsScalarTower A B L] [IsScalarTower A K L]
[IsExtension A B] [IsFractionRing A K] [IsFractionRing B L]
[Algebra.EssFiniteType A B] :
∃ (K₁ : Type uK) (_ : Field K₁) (_ : Algebra K K₁) (_ : Algebra A K₁)
(_ : IsScalarTower A K K₁) (_ : Module.Finite K K₁),
∃ D : IntegralClosureBaseChange.{uA, uB, uK, uL, uK, max uL uK, uK, max uL uK}
A B K L K₁,
D.IsSolution.{uA, uB, uK, uL, uK, max uL uK, uK, max uL uK, v}
Tag 0BRP, a lemma
Tag 0BRP in the Stacks Project.
IsDiscreteValuationRing.exists_isSeparableSolution_of_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/EppSeparableSolutionII.lean, line 120.
Let
A → Bbe an extension of discrete valuation rings with fraction fieldsK ⊂ Lsuch thatBis essentially of finite type overA,AorBis a Nagata ring, andL / Kis separable. Then there exists a separable solution forA → B.
theorem exists_isSeparableSolution_of_essFiniteType
(A : Type uA) (B : Type uB) (K : Type uK) (L : Type uL)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
[Field K] [Field L]
[Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L] [Algebra K L]
[IsScalarTower A B L] [IsScalarTower A K L]
[IsExtension A B]
[IsFractionRing A K] [IsFractionRing B L]
[Algebra.EssFiniteType A B]
(hNagata : IsNagataRing A ∨ IsNagataRing B)
(hsep : Algebra.IsSeparableExtension K L) :
∃ (K₁ : Type uK) (_ : Field K₁) (_ : Algebra K K₁) (_ : Algebra A K₁)
(_ : IsScalarTower A K K₁) (_ : Module.Finite K K₁),
∃ D₁ : IntegralClosureBaseChange.{uA, uB, uK, uL, uK,
max uL uK, uK, max uL uK} A B K L K₁,
D₁.IsSeparableSolution.{uA, uB, uK, uL, uK,
max uL uK, uK, max uL uK, max uL uK}
Sources
Section15.119 Picard groups of rings#
Section 15.119 of the Stacks Project, Tag 0AFW. 2 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0B8H, a definition
Tag 0B8H in the Stacks Project.
Module.IsInvertibleModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/Invertible.lean, line 62.
An
R-moduleMis invertible when the functorM ⊗[R] -is an equivalence of the category ofR-modules.
public abbrev Module.IsInvertibleModule
(R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] : Prop
Module.IsTrivialInvertibleModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/Invertible.lean, line 68.
An invertible
R-module is trivial if it is isomorphic toRas anR-module.
public abbrev Module.IsTrivialInvertibleModule
(R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] : Prop
Tag 0B8I, a lemma
Tag 0B8I in the Stacks Project.
Module.finite_projective_rankAtStalk_one_tfae_invertible_exists_tensor_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/Invertible.lean, line 201.
Stacks 0B8I. For an
R-moduleM, the following are equivalent:Mis finite projective of rank one at every prime,Mis invertible, andMadmits a tensor inverse. Moreover, every tensor inverse ofMis isomorphic to the linear dual ofM.
public theorem Module.finite_projective_rankAtStalk_one_tfae_invertible_exists_tensor_inverse
(R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] :
List.TFAE [
Module.Finite R M ∧ Module.Projective R M ∧
Module.rankAtStalk M = Function.const (PrimeSpectrum R) 1,
Module.Invertible R M,
∃ (N : Type (max u v)) (_ : AddCommGroup N) (_ : Module R N),
Nonempty (TensorProduct R M N ≃ₗ[R] R)] ∧
∀ (N : Type w) [AddCommGroup N] [Module R N],
Nonempty (TensorProduct R M N ≃ₗ[R] R) →
Nonempty (N ≃ₗ[R] Module.Dual R M)
Module.isInvertibleModule_iff_invertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/Invertible.lean, line 290.
Stacks 0B8I, the description of invertibility the Stacks Project takes as its definition in Tag 0B8H:
M ⊗[R] -is an equivalence of the category ofR-modules exactly whenMis invertible. Without this,Module.IsInvertibleModuleandModule.Invertibleare two unrelated predicates and the equivalence above is about the wrong condition (2).
public theorem Module.isInvertibleModule_iff_invertible :
Module.IsInvertibleModule R M ↔ Module.Invertible R M
Sources
Section15.120 Determinants#
Section 15.120 of the Stacks Project, Tag 0FJ9. 7 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0FJA, a remark
Tag 0FJA in the Stacks Project.
ProjectiveDeterminant.determinant_submodule_eq_annihilator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/Determinant/Basic/Localization.lean, line 728.
Stacks 0FJA. The determinant line of a finite projective module is the annihilator of the degree-one elements in its exterior algebra.
public theorem determinant_submodule_eq_annihilator (R : Type u) (M : Type v)
[CommRing R] [AddCommGroup M] [Module R M]
[Module.Finite R M] [Module.Projective R M] :
ProjectiveDeterminant.submodule (R := R) (M := M) =
⨅ m : M, LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R m))
Tag 0FJB, a lemma
Tag 0FJB in the Stacks Project.
ProjectiveDeterminant.determinantTensorDeterminantEquiv_of_exact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/Determinant/ShortExact/Construction.lean, line 157. References: SGA 6 X (5.1), “affine case”.
A short exact sequence
0 → M' → M → M'' → 0of finite projective modules has a canonical determinant isomorphism. Its value onx' ⊗ x''is the wedge of the image ofx'with any lift ofx''to the exterior algebra ofM.
public noncomputable def determinantTensorDeterminantEquiv_of_exact
{R : Type u} [CommRing R]
{M' : Type v} {M : Type w} {M'' : Type x}
[AddCommGroup M'] [Module R M'] [Module.Finite R M'] [Module.Projective R M']
[AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M]
[AddCommGroup M''] [Module R M''] [Module.Finite R M''] [Module.Projective R M'']
(f : M' →ₗ[R] M) (g : M →ₗ[R] M'')
(hf : Function.Injective f) (hfg : Function.Exact f g) (hg : Function.Surjective g) :
{ γ : TensorProduct R
(↥(⨅ m : M', LinearMap.ker
(LinearMap.mulLeft R (ExteriorAlgebra.ι R m))))
(↥(⨅ m : M'', LinearMap.ker
(LinearMap.mulLeft R (ExteriorAlgebra.ι R m)))) ≃ₗ[R]
↥(⨅ m : M, LinearMap.ker
(LinearMap.mulLeft R (ExteriorAlgebra.ι R m))) //
∀ (x' : ↥(⨅ m : M', LinearMap.ker
(LinearMap.mulLeft R (ExteriorAlgebra.ι R m))))
(x'' : ↥(⨅ m : M'', LinearMap.ker
(LinearMap.mulLeft R (ExteriorAlgebra.ι R m))))
(y'' : ExteriorAlgebra R M),
ExteriorAlgebra.map g y'' = (x'' : ExteriorAlgebra R M'') →
((γ (x' ⊗ₜ[R] x'') : ↥(⨅ m : M, LinearMap.ker
(LinearMap.mulLeft R (ExteriorAlgebra.ι R m)))) : ExteriorAlgebra R M) =
ExteriorAlgebra.map f (x' : ExteriorAlgebra R M') * y'' }
Tag 0FJC, a lemma
Tag 0FJC in the Stacks Project.
ProjectiveDeterminant.determinantTensorDeterminantEquiv_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/Determinant/ShortExact/Construction.lean, line 364.
The canonical determinant isomorphism of a short exact sequence of finite projective modules is natural under an isomorphism of short exact sequences.
public theorem determinantTensorDeterminantEquiv_naturality
{R : Type u} [CommRing R]
{M' : Type v₁} {M : Type v₂} {M'' : Type v₃}
{K' : Type w₁} {K : Type w₂} {K'' : Type w₃}
[AddCommGroup M'] [Module R M'] [Module.Finite R M'] [Module.Projective R M']
[AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M]
[AddCommGroup M''] [Module R M''] [Module.Finite R M''] [Module.Projective R M'']
[AddCommGroup K'] [Module R K'] [Module.Finite R K'] [Module.Projective R K']
[AddCommGroup K] [Module R K] [Module.Finite R K] [Module.Projective R K]
[AddCommGroup K''] [Module R K''] [Module.Finite R K''] [Module.Projective R K'']
(f : M' →ₗ[R] M) (g : M →ₗ[R] M'')
(fK : K' →ₗ[R] K) (gK : K →ₗ[R] K'')
(hf : Function.Injective f) (hfg : Function.Exact f g) (hg : Function.Surjective g)
(hfK : Function.Injective fK) (hfgK : Function.Exact fK gK)
(hgK : Function.Surjective gK)
(a : M' ≃ₗ[R] K') (b : M ≃ₗ[R] K) (c : M'' ≃ₗ[R] K'')
(hab : ∀ x : M', b (f x) = fK (a x))
(hbc : ∀ x : M, c (g x) = gK (b x)) :
let D_M' : Submodule R (ExteriorAlgebra R M') :=
⨅ x : M', LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R x))
let D_M : Submodule R (ExteriorAlgebra R M) :=
⨅ x : M, LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R x))
let D_M'' : Submodule R (ExteriorAlgebra R M'') :=
⨅ x : M'', LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R x))
let D_K' : Submodule R (ExteriorAlgebra R K') :=
⨅ x : K', LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R x))
let D_K : Submodule R (ExteriorAlgebra R K) :=
⨅ x : K, LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R x))
let D_K'' : Submodule R (ExteriorAlgebra R K'') :=
⨅ x : K'', LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R x))
let γM := (determinantTensorDeterminantEquiv_of_exact f g hf hfg hg).val
let γK := (determinantTensorDeterminantEquiv_of_exact fK gK hfK hfgK hgK).val
Set.BijOn (ExteriorAlgebra.map a)
(D_M' : Set (ExteriorAlgebra R M')) (D_K' : Set (ExteriorAlgebra R K')) ∧
Set.BijOn (ExteriorAlgebra.map b)
(D_M : Set (ExteriorAlgebra R M)) (D_K : Set (ExteriorAlgebra R K)) ∧
Set.BijOn (ExteriorAlgebra.map c)
(D_M'' : Set (ExteriorAlgebra R M'')) (D_K'' : Set (ExteriorAlgebra R K'')) ∧
∀ (x' : D_M') (x'' : D_M'') (y' : D_K') (y'' : D_K''),
ExteriorAlgebra.map a (x' : ExteriorAlgebra R M') =
(y' : ExteriorAlgebra R K') →
ExteriorAlgebra.map c (x'' : ExteriorAlgebra R M'') =
(y'' : ExteriorAlgebra R K'') →
ExteriorAlgebra.map b
((γM (x' ⊗ₜ[R] x'') : D_M) : ExteriorAlgebra R M) =
((γK (y' ⊗ₜ[R] y'') : D_K) : ExteriorAlgebra R K)
Tag 0FJD, a lemma
Tag 0FJD in the Stacks Project.
ProjectiveDeterminant.determinantEquiv_filtration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/Determinant/ShortExact/Filtration.lean, line 94.
For finite projective successive quotients of a filtration
K ≤ L ≤ M, combining the canonical determinant equivalences first acrossK ≤ Lor first across the induced sequenceL / K → M / K → M / Lgives the same equivalence to the determinant line ofM.
public theorem determinantEquiv_filtration
{R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
(K L : Submodule R M) (hKL : K ≤ L)
[Module.Finite R K] [Module.Projective R K]
[Module.Finite R (L ⧸ K.submoduleOf L)]
[Module.Projective R (L ⧸ K.submoduleOf L)]
[Module.Finite R (M ⧸ L)] [Module.Projective R (M ⧸ L)] :
let iQ : (L ⧸ K.submoduleOf L) →ₗ[R] (M ⧸ K) :=
(K.submoduleOf L).mapQ K L.subtype (by
intro x hx
exact hx)
let pQ : (M ⧸ K) →ₗ[R] (M ⧸ L) :=
K.mapQ L LinearMap.id (by simpa using hKL)
∃ hLfin : Module.Finite R L,
∃ hLproj : Module.Projective R L,
∃ hMKfin : Module.Finite R (M ⧸ K),
∃ hMKproj : Module.Projective R (M ⧸ K),
∃ hMfin : Module.Finite R M,
∃ hMproj : Module.Projective R M,
let _ : Module.Finite R L := hLfin
let _ : Module.Projective R L := hLproj
let _ : Module.Finite R (M ⧸ K) := hMKfin
let _ : Module.Projective R (M ⧸ K) := hMKproj
let _ : Module.Finite R M := hMfin
let _ : Module.Projective R M := hMproj
let hiQ : Function.Injective iQ
:= by
intro x y hxy
obtain ⟨x, rfl⟩
Tag 0FJE, a lemma
Tag 0FJE in the Stacks Project.
ProjectiveDeterminant.determinantTensorDeterminantEquiv_prodComm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/Determinant/ShortExact/ProdComm.lean, line 366.
Switching the summands in a direct sum is compatible with the canonical isomorphism from the tensor product of their determinant lines, up to the determinant of minus the identity on the tensor product of the summands.
public theorem determinantTensorDeterminantEquiv_prodComm
{R : Type u} [CommRing R]
(M' : Type v) (M'' : Type w)
[AddCommGroup M'] [Module R M'] [Module.Finite R M'] [Module.Projective R M']
[AddCommGroup M''] [Module R M''] [Module.Finite R M''] [Module.Projective R M''] :
let D' : Submodule R (ExteriorAlgebra R M') :=
⨅ m : M', LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R m))
let D'' : Submodule R (ExteriorAlgebra R M'') :=
⨅ m : M'', LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R m))
let D'_prod_D'' : Submodule R (ExteriorAlgebra R (M' × M'')) :=
⨅ m : M' × M'', LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R m))
let D''_prod_D' : Submodule R (ExteriorAlgebra R (M'' × M')) :=
⨅ m : M'' × M', LinearMap.ker (LinearMap.mulLeft R (ExteriorAlgebra.ι R m))
let γ' := (determinantTensorDeterminantEquiv_of_exact
(LinearMap.inl R M' M'') (LinearMap.snd R M' M'')
LinearMap.inl_injective Function.Exact.inl_snd LinearMap.snd_surjective).val
let γ'' := (determinantTensorDeterminantEquiv_of_exact
(LinearMap.inl R M'' M') (LinearMap.snd R M'' M')
LinearMap.inl_injective Function.Exact.inl_snd LinearMap.snd_surjective).val
∃ ε : Rˣ,
(ε : R) = ProjectiveDeterminant.det
(-(LinearMap.id : TensorProduct R M' M'' →ₗ[R] TensorProduct R M' M'')) ∧
∀ x : TensorProduct R D' D'',
ExteriorAlgebra.map (LinearEquiv.prodComm R M' M'')
((γ' x : D'_prod_D'') : ExteriorAlgebra R (M' × M'')) =
((γ'' ((ε : R) • TensorProduct.comm R D' D'' x) : D''_prod_D') :
ExteriorAlgebra R (M'' × M'))
Tag 0FJF, a lemma
Tag 0FJF in the Stacks Project.
ProjectiveDeterminant.det_one_add_comp_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/Determinant/Basic/Localization.lean, line 782.
Stacks 0FJF. For maps in opposite directions between finite projective modules, the determinants of the identity plus the two possible composites agree.
public theorem det_one_add_comp_comm
{R : Type u} [CommRing R]
{M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M]
{N : Type w} [AddCommGroup N] [Module R N] [Module.Finite R N] [Module.Projective R N]
(a : M →ₗ[R] N) (b : N →ₗ[R] M) :
ProjectiveDeterminant.det (LinearMap.id + a.comp b) =
ProjectiveDeterminant.det (LinearMap.id + b.comp a)
Tag 0AFX, a lemma
Tag 0AFX in the Stacks Project.
K0.exists_determinant_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/Determinant.lean, line 155. References: SGA 6 X (5.1), “affine case”.
Stacks 0AFX. The determinant gives a homomorphism from
K₀(R)to the Picard group. For a finite locally free module of constant rankn, it sends its class to the class of itsnth exterior power.
public theorem K0.exists_determinant_hom (R : Type u) [CommRing R] :
∃ det : K0 R →+ Additive (CommRing.Pic R),
∀ (M : FGProj R) (n : ℕ),
Module.rankAtStalk M.carrier = Function.const (PrimeSpectrum R) n →
∃ h : Module.Invertible R (⋀[R]^n M.carrier),
det (K0.mk M) =
Additive.ofMul (@CommRing.Pic.mk R (⋀[R]^n M.carrier) inferInstance
inferInstance inferInstance h)
Sources
Section15.121 Perfect complexes and K-groups#
Section 15.121 of the Stacks Project, Tag 0FJG. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0AFY, a lemma
Tag 0AFY in the Stacks Project.
K0.exists_eulerChar_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/PerfectComplex.lean, line 675. References: SGA 6 0 (3.1), “special case”.
Stacks 0AFY. Perfect complexes over
Rhave an Euler characteristic inK₀(R)which changes by(-1)ⁿunder a shift byn, is additive in distinguished triangles, and is the alternating sum of the classes of the terms of every bounded finite-projective representative.
public theorem K0.exists_eulerChar_perfect (R : Type u) [CommRing R]
[HasDerivedCategory.{w} (ModuleCat.{u} R)] :
∃ c : {K : DerivedCategory (ModuleCat.{u} R) // StacksDraft.Perfect.IsPerfect K} → K0 R,
(∀ (K : DerivedCategory (ModuleCat.{u} R)) (hK : StacksDraft.Perfect.IsPerfect K) (n : ℤ),
∃ hKn : StacksDraft.Perfect.IsPerfect (K⟦n⟧),
c ⟨K⟦n⟧, hKn⟩ = (n.negOnePow : ℤ) • c ⟨K, hK⟩) ∧
(∀ (T : Triangle (DerivedCategory (ModuleCat.{u} R))),
T ∈ distTriang (DerivedCategory (ModuleCat.{u} R)) →
∀ (h₁ : StacksDraft.Perfect.IsPerfect T.obj₁) (h₂ : StacksDraft.Perfect.IsPerfect T.obj₂)
(h₃ : StacksDraft.Perfect.IsPerfect T.obj₃),
c ⟨T.obj₂, h₂⟩ = c ⟨T.obj₁, h₁⟩ + c ⟨T.obj₃, h₃⟩) ∧
(∀ (K : DerivedCategory (ModuleCat.{u} R)) (hK : StacksDraft.Perfect.IsPerfect K)
(P : CochainComplex (ModuleCat.{u} R) ℤ) (a b : ℤ),
P.IsStrictlyGE a → P.IsStrictlyLE b →
(hfinite : ∀ i : ℤ, Module.Finite R (P.X i)) →
(hprojective : ∀ i : ℤ, Module.Projective R (P.X i)) →
Nonempty (K ≅ DerivedCategory.Q.obj P) →
c ⟨K, hK⟩ = ∑ i ∈ Finset.Icc a b,
(i.negOnePow : ℤ) • K0.mk
({ carrier := P.X i, finite := hfinite i, projective := hprojective i } : FGProj R))
Tag 0FCU, a lemma
Tag 0FCU in the Stacks Project.
K0.exists_k0_perfectDerivedCategory_addEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/PerfectDerivedCategory.lean, line 505.
Stacks 0FCU. Euler characteristic induces an additive equivalence from the zeroth K-group of the perfect derived category of
Rto the zeroth K-group of finite projectiveR-modules. On a bounded finite-projective representative it is the alternating sum of the classes of its terms.
public theorem K0.exists_k0_perfectDerivedCategory_addEquiv (R : Type u) [CommRing R] :
let P : ObjectProperty (DerivedCategory (ModuleCat.{u} R)) :=
(ObjectProperty.singleton
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
(ModuleCat.of R R))).triangEnvelope
∃ e : CategoryTheory.Pretriangulated.K0 P.FullSubcategory ≃+ K0 R,
∀ (K : P.FullSubcategory)
(Q : CochainComplex (ModuleCat.{u} R) ℤ) (a b : ℤ),
Q.IsStrictlyGE a → Q.IsStrictlyLE b →
(hfinite : ∀ i : ℤ, Module.Finite R (Q.X i)) →
(hprojective : ∀ i : ℤ, Module.Projective R (Q.X i)) →
Nonempty (K.obj ≅ DerivedCategory.Q.obj Q) →
e (CategoryTheory.Pretriangulated.K0.cls K) = ∑ i ∈ Finset.Icc a b,
(i.negOnePow : ℤ) • K0.mk
({ carrier := Q.X i, finite := hfinite i, projective := hprojective i } : FGProj R)
Sources
Section15.122 Determinants of endomorphisms of finite length modules#
Section 15.122 of the Stacks Project, Tag 0GSX. 3 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GSY, a lemma
Tag 0GSY in the Stacks Project.
FiniteLengthEndomorphism.det_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FiniteLength/Determinant.lean, line 724. The attribute's comment: “multiplicativity of the residue-field determinant”.
Determinant is multiplicative in an equivariant short exact sequence.
public theorem det_exact (M₁ : Type v₁) (M₂ : Type v₂) (M₃ : Type v₃)
[AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂]
[AddCommGroup M₃] [Module R M₃]
(h₁ : IsFiniteLength R M₁) (h₂ : IsFiniteLength R M₂) (h₃ : IsFiniteLength R M₃)
(φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂) (φ₃ : Module.End R M₃)
(f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (hf : Function.Injective f)
(hexact : Function.Exact f g) (hg : Function.Surjective g)
(hfφ : f.comp φ₁ = φ₂.comp f) (hgφ : g.comp φ₂ = φ₃.comp g) :
det R h₂ φ₂ = det R h₁ φ₁ * det R h₃ φ₃
FiniteLengthEndomorphism.trace_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FiniteLength/Determinant.lean, line 737. The attribute's comment: “additivity of the residue-field trace”.
Trace is additive in an equivariant short exact sequence.
public theorem trace_exact (M₁ : Type v₁) (M₂ : Type v₂) (M₃ : Type v₃)
[AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂]
[AddCommGroup M₃] [Module R M₃]
(h₁ : IsFiniteLength R M₁) (h₂ : IsFiniteLength R M₂) (h₃ : IsFiniteLength R M₃)
(φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂) (φ₃ : Module.End R M₃)
(f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (hf : Function.Injective f)
(hexact : Function.Exact f g) (hg : Function.Surjective g)
(hfφ : f.comp φ₁ = φ₂.comp f) (hgφ : g.comp φ₂ = φ₃.comp g) :
trace R h₂ φ₂ = trace R h₁ φ₁ + trace R h₃ φ₃
FiniteLengthEndomorphism.charpoly_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FiniteLength/Determinant.lean, line 750. The attribute's comment: “multiplicativity of the residue-field characteristic polynomial”.
Characteristic polynomial is multiplicative in an equivariant short exact sequence.
public theorem charpoly_exact (M₁ : Type v₁) (M₂ : Type v₂) (M₃ : Type v₃)
[AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂]
[AddCommGroup M₃] [Module R M₃]
(h₁ : IsFiniteLength R M₁) (h₂ : IsFiniteLength R M₂) (h₃ : IsFiniteLength R M₃)
(φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂) (φ₃ : Module.End R M₃)
(f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (hf : Function.Injective f)
(hexact : Function.Exact f g) (hg : Function.Surjective g)
(hfφ : f.comp φ₁ = φ₂.comp f) (hgφ : g.comp φ₂ = φ₃.comp g) :
charpoly R h₂ φ₂ = charpoly R h₁ φ₁ * charpoly R h₃ φ₃
Tag 0GSZ, a lemma
Tag 0GSZ in the Stacks Project.
FiniteLengthEndomorphism.multiplication_det_eq_norm_pow_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FiniteLength/Determinant.lean, line 926.
For a local homomorphism of local rings with finite residue-field extension, the determinant over the source residue field of multiplication by
uon a finite-length target module is the appropriate power of the residue-field norm ofu.
public theorem multiplication_det_eq_norm_pow_length
(R : Type u) [CommRing R] [IsLocalRing R]
(R' : Type v) [CommRing R'] [IsLocalRing R'] [Algebra R R']
[IsLocalHom (algebraMap R R')]
[Module.Finite (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField R')]
(M' : Type w) [AddCommGroup M'] [Module R M'] [Module R' M'] [IsScalarTower R R' M']
(hM' : IsFiniteLength R' M') (u : R') :
let hM : IsFiniteLength R M' := Module.length_ne_top_iff.mp <| by
rw [IsLocalRing.length_restrictScalars R R' M']
exact WithTop.mul_ne_top (Module.length_ne_top_iff.mpr hM') (by
rw [Module.length_eq_finrank]
exact ENat.natCast_ne_top _)
FiniteLengthEndomorphism.det R hM
((LinearMap.lsmul R' M' u).restrictScalars R) =
Algebra.norm (IsLocalRing.ResidueField R) (IsLocalRing.residue R' u) ^
(Module.length R' M').toNat
Tag 0GT0, a lemma
Tag 0GT0 in the Stacks Project.
FiniteLengthEndomorphism.map_det_pow_eq_det_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FiniteLength/Determinant.lean, line 1324.
Stacks 0GT0. Under a flat local homomorphism
R → Swhose closed fibre has finite lengthm, the determinant of a finite-length module endomorphism after scalar extension is the image in the residue field ofSof the original determinant raised to the powerm.
public theorem map_det_pow_eq_det_baseChange
{R : Type u} {S : Type v} [CommRing R] [CommRing S]
[IsLocalRing R] [IsLocalRing S] [Algebra R S]
[IsLocalHom (algebraMap R S)] [Module.Flat R S]
(m : ℕ)
(hm : Module.length S
(S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)) = m)
{M : Type w} [AddCommGroup M] [Module R M]
(hM : IsFiniteLength R M) (phi : Module.End R M) :
∃ hMS : IsFiniteLength S (S ⊗[R] M),
IsLocalRing.ResidueField.map (algebraMap R S)
(FiniteLengthEndomorphism.det R hM phi ^ m) =
FiniteLengthEndomorphism.det S hMS (LinearMap.baseChange S phi)
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.