Theorems · Theorem · algebraic geometry

AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.V (i, j))) {Z : C}
  (h :
    ((TopCat.Presheaf.pushforward C (D.f i k).base).obj (D.V (i, k)).presheaf).obj
        (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f i j)).obj U)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (D.f i j) U)
      (CategoryTheory.CategoryStruct.comp
        ((D.f i k).c.app
          (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f i j)).obj U)))
        h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
          (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))
          ((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).base).1 U))
        (CategoryTheory.CategoryStruct.comp ((D.V (i, k)).presheaf.map (CategoryTheory.eqToHom ⋯)) h))

The red and the blue arrows in  commute.

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category