Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_coe

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

Defined in

Mathlib.AlgebraicGeometry.Sites.EtalePoint

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldIsSepClosed