Yamaguchi26SolvableCoverings.boundaryUnramified_fractionPullback_normalization_etale
The normalization of the entire fraction-stalk pullback is étale over the generic boundary DVR, without selecting a component in the conclusion.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory AlgebraicGeometry.FiniteEtale
open EtaleFundamentalGroups.Inertia
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]
(D : X.EffectiveCartierDivisor) (E : Component D)
[IsDomain (X.presheaf.stalk (componentPoint D E))]
[IsDiscreteValuationRing (X.presheaf.stalk (componentPoint D E))]
[ConnectedSpace D.1.supportComplement]
local notation "R" => X.presheaf.stalk (componentPoint D E)
local notation "K" => FractionRing R
local notation "c" =>
Scheme.IdealSheafData.IsEffectiveCartier.fractionStalkToSupportComplement
(Subtype.property D) (componentPoint D E)
local notation "a₀" => Spec.map (CommRingCat.ofHom (algebraMap R K))Lean source · full declaration
theorem boundaryUnramified_fractionPullback_normalization_etale
(W : FiniteEtale D.1.supportComplement) (hW : IsGalois W)
(hU : IsBoundaryUnramified D W) :
Etale (((show ((FiniteEtale.pullback c).obj W).left ⟶ Spec (.of K) from
((FiniteEtale.pullback c).obj W).hom) ≫ a₀).fromNormalization) := by
let xi : Spec (.of (AlgebraicClosure K)) ⟶ Spec (.of K) :=
Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
let A := (FiniteEtale.pullback c).obj W
let f : A.left ⟶ Spec (.of R) := (show A.left ⟶ Spec (.of K) from A.hom) ≫ a₀
apply etale_normalization_of_galoisComponents c xi W hW f
intro w Z i v hiv hZ hi
have hZet : Etale (((show Z.left ⟶ Spec (.of K) from Z.hom) ≫ a₀).fromNormalization) :=
boundaryUnramified_localComponent_normalization_etale D E xi W hW hU w Z i v hiv hZ hi
have hiw : i.left ≫ (show A.left ⟶ Spec (.of K) from A.hom) =
(show Z.left ⟶ Spec (.of K) from Z.hom) := i.w
have he : (Iso.refl Z.left).hom ≫ ((show Z.left ⟶ Spec (.of K) from Z.hom) ≫ a₀) =
i.left ≫ f := by
exact (Category.id_comp _).trans
((congrArg (fun k => k ≫ a₀) hiw).symm.trans (Category.assoc _ _ _))
let e := normalizationSourceIso (i.left ≫ f)
((show Z.left ⟶ Spec (.of K) from Z.hom) ≫ a₀) (Iso.refl Z.left) he
have ht : Etale (e.hom ≫ ((show Z.left ⟶ Spec (.of K) from Z.hom) ≫ a₀).fromNormalization) :=
inferInstance
rw [normalizationSourceIso_hom_fromNormalization] at ht
exact ht