AlgebraicGeometry.Scheme.EffectiveCartierDivisor.galoisPullback_componentGenericPoint_chart
Geometry and an affine principal chart at the canonical generic point of a pulled-back arithmetic boundary component. Neither the point nor the chart is supplied as an additional hypothesis.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
universe u
variable {X S : Scheme.{u}}Lean source · full declaration
theorem galoisPullback_componentGenericPoint_chart
[IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X] [IsIntegral S]
(D : EffectiveCartierDivisor X) (p : X ⟶ S)
(hD : D.SatisfiesResidueCharacteristicTwoBoundaryCondition p)
(Y : FiniteEtale X) (hY : CategoryTheory.PreGaloisCategory.IsGalois Y)
(Z : Set (D.1.comap Y.hom).subscheme)
(hZ : Z ∈ irreducibleComponents (D.1.comap Y.hom).subscheme) :
let I : Y.left.IdealSheafData := D.1.comap Y.hom
let C := I.subscheme.reducedIrreducibleComponent Z hZ
let x := I.componentGenericPoint Z hZ
Y.left.IsRegularAt x ∧
Order.coheight x = 1 ∧
I.componentToBase (Y.hom ≫ p) Z hZ (genericPoint C) = genericPoint S ∧
GeometricallyIntegral
((I.componentToBase (Y.hom ≫ p) Z hZ).fiberToSpecResidueField
(genericPoint S)) ∧
∃ (U : Y.left.affineOpens) (_hx : x ∈ U.1) (f : Γ(Y.left, U.1)),
IsRegular f ∧ I.ideal U = Ideal.span {f} := by
let : CategoryTheory.PreGaloisCategory.IsGalois Y := hY
let : IsIntegral Y.left :=
EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale Y
let : IsLocallyNoetherian Y.left :=
EtaleFundamentalGroups.isLocallyNoetherian_left_finiteEtale Y
let D' : EffectiveCartierDivisor Y.left := D.comapFiniteEtale Y
have hstable := D.galoisPullback_stability p hD Y hY
dsimp only at hstable
let I : Y.left.IdealSheafData := D.1.comap Y.hom
let C := I.subscheme.reducedIrreducibleComponent Z hZ
let x := I.componentGenericPoint Z hZ
change Y.left.IsRegularAt x ∧
Order.coheight x = 1 ∧
I.componentToBase (Y.hom ≫ p) Z hZ (genericPoint C) = genericPoint S ∧
GeometricallyIntegral
((I.componentToBase (Y.hom ≫ p) Z hZ).fiberToSpecResidueField
(genericPoint S)) ∧
∃ (U : Y.left.affineOpens) (_hx : x ∈ U.1) (f : Γ(Y.left, U.1)),
IsRegular f ∧ I.ideal U = Ideal.span {f}
rcases hstable with ⟨_reduced, hhorizontal, hregular, hcomponents⟩
refine ⟨hregular.isRegularAt_componentGenericPoint Z hZ,
D'.2.coheight_componentGenericPoint_eq_one Z hZ, ?_,
(hcomponents Z hZ).1, ?_⟩
· exact I.componentToBase_genericPoint (Y.hom ≫ p) Z hZ
(hhorizontal Z hZ)
· exact D'.2.exists_affineChart_at_componentGenericPoint Z hZ