comp — Mathlib

English

The induced map with identity base yields the identity morphism on the domain.

Русский

Индукционное отображение с надлежащим тождественным основанием даёт единицу на области определения.

LaTeX

$$$map(p,f,φ,(id\\_comp f).symm,φ) = 𝟙_a$$$

Lean4

/-- Given two strongly Cartesian morphisms `φ`, `ψ` as follows
```
a --φ--> b --ψ--> c
|        |        |
v        v        v
R --f--> S --g--> T
```
Then the composite `φ ≫ ψ` is also strongly Cartesian. -/
instance comp [IsStronglyCartesian p f φ] [IsStronglyCartesian p g ψ] : IsStronglyCartesian p (f ≫ g) (φ ≫ ψ) where
  universal_property' := by
    intro a' h τ hτ
    use map p f φ (f' := h ≫ f) rfl (map p g ψ (assoc h f g).symm τ)
    refine ⟨⟨inferInstance, ?_⟩, ?_⟩
    · rw [← assoc, fac, fac]
    · intro π' ⟨hπ'₁, hπ'₂⟩
      apply map_uniq
      apply map_uniq
      simp only [assoc, hπ'₂]

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