Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map

Deprecated since 2026-02-01Use AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map instead.

∀ {X : AlgebraicGeometry.Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat)
  (α : (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf ⟶ F)
  (H : CategoryTheory.NatTrans.Coequifibered α) {U : X.AffineZariskiSite} (r : ↑(X.presheaf.obj (Opposite.op ↑U))),
  AlgebraicGeometry.Scheme.Hom.opensRange
      ((AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData H).functor.map (CategoryTheory.homOfLE ⋯)) =
    PrimeSpectrum.basicOpen ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op U))) r)

Alias of AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map.

Defined in

Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Cited by

0 results in Mathlib

Foundations

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