subobjectOrderIso — Mathlib

English

The subobject lattice of a subobject Y is order-isomorphic to the interval Set.Iic Y.

Русский

Ладша подпредметов подпредмета Y изоморфна по порядку интервалу Set.Iic Y.

LaTeX

$$def subobjectOrderIso {X : C} (Y : Subobject X) : Subobject (Y : C) ≃o Set.Iic Y$$

Lean4

/-- The subobject lattice of a subobject `Y` is order isomorphic to the interval `Set.Iic Y`. -/
def subobjectOrderIso {X : C} (Y : Subobject X) : Subobject (Y : C) ≃o Set.Iic Y
    where
  toFun
    Z := ⟨Subobject.mk (Z.arrow ≫ Y.arrow), Set.mem_Iic.mpr (le_of_comm ((underlyingIso _).hom ≫ Z.arrow) (by simp))⟩
  invFun Z := Subobject.mk (ofLE _ _ Z.2)
  left_inv Z := mk_eq_of_comm _ (underlyingIso _) (by cat_disch)
  right_inv Z := Subtype.ext (mk_eq_of_comm _ (underlyingIso _) (by simp [← Iso.eq_inv_comp]))
  map_rel_iff'
    {W Z} := by
    dsimp
    constructor
    · intro h
      exact
        le_of_comm (((underlyingIso _).inv ≫ ofLE _ _ (Subtype.mk_le_mk.mp h) ≫ (underlyingIso _).hom)) (by cat_disch)
    · intro h
      exact Subtype.mk_le_mk.mpr (le_of_comm ((underlyingIso _).hom ≫ ofLE _ _ h ≫ (underlyingIso _).inv) (by simp))

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