Theorems · Theorem · algebraic geometry

AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app

∀ {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))),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (D.f i j) U)
      ((D.f i k).c.app
        (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f i j)).obj U))) =
    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))
          (Opposite.unop
            (Opposite.op
              ((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).base).1
                (Opposite.unop (Opposite.op U))))))
        ((D.V (i, k)).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