hom_inv_apply — Mathlib

English

Let e: R ≅ S be an isomorphism in the category of commutative semirings. Then for every s ∈ S, applying the inverse morphism and then the forward morphism returns s; equivalently, e.hom ∘ e.inv = id_S.

Русский

Пусть e: R ≅ S есть изоморфизм в категории коммутативных полукольц. Тогда для каждого s ∈ S выполняется e.hom(e.inv(s)) = s; эквивалентно e.hom ∘ e.inv = id_S.

LaTeX

$$$e\colon R \cong S$ implies e_{hom}(e_{inv}(s)) = s \quad (\text{for all } s \in S).$$$

Lean4

theorem hom_inv_apply {R S : CommSemiRingCat} (e : R ≅ S) (s : S) : e.hom (e.inv s) = s := by simp

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