isMultiplicative — Mathlib

English

The property of relative representability is closed under composition and has base cases with identity morphisms.

Русский

Свойство относительной представимой сохраняется при композиции и содержит тождественные морфизмы как базовый случай.

LaTeX

$$$ F.relativelyRepresentable.IsMultiplicative $$$

Lean4

instance isMultiplicative : IsMultiplicative F.relativelyRepresentable
    where
  id_mem _ := of_isIso F _
  comp_mem {F G H} f g hf
    hg := fun X h ↦
    ⟨hf.pullback (hg.fst h), hf.snd (hg.fst h) ≫ hg.snd h, hf.fst (hg.fst h), by
      simpa using IsPullback.paste_vert (hf.isPullback (hg.fst h)) (hg.isPullback h)⟩

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