Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isOpenImmersion

Deprecated since 2026-02-01Mathlib marks this declaration as deprecated.

∀ {X : AlgebraicGeometry.Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat)
  (α : (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf ⟶ F),
  CategoryTheory.NatTrans.Coequifibered α →
    ∀ ⦃U V : X.AffineZariskiSite⦄ (f : U ⟶ V),
      AlgebraicGeometry.IsOpenImmersion ((F.rightOp.comp AlgebraicGeometry.Scheme.Spec).map f)

Defined in

Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Cited by

0 results in Mathlib

Foundations

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