iso — Mathlib

English

The second verification of the iso between a mono over m and the pullback representation is established.

Русский

Доказано второе свойство изоморфизма между MonoOver и представителем подмножества.

LaTeX

$$Eq (Subobject.mk m) ((Subobject.pullback (EquivLike.toFunLike.coe h.homEquiv.symm (Subobject.mk m))).obj h.Ω₀)$$

Lean4

/-- `h.iso m` is the isomorphism between `m` and the pullback of `Ω₀`
along the characteristic map of `m`. -/
noncomputable def iso : MonoOver.mk' m ≅ Subobject.representative.obj ((Subobject.pullback (h.χ m)).obj h.Ω₀) :=
  (Subobject.representativeIso (.mk' m)).symm ≪≫
    Subobject.representative.mapIso (eqToIso (h.pullback_homEquiv_symm_obj_Ω₀ (.mk m)).symm)

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