Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) {Z : CommRingCat}
  (h :
    Y.presheaf.obj
        (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.appIso f ((TopologicalSpace.Opens.map f.base).obj U)).inv h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

Defined in

Mathlib.AlgebraicGeometry.OpenImmersion

Cited by

2 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsOpenImmersion