ofEpiOfIsIsoOfMono_p — Mathlib

English

For h a RightHomologyData of S1 and φ: S1 ⟶ S2 with epi τ1, iso τ2, mono τ3, the p-component of the constructed data satisfies (ofEpiOfIsIsoOfMono φ h).p = inv(φ.τ₂) ∘ h.p.

Русский

Для h — RightHomologyData S1 и морфизма φ: S1 ⟶ S2 с epi τ1, изоморфизмом τ2 и моно τ3 выполняется: (ofEpiOfIsIsoOfMono φ h).p = inv(φ.τ₂) ∘ h.p.

LaTeX

$$$ (\\mathrm{ofEpiOfIsIsoOfMono}\\ φ\ \\, h).p = (\\phi.\\tau_2)^{-1} \\circ h.p $$$

Lean4

@[simp]
theorem ofEpiOfIsIsoOfMono_p : (ofEpiOfIsIsoOfMono φ h).p = inv φ.τ₂ ≫ h.p := by simp [ofEpiOfIsIsoOfMono, opMap]

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