instSmallUnitsSkeletonModuleCat — Mathlib

English

Given an invertible R-module M with freeness assumptions, define a submodule of A as the image of embAlgebra.

Русский

При наличии обратимого R-модуля M и предположений о свободности задаётся подмодуль A как образ embAlgebra.

LaTeX

$$toSubmodule : Submodule R A$$

Lean4

instance : Small.{u} (Skeleton <| ModuleCat.{u} R)ˣ :=
  let sf := Σ n, Submodule R (Fin n → R)
  have {M N : sf} : M = N → (_ ⧸ M.2) ≃ₗ[R] _ ⧸ N.2 := by rintro rfl; exact .refl ..
  let f (M : (Skeleton <| ModuleCat.{u} R)ˣ) : sf := ⟨_, Finite.kerRepr R M⟩
  small_of_injective (f := f) fun M N eq ↦
    Units.ext <|
      Quotient.out_equiv_out.mp ⟨((Finite.reprEquiv R M).symm ≪≫ₗ this eq ≪≫ₗ Finite.reprEquiv R N).toModuleIso⟩

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