toMonObj_injective — Mathlib

English

The map toMonObj is injective on GrpObj morphisms.

Русский

Отображение toMonObj инъективно на морфизмах между объектами группы.

LaTeX

$$$ToMonObj\;\text{injective}$$$

Lean4

theorem toMonObj_injective {X : C} : Function.Injective (@GrpObj.toMonObj C ‹_› ‹_› X) :=
  by
  intro h₁ h₂ e
  suffices h₁.inv = h₂.inv by cases h₁; congr!
  apply lift_left_mul_ext (𝟙 _)
  rw [left_inv]
  convert @left_inv _ _ _ _ h₁ using 2
  exacts [congr(($e.symm).mul), congr(($e.symm).one)]

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