congrHom_inv — Mathlib

English

The inverse of the congruent pullback Hom is given by a pullback.map with identities on bears and the appropriate simp refinements.

Русский

Обратный конгруентный гомоморфизм пулабэка задаётся через map с тождественными на переменных и соответствующими упрощениями.

LaTeX

$$$(\mathrm{pullback.congrHom} h_1 h_2)^{-1} = \mathrm{pullback.map} \_ \_ \_ \_ (\mathbf{1}) (\mathbf{1}) (\mathbf{1}) (by\ simp[ h_1 ]) (by\ simp[ h_2 ])$$$

Lean4

@[simp]
theorem congrHom_inv {X Y Z : C} {f₁ f₂ : X ⟶ Z} {g₁ g₂ : Y ⟶ Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [HasPullback f₁ g₁]
    [HasPullback f₂ g₂] :
    (pullback.congrHom h₁ h₂).inv = pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simp [h₁]) (by simp [h₂]) := by
  ext <;> simp [Iso.inv_comp_eq]

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