isoOfMkEq — Mathlib

English

From mk f = X one obtains an isomorphism between the subobject X and the object A.

Русский

Из mk f = X следует изоморфизм между подобъектом X и объектом A.

LaTeX

$$$\text{isoOfMkEqMk } f X h : X \cong A$$$

Lean4

/-- An equality of subobjects gives an isomorphism of the corresponding objects. -/
@[simps]
def isoOfMkEq {B A : C} (f : A ⟶ B) [Mono f] (X : Subobject B) (h : mk f = X) : A ≅ (X : C)
    where
  hom := ofMkLE f X h.le
  inv := ofLEMk X f h.ge

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