Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens}
  (i : Opposite.op U ⟶ Opposite.op V),
  CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (AlgebraicGeometry.Scheme.Hom.appIso f V).inv =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).inv
      (Y.presheaf.map ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).op.map i))

Defined in

Mathlib.AlgebraicGeometry.OpenImmersion

Cited by

4 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsOpenImmersion