Documentation

Mathlib.AlgebraicGeometry.Sites.EtalePoint

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.

source
theorem AlgebraicGeometry.Scheme.exists_fac_of_etale_of_isSepClosed {X S : Scheme} (f : X ⟶ S) [Etale f] {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec ↧Ω ⟶ S) (x : ↥X) (hx : f x = s default) :
∃ (l : Spec ↧Ω ⟶ X), CategoryTheory.CategoryStruct.comp l f = s ∧ l default = x
source
instance AlgebraicGeometry.Scheme.instIsCofilteredElementsEtaleCompOverForgetObjOppositeFunctorTypeCoyonedaOpMk {S : Scheme} {Ω : Type u} [Field Ω] (s : Spec ↧Ω ⟶ S) :
CategoryTheory.IsCofiltered ((Etale.forget S).comp (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Over.mk s)))).Elements
source
noncomputable def AlgebraicGeometry.Scheme.pointSmallEtale {S : Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec ↧Ω ⟶ 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.
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.pointSmallEtale_fiber {S : Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec ↧Ω ⟶ S) :
    (pointSmallEtale s).fiber = (Etale.forget S).comp (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Over.mk s)))
    source
    noncomputable def AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage {S : Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec ↧Ω ⟶ 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
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_coe {S : Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec ↧Ω ⟶ 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
      source
      instance AlgebraicGeometry.Scheme.instEtaleFiberToSpecResidueField {Y X : Scheme} (f : Y ⟶ X) [Etale f] (x : ↥X) :
      Etale (Hom.fiberToSpecResidueField f x)
      source
      theorem AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_surjective {S : Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec ↧Ω ⟶ S) {s₀ : ↥S} (hs₀ : s default = s₀) (X : S.Etale) :
      Function.Surjective (pointSmallEtaleFiberObjToPreimage s hs₀)
      source
      theorem AlgebraicGeometry.Scheme.isConservative_pointSmallEtale {ι : Type u_1} {S : Scheme} {Ω : ι → Type u} [(i : ι) → Field (Ω i)] [∀ (i : ι), IsSepClosed (Ω i)] (s : (i : ι) → Spec ↧(Ω i) ⟶ S) (hs : ⋃ (i : ι), Set.range ⇑(s i) = Set.univ) :
      (CategoryTheory.ObjectProperty.ofObj fun (i : ι) => pointSmallEtale (s i)).IsConservativeFamilyOfPoints
      source
      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
      source
      instance AlgebraicGeometry.Scheme.instHasEnoughPointsEtaleSmallEtaleTopology {S : Scheme} :
      S.smallEtaleTopology.HasEnoughPoints