Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.isConservative_pointSmallEtale

∀ {ι : Type u_1} {S : AlgebraicGeometry.Scheme} {Ω : ι → Type u} [inst : (i : ι) → Field (Ω i)]
  [inst_1 : ∀ (i : ι), IsSepClosed (Ω i)] (s : (i : ι) → AlgebraicGeometry.Spec (CommRingCat.of (Ω i)) ⟶ S),
  ⋃ i, Set.range ⇑(s i) = Set.univ →
    (CategoryTheory.ObjectProperty.ofObj fun i =>
        AlgebraicGeometry.Scheme.pointSmallEtale (s i)).IsConservativeFamilyOfPoints

Defined in

Mathlib.AlgebraicGeometry.Sites.EtalePoint

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldIsSepClosed