Theorems · Theorem · algebraic geometry

AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app

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

The red and the blue arrows in  commute.

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category