English
There is a type-level bijection preserving order between Subobject X and Subobject Y for an isomorphism X ≅ Y.
Русский
Для изоморфизма X ≅ Y существует биекция на уровне типов, сохраняющая порядок между Subobject(X) и Subobject(Y).
LaTeX
$$$\text{mapIsoToOrderIso}(e) : \mathrm{Subobject}(X) \cong_{\mathrm{ord}} \mathrm{Subobject}(Y)$$$
Lean4
/-- In fact, there's a type level bijection between the subobjects of isomorphic objects,
which preserves the order. -/
@[simps]
def mapIsoToOrderIso (e : X ≅ Y) : Subobject X ≃o Subobject Y
where
toFun := (map e.hom).obj
invFun := (map e.inv).obj
left_inv g := by simp_rw [← map_comp, e.hom_inv_id, map_id]
right_inv g := by simp_rw [← map_comp, e.inv_hom_id, map_id]
map_rel_iff'
{A B} := by
dsimp
constructor
· intro h
apply_fun (map e.inv).obj at h
· simpa only [← map_comp, e.hom_inv_id, map_id] using h
· apply Functor.monotone
· intro h
apply_fun (map e.hom).obj at h
· exact h
· apply Functor.monotone
