Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.appIso_hom_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 (Y.presheaf.map ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).map i.unop).op)
      (AlgebraicGeometry.Scheme.Hom.appIso f V).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).hom (X.presheaf.map i)

Defined in

Mathlib.AlgebraicGeometry.OpenImmersion

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsOpenImmersion