mapIso — Mathlib

English

Isomorphisms induce equivalences between subobject lattices: Subobject A ≌ Subobject B.

Русский

Изоморфизм порождает эквивалентность решёток подобъектов: Subobject A ≌ Subobject B.

LaTeX

$$$\mathrm{map} \; (e) : \mathrm{Subobject}(A) \simeq \mathrm{Subobject}(B)$ for $e : A \cong B$$$

Lean4

/-- Isomorphic objects have equivalent subobject lattices. -/
def mapIso {A B : C} (e : A ≅ B) : Subobject A ≌ Subobject B :=
  lowerEquivalence (MonoOver.mapIso e)

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