Theorems · Theorem · algebraic geometry

AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt

∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.LocallyOfFiniteType f]
  [AlgebraicGeometry.IsSeparated f] {x : ↥X} {s : ↥S},
  f x = s →
    AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x →
      ∃ U g,
        AlgebraicGeometry.Etale g ∧
          s ∈ Set.range ⇑g ∧
            ∃ V W v,
              IsCompl V W ∧
                AlgebraicGeometry.IsFinite
                    (CategoryTheory.CategoryStruct.comp V.ι (CategoryTheory.Limits.pullback.snd f g)) ∧
                  (CategoryTheory.Limits.pullback.fst f g) ↑v = x

Defined in

Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.LocallyOfFiniteTypeAlgebraicGeometry.IsSeparated