EtaleFundamentalGroups.restrict_punctured_finiteEtale_bijective
Hartogs extension for the actual punctured open of a finite étale cover.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory TopologicalSpace AlgebraicGeometry IsLocalRing
namespace EtaleFundamentalGroups
universe uLean source · full declaration
theorem restrict_punctured_finiteEtale_bijective
(R : Type u) [CommRing R] [IsDomain R] [IsRegularLocalRing R]
(hdim : 2 ≤ ringKrullDim R)
{X : Scheme.{u}} (p : X ⟶ Spec (.of R)) [IsFiniteEtale p] :
Function.Bijective (X.presheaf.map
(homOfLE (show p ⁻¹ᵁ Scheme.puncturedSpectrumOpen R ≤ ⊤ from le_top)).op) := by
let : IsAffine X := isAffine_of_isAffineHom p
let : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian p
let : IsNoetherianRing Γ(X, ⊤) :=
IsLocallyNoetherian.component_noetherian ⟨⊤, isAffineOpen_top X⟩
let : NoetherianSpace X := noetherianSpace_of_isAffine (X := X)
let c : CommRingCat.of R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (.of R)).inv ≫ p.appTop
let : Algebra R Γ(X, ⊤) := c.hom.toAlgebra
let : Module.Flat R Γ(X, ⊤) :=
(RingHom.Flat.of_bijective
(ConcreteCategory.bijective_of_isIso (Scheme.ΓSpecIso (.of R)).inv)).comp
p.flat_appTop
obtain ⟨x, y, hxmem, hymem, hx, hy, hxy⟩ :=
exists_primePair_of_isRegularLocalRing R hdim
have hbasic {r : R} (hr : r ∈ maximalIdeal R) :
X.basicOpen (algebraMap R Γ(X, ⊤) r) ≤
p ⁻¹ᵁ Scheme.puncturedSpectrumOpen R := by
change X.basicOpen (p.appTop ((Scheme.ΓSpecIso (.of R)).inv r)) ≤ _
rw [← Scheme.preimage_basicOpen_top, basicOpen_eq_of_affine]
apply Scheme.Hom.preimage_mono p
intro q hq
apply (Scheme.mem_puncturedSpectrumOpen_iff R q).mpr
intro hqclosed
subst q
exact hq hr
apply restrict_bijective_of_primePair X hx hy hxy
(p ⁻¹ᵁ Scheme.puncturedSpectrumOpen R)
(NoetherianSpace.isCompact _) ?_ (hbasic hxmem) (hbasic hymem)
intro A B _ _ _ _ _ _
exact NoetherianSpace.isCompact _