functorInclusion_comp_extend — Mathlib

English

Re-statement of extension and amalgamation equivalence in Yoneda context; two-way correspondence.

Русский

Повторное изложение эквивалентности расширения и амальгаммы в контексте Янеды; двусторонняя соответствие.

LaTeX

$$extension_iff_amalgamation (categorical Yoneda context)$$

Lean4

/-- Show that the extension of `f : S.functor ⟶ P` to all of `yoneda.obj X` is in fact an extension,
i.e. that the triangle below commutes, provided `P` is a sheaf for `S`
```
      f
   S  →  P
   ↓  ↗
   yX
```
-/
@[reassoc (attr := simp)]
theorem functorInclusion_comp_extend {P : Cᵒᵖ ⥤ Type v₁} (h : IsSheafFor P S.arrows) (f : S.functor ⟶ P) :
    S.functorInclusion ≫ h.extend f = f :=
  (isSheafFor_iff_yonedaSheafCondition.1 h f).exists.choose_spec

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