Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage

{S : AlgebraicGeometry.Scheme} →
  {Ω : Type u} →
    [inst : Field Ω] →
      [inst_1 : IsSepClosed Ω] →
        (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) →
          {s₀ : ↥S} →
            s default = s₀ →
              {X : S.Etale} → (AlgebraicGeometry.Scheme.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.

Defined in

Mathlib.AlgebraicGeometry.Sites.EtalePoint

Cited by

4 results in Mathlib

Foundations

Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldIsSepClosed