inclusionMapCompAux — Mathlib

English

Auxiliary construction giving coherent isomorphisms for composing two paths under preinclusion.

Русский

Вспомогательное построение, задающее когерентные изоморфизмы для композиции двух путей под предварительным включением.

LaTeX

$$Definition: inclusionMapCompAux {a b} (f : Path a b) (g : Path b c) ... : (preinclusion _).map (⟨f⟩ ≫ ⟨g⟩) ≅ (preinclusion _).map ⟨f⟩ ≫ (preinclusion _).map ⟨g⟩$$

Lean4

/-- Auxiliary definition for `inclusion`. -/
def inclusionMapCompAux {a b : B} :
    ∀ {c : B} (f : Path a b) (g : Path b c),
      (preinclusion _).map (⟨f⟩ ≫ ⟨g⟩) ≅ (preinclusion _).map ⟨f⟩ ≫ (preinclusion _).map ⟨g⟩
  | _, f, nil => (ρ_ ((preinclusion _).map ⟨f⟩)).symm
  | _, f, cons g₁ g₂ => whiskerRightIso (inclusionMapCompAux f g₁) (Hom.of g₂) ≪≫ α_ _ _ _

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