Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.exists_fac_of_etale_of_isSepClosed

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

Defined in

Mathlib.AlgebraicGeometry.Sites.EtalePoint

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.EtaleFieldIsSepClosed