Points of the étale site

In this file, we show that a morphism Spec (.of Ω) ⟶ S where Ω is a separably closed field defines a point on the small étale site of S. We show that these points form a conservative family.

theorem AlgebraicGeometry.Scheme.exists_fac_of_etale_of_isSepClosed {X S : Scheme} (f : X ⟶ S) [Etale f] {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (CommRingCat.of Ω) ⟶ S) (x : ↥X) (hx : f x = s default) : ∃ (l : Spec (CommRingCat.of Ω) ⟶ X), CategoryTheory.CategoryStruct.comp l f = s ∧ l default = x

instance AlgebraicGeometry.Scheme.instIsCofilteredElementsEtaleCompOverForgetObjOppositeFunctorTypeCoyonedaOpMk {S : Scheme} {Ω : Type u} [Field Ω] (s : Spec (CommRingCat.of Ω) ⟶ S) : CategoryTheory.IsCofiltered ((Etale.forget S).comp (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Over.mk s)))).Elements

noncomputable def AlgebraicGeometry.Scheme.pointSmallEtale {S : Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (CommRingCat.of Ω) ⟶ S) : S.smallEtaleTopology.Point

A morphism s : Spec (.of Ω) ⟶ S where Ω is a separably closed field defines a point for the small étale site of S.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.pointSmallEtale_fiber {S : Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (CommRingCat.of Ω) ⟶ S) : (pointSmallEtale s).fiber = (Etale.forget S).comp (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Over.mk s)))

noncomputable def AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage {S : Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (CommRingCat.of Ω) ⟶ S) {s₀ : ↥S} (hs₀ : s default = s₀) {X : S.Etale} (t : (pointSmallEtale s).fiber.obj X) : ↑(⇑X.hom ⁻¹' {s₀})

Given a morphism s : Spec (.of Ω) ⟶ S with image s₀ : S where Ω is a separably closed field, this is the canonical map (pointSmallEtale s).fiber.obj X ⟶ X.hom ⁻¹' {s₀} for X : S.Etale.

Equations

• AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage s hs₀ t = ⟨(CategoryTheory.Over.Hom.left t) default, ⋯⟩

@[simp]

theorem AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_coe {S : Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (CommRingCat.of Ω) ⟶ S) {s₀ : ↥S} (hs₀ : s default = s₀) {X : S.Etale} (t : (pointSmallEtale s).fiber.obj X) : ↑(pointSmallEtaleFiberObjToPreimage s hs₀ t) = (CategoryTheory.Over.Hom.left t) default

instance AlgebraicGeometry.Scheme.instEtaleFiberToSpecResidueField {Y X : Scheme} (f : Y ⟶ X) [Etale f] (x : ↥X) : Etale (Hom.fiberToSpecResidueField f x)

theorem AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_surjective {S : Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (CommRingCat.of Ω) ⟶ S) {s₀ : ↥S} (hs₀ : s default = s₀) (X : S.Etale) : Function.Surjective (pointSmallEtaleFiberObjToPreimage s hs₀)

theorem AlgebraicGeometry.Scheme.isConservative_pointSmallEtale {ι : Type u_1} {S : Scheme} {Ω : ι → Type u} [(i : ι) → Field (Ω i)] [∀ (i : ι), IsSepClosed (Ω i)] (s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S) (hs : ⋃ (i : ι), Set.range ⇑(s i) = Set.univ) : (CategoryTheory.ObjectProperty.ofObj fun (i : ι) => pointSmallEtale (s i)).IsConservativeFamilyOfPoints

theorem AlgebraicGeometry.Scheme.isConservativeFamilyOfPoints_pointSmallEtale' (S : Scheme) : (CategoryTheory.ObjectProperty.ofObj fun (s : ↥S) => pointSmallEtale ((SpecToEquivOfField (SeparableClosure ↑(S.residueField s)) S).invFun ⟨s, CommRingCat.ofHom (algebraMap (↑(S.residueField s)) (SeparableClosure ↑(S.residueField s)))⟩)).IsConservativeFamilyOfPoints

instance AlgebraicGeometry.Scheme.instHasEnoughPointsEtaleSmallEtaleTopology {S : Scheme} : S.smallEtaleTopology.HasEnoughPoints