hom_inv_hom — Mathlib

English

For any isomorphism of actions, the composite of the forward and inverse maps is the identity on the source.

Русский

Для изоморфизма действий композиция прямого и обратного отображения равна тождественному отображению на исходном объекте.

LaTeX

$$$\\text{hom\_inv\_hom} : f:\\ M \\cong N \\Rightarrow f.hom.hom \\circ f.inv.hom = \\mathrm{id}_{M.V}$$$

Lean4

@[reassoc (attr := simp)]
theorem hom_inv_hom {M N : Action V G} (f : M ≅ N) : f.hom.hom ≫ f.inv.hom = 𝟙 M.V := by
  rw [← comp_hom, Iso.hom_inv_id, id_hom]

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