Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.pointSmallEtale

{S : AlgebraicGeometry.Scheme} →
  {Ω : Type u} →
    [inst : Field Ω] → [IsSepClosed Ω] → (AlgebraicGeometry.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.

Defined in

Mathlib.AlgebraicGeometry.Sites.EtalePoint

Cited by

7 results in Mathlib

Foundations

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

Assumes

FieldIsSepClosed