Theorems · Theorem · algebraic geometry

AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc

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

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasLimits