subobjectModule — Mathlib

English

The categorical subobjects of M are in bijection with Submodules of M.

Русский

Категориальные подобъекты M и подмодули M устанавливают биекцию.

LaTeX

$$$\mathrm{Subobject}(M) \cong_{\mathrm{ord}} \mathrm{Submodule}_R(M)$$$

Lean4

/-- The categorical subobjects of a module `M` are in one-to-one correspondence with its
submodules. -/
noncomputable def subobjectModule : Subobject M ≃o Submodule R M :=
  OrderIso.symm
    { invFun := fun S => LinearMap.range S.arrow.hom
      toFun := fun N => Subobject.mk (ofHom N.subtype)
      right_inv := fun S =>
        Eq.symm
          (by
            fapply eq_mk_of_comm
            · apply LinearEquiv.toModuleIso
              apply LinearEquiv.ofBijective (LinearMap.codRestrict (LinearMap.range S.arrow.hom) S.arrow.hom _)
              constructor
              · simp [← LinearMap.ker_eq_bot, ker_eq_bot_of_mono]
              · rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, Submodule.comap_subtype_self]
                exact LinearMap.mem_range_self _
            · ext x
              rfl)
      left_inv := fun N =>
        by
        convert congr_arg LinearMap.range (ModuleCat.hom_ext_iff.mp (underlyingIso_arrow (ofHom N.subtype))) using 1
        · have :
            (underlyingIso (ofHom N.subtype)).inv =
              ofHom (underlyingIso (ofHom N.subtype)).symm.toLinearEquiv.toLinearMap :=
            by
            ext x
            rfl
          rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]
        · exact (Submodule.range_subtype _).symm
      map_rel_iff' := fun {S T} =>
        by
        refine ⟨fun h => ?_, fun h => mk_le_mk_of_comm (↟(Submodule.inclusion h)) rfl⟩
        convert LinearMap.range_comp_le_range (ofMkLEMk _ _ h).hom (ofHom T.subtype).hom
        · rw [← hom_comp, ofMkLEMk_comp]
          exact (Submodule.range_subtype _).symm
        · exact (Submodule.range_subtype _).symm }

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