isGluing_iff_pairwise — Mathlib

English

A gluing condition for a compatible family sf is equivalent to the projection equalities to the pairwise components for all indices in the Pairwise diagram.

Русский

Условие слепления для совместимой семьи sf эквивалентно равенствам проекций к парным компонентам для всех индексов диаграммы Pairwise.

LaTeX

$$$$\text{IsGluing } F\, U\, sf\, s \;\iff\; \forall i,\ (F.mapCone (Pairwise.cocone U).op).\pi.app i\, s = objPairwiseOfFamily\ sf\ i.$$$$

Lean4

theorem isGluing_iff_pairwise {sf s} :
    IsGluing F U sf s ↔ ∀ i, (F.mapCone (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i :=
  by
  refine ⟨fun h ↦ ?_, fun h i ↦ h (op <| Pairwise.single i)⟩
  rintro (i | ⟨i, j⟩)
  · exact h i
  · rw [← (F.mapCone (Pairwise.cocone U).op).w (op <| Pairwise.Hom.left i j)]
    exact congr_arg _ (h i)

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