EtaleCohomology.etalePullbackClosedFiberUnit_zariskiStalk_mono
Pulling the original closed-fiber unit along an arbitrary scheme map keeps its Zariski stalk map injective at all points over the closed point.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomologyLean source · full declaration
theorem etalePullbackClosedFiberUnit_zariskiStalk_mono
(R : Type u) [CommRing R] [IsLocalRing R]
{X Y : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) (q : Y ⟶ X)
(Λ : Type u) [CommRing Λ] (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ))
(y : Y) (hy : f (q y) = IsLocalRing.closedPoint R) :
let r : Spec (CommRingCat.of (IsLocalRing.ResidueField R)) ⟶ Spec (CommRingCat.of R) :=
Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))
let i : pullback f r ⟶ X := pullback.fst f r
let η : F ⟶ (etalePushforward i Λ).obj ((etalePullback i Λ).obj F) :=
(etalePullbackPushforwardAdjunction i Λ).unit.app F
Mono ((TopCat.Presheaf.stalkFunctor (Type u) y).map
((etaleModuleZariskiRestriction Y Λ).map ((etalePullback q Λ).map η)).hom) := by
intro r i η
have : IsClosedImmersion r := IsClosedImmersion.spec_of_surjective
(CommRingCat.ofHom (IsLocalRing.residue R)) IsLocalRing.residue_surjective
have : IsClosedImmersion i := inferInstanceAs (IsClosedImmersion (pullback.fst f r))
let Ω : Type u := SeparableClosure (Y.residueField y)
let s : Spec (CommRingCat.of Ω) ⟶ Y :=
Spec.map (CommRingCat.ofHom (algebraMap (Y.residueField y) Ω)) ≫
Y.fromSpecResidueField y
let ξ : Spec (CommRingCat.of Ω) := default
have hs : s ξ = y := by
rw [Scheme.Hom.comp_apply]
exact Scheme.fromSpecResidueField_apply y _
let x₀ : Spec (CommRingCat.of (IsLocalRing.ResidueField R)) := default
have hr : r x₀ = IsLocalRing.closedPoint R :=
IsLocalRing.PrimeSpectrum.comap_residue R x₀
have hRange : Set.range (s ≫ q) ⊆ Set.range i := by
rintro x ⟨t, rfl⟩
have ht : s t = y := (congrArg s (Subsingleton.elim t ξ)).trans hs
have hbase : f ((s ≫ q) t) = r x₀ :=
(congrArg f ((Scheme.Hom.comp_apply s q t).trans (congrArg q ht))).trans
(hy.trans hr.symm)
obtain ⟨z, hzi, _⟩ := Scheme.Pullback.exists_preimage_pullback
(f := f) (g := r) ((s ≫ q) t) x₀ hbase
exact ⟨z, hzi⟩
obtain ⟨sZ, hsZ⟩ := IsClosedImmersion.exists_lift_of_isReduced_of_range_subset
i (s ≫ q) hRange
have hη : IsIso ((Scheme.pointSmallEtale (s ≫ q)).sheafFiber.map η) := by
rw [← hsZ]
exact etalePushforwardClosed_unit_stalk_isIso i Λ sZ F
let μ := (etalePullback q Λ).map η
let Φ := Scheme.pointSmallEtale s
have hμ : IsIso (Φ.sheafFiber.map μ) :=
(NatIso.isIso_map_iff (etalePullbackStalkIso q s Λ) η).mpr hη
let μ₀ := (etaleModuleUnderlying Y Λ).map μ
have hμ₀ : IsIso (Φ.sheafFiber.map μ₀) :=
(NatIso.isIso_map_iff (Φ.sheafFiberCompIso (forget (ModuleCat.{u} Λ))) μ).mpr
(inferInstanceAs (IsIso ((forget (ModuleCat.{u} Λ)).map (Φ.sheafFiber.map μ))))
have : Mono (Φ.presheafFiber.map μ₀.hom) := inferInstanceAs (Mono (Φ.sheafFiber.map μ₀))
rw [← hs]
exact etaleZariski_stalk_map_mono_of_geometric s ξ μ₀