English
If there is an equivalence between MonoOver A and MonoOver B, then Subobject A is equivalent to Subobject B.
Русский
Если существует эквивалентность между MonoOver(A) и MonoOver(B), то подобъект A эквивалентен подобъекту B.
LaTeX
$$$\mathrm{Subobject}(A) \simeq \mathrm{Subobject}(B)$$$
Lean4
/-- An equivalence between `MonoOver A` and `MonoOver B` gives an equivalence
between `Subobject A` and `Subobject B`. -/
@[simps]
def lowerEquivalence {A : C} {B : D} (e : MonoOver A ≌ MonoOver B) : Subobject A ≌ Subobject B
where
functor := lower e.functor
inverse := lower e.inverse
unitIso := by
apply eqToIso
convert ThinSkeleton.map_iso_eq e.unitIso
· exact ThinSkeleton.map_id_eq.symm
· exact (ThinSkeleton.map_comp_eq _ _).symm
counitIso := by
apply eqToIso
convert ThinSkeleton.map_iso_eq e.counitIso
· exact (ThinSkeleton.map_comp_eq _ _).symm
· exact ThinSkeleton.map_id_eq.symm
