isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff

English

Analogous result for the same amalgamation property in the presieve FamilyOfElements.

Русский

Аналогичный результат для того же свойства амальгамации в семействе элементов пресева.

LaTeX

$$$((\mathrm{localPreimage}\phi\ r').map\ \phi).IsAmalgamation\ r'$$$

Lean4

theorem isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff [HasWeakSheafify J (Type v)] (F : Sheaf J (Type v))
    (sq : Square C) :
    (sq.op.map ((yoneda ⋙ presheafToSheaf J _).op ⋙ yoneda.obj F)).IsPullback ↔ (sq.op.map F.val).IsPullback :=
  by
  refine
    Square.IsPullback.iff_of_equiv _ _ (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
      (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
      (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
      (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv) ?_ ?_ ?_ ?_
  all_goals
    ext x
    dsimp
    rw [yonedaEquiv_naturality]
    erw [Adjunction.homEquiv_naturality_left]
    rfl

Похожие утверждения