EtaleFundamentalGroups.StrictHenselian.inertiaInvariantPrimeLocalization_exists_geometricStalk_preimage
Every element of the original inertia-invariant prime localization has an actual preimage under the geometric-stalk map to the normalization prime localization. The strict target and its separably closed residue field are supplied by the original separably closed ambient field.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
normalizationInertiaCoefficientCommClass inertiaInvariantPrime_isPrime
finiteLevelInertiaPrime_isPrimeLean source · full declaration
theorem inertiaInvariantPrimeLocalization_exists_geometricStalk_preimage
(A : Type u) (K : Type v) (L : Type u)
[CommRing A] [IsDomain A] [IsIntegrallyClosed A] [Field K] [Field L]
[Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
[IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
(Q : Ideal (integralClosure A L)) [Q.IsPrime]
(z : inertiaInvariantPrimeLocalizationAlgebra A K L Q) :
let : HenselianLocalRing (Localization.AtPrime Q) :=
(integralClosure_localizationAtPrime_strictHenselian A K L Q).1
let : IsSepClosed (IsLocalRing.ResidueField (Localization.AtPrime Q)) :=
(integralClosure_localizationAtPrime_strictHenselian A K L Q).2
∃ a : geometricStalk (Spec.map (CommRingCat.ofHom
((IsLocalRing.residue (Localization.AtPrime Q)).comp
(integralClosurePrimeBaseMap A L Q)))),
geometricStalkToHenselian (integralClosurePrimeBaseMap A L Q) a =
inertiaInvariantPrimeLocalizationMap A K L Q z := by
intro actualHenselian actualSepClosed
obtain ⟨X, x, hx⟩ := Concrete.isColimit_exists_rep
(finiteLevelEtaleDiagram A K L Q ⋙ forget₂ (CommAlgCat.{u} A) (AlgCat.{u} A))
(finiteLevelEtaleCoconeIsColimit A K L Q) z
let B : CommAlgCat.{u} A := (finiteLevelEtaleDiagram A K L Q).obj X
let U : CommAlgCat.{u} A := inertiaInvariantPrimeLocalizationAlgebra A K L Q
let j : B →ₐ[A] U := finiteLevelEtaleNeighborhoodInclusion A K L Q X
have hjx : j x = z := hx
have : Algebra.Etale A B := X.etale
let g : B →+* Localization.AtPrime Q :=
(inertiaInvariantPrimeLocalizationMap A K L Q).comp j.toRingHom
have hupper : (inertiaInvariantPrimeLocalizationMap A K L Q).comp
(algebraMap A U) = integralClosurePrimeBaseMap A L Q :=
(congrArg
(fun c : A →+* U => (inertiaInvariantPrimeLocalizationMap A K L Q).comp c)
(inertiaInvariantPrimeLocalizationBaseMap_eq_algebraMap A K L Q)).symm.trans
(inertiaInvariantPrimeLocalizationMap_comp_base A K L Q)
have hbase : g.comp (algebraMap A B) = integralClosurePrimeBaseMap A L Q :=
(RingHom.comp_assoc (algebraMap A B) j.toRingHom
(inertiaInvariantPrimeLocalizationMap A K L Q)).trans
((congrArg
(fun c : A →+* U => (inertiaInvariantPrimeLocalizationMap A K L Q).comp c)
j.comp_algebraMap).trans hupper)
obtain ⟨a, ha⟩ := geometricStalkToHenselian_exists_preimage_of_etale
(integralClosurePrimeBaseMap A L Q) g hbase x
exact ⟨a, ha.trans (congrArg (inertiaInvariantPrimeLocalizationMap A K L Q) hjx)⟩