EtaleFundamentalGroups.exists_integralClosure_integralBase_chosenLocalization_finiteEtale_unique_away
The common normalization has a chosen local factor over the closed point of the integral Henselian base. The prime is produced internally by lying over; finiteness, etaleness, closed-prime uniqueness, and the primitive away property are then supplied by integralClosure_integralBase_chosenLocalization_finiteEtale_unique_away.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe uA uB uLLean source · full declaration
theorem
exists_integralClosure_integralBase_chosenLocalization_finiteEtale_unique_away
{A : Type uA} {B : Type uB} {L : Type uL}
[CommRing A] [CommRing B] [Field L]
[IsNoetherianRing A]
[HenselianLocalRing B]
[Algebra A B] [Module.Finite A B]
[Algebra A L] [Algebra B L] [IsScalarTower A B L]
(hEtale : Algebra.Etale B (integralClosure B L))
(f : A)
(hAway :
(Localization.awayMap
(algebraMap A (integralClosure A L)) f).Etale) :
let C := integralClosure A L
letI : Algebra B C := integralClosureIntegralBaseAlgebra
letI : IsScalarTower A B C :=
integralClosureIntegralBase_isScalarTower
∃ (q : Ideal C) (_ : q.IsPrime)
(_ : q.LiesOver (maximalIdeal B)),
let D := Localization.AtPrime q
Module.Finite B D ∧
Algebra.Etale B D ∧
(maximalIdeal D).LiesOver (maximalIdeal B) ∧
(∀ Q : Ideal D, Q.IsPrime →
Q.LiesOver (maximalIdeal B) → Q = maximalIdeal D) ∧
@Algebra.Etale
(Localization.Away f)
(Localization.Away (algebraMap A D f))
_ _
(Localization.awayMap (algebraMap A D) f).toAlgebra := by
dsimp only
let C := integralClosure A L
let : Algebra B C := integralClosureIntegralBaseAlgebra
let : IsScalarTower A B C :=
integralClosureIntegralBase_isScalarTower
let : Algebra.IsIntegral A C :=
IsIntegralClosure.isIntegral_algebra A L
let : Algebra.IsIntegral B C :=
Algebra.IsIntegral.tower_top A
have hker : RingHom.ker (algebraMap B C) ≤ maximalIdeal B :=
IsLocalRing.le_maximalIdeal (RingHom.ker_ne_top (algebraMap B C))
obtain ⟨q, hqMaximal, hqComap⟩ :=
Ideal.exists_ideal_over_maximal_of_isIntegral (maximalIdeal B) hker
let : q.IsPrime := hqMaximal.isPrime
let : q.LiesOver (maximalIdeal B) :=
(Ideal.liesOver_iff q (maximalIdeal B)).mpr hqComap.symm
exact ⟨q, inferInstance, inferInstance,
integralClosure_integralBase_chosenLocalization_finiteEtale_unique_away
(A := A) (B := B) (L := L) hEtale f hAway q⟩