instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse

English

The inverse equivalence is essentially surjective on objects; every Mat R object is isomorphic to the image of an object from Mat_ (SingleObj (R^op)).

Русский

Обратная эквивалентность существенно сюръективна на объектах; каждый объект в Mat R изоморфен изображению объекта из Mat_(SingleObj (R^op)).

LaTeX

$$EssSurj II$$

Lean4

instance : (equivalenceSingleObjInverse R).EssSurj where
  mem_essImage
    X :=
    ⟨{  ι := X
        X := fun _ => PUnit.unit }, ⟨eqToIso (by cases X; congr)⟩⟩

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