Documentation

Mathlib.Algebra.Category.ModuleCat.Biproducts

The category of R-modules has finite biproducts #

source
instance ModuleCat.instHasBinaryBiproductsModuleCatModuleCategoryPreadditiveHasZeroMorphismsInstPreadditiveModuleCatModuleCategory {R : Type u} [Ring R] :
CategoryTheory.Limits.HasBinaryBiproducts (ModuleCat R)
Equations
  • ⋯ = ⋯
source
instance ModuleCat.instHasFiniteBiproductsModuleCatModuleCategoryPreadditiveHasZeroMorphismsInstPreadditiveModuleCatModuleCategory {R : Type u} [Ring R] :
CategoryTheory.Limits.HasFiniteBiproducts (ModuleCat R)
Equations
  • ⋯ = ⋯
source
@[simp]
theorem ModuleCat.binaryProductLimitCone_isLimit_lift {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) (s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair M N)) :
(ModuleCat.binaryProductLimitCone M N).isLimit.lift s = LinearMap.prod (s.π.app { as := CategoryTheory.Limits.WalkingPair.left }) (s.π.app { as := CategoryTheory.Limits.WalkingPair.right })
source
@[simp]
theorem ModuleCat.binaryProductLimitCone_cone_pt {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) :
(ModuleCat.binaryProductLimitCone M N).cone.pt = ModuleCat.of R (↑M × ↑N)
source
def ModuleCat.binaryProductLimitCone {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) :
CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair M N)

Construct limit data for a binary product in ModuleCat R, using ModuleCat.of R (M × N).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem ModuleCat.binaryProductLimitCone_cone_π_app_left {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) :
    (ModuleCat.binaryProductLimitCone M N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = LinearMap.fst R ↑M ↑N
    source
    @[simp]
    theorem ModuleCat.binaryProductLimitCone_cone_π_app_right {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) :
    (ModuleCat.binaryProductLimitCone M N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = LinearMap.snd R ↑M ↑N
    source
    @[simp]
    theorem ModuleCat.biprodIsoProd_hom_apply {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) (i : ↑(CategoryTheory.Limits.BinaryBicone.toCone (CategoryTheory.Limits.BinaryBiproduct.bicone M N)).pt) :
    (ModuleCat.biprodIsoProd M N).hom i = (CategoryTheory.Limits.biprod.fst i, CategoryTheory.Limits.biprod.snd i)
    source
    noncomputable def ModuleCat.biprodIsoProd {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) :
    M ⊞ N ≅ ModuleCat.of R (↑M × ↑N)

    We verify that the biproduct in ModuleCat R is isomorphic to the cartesian product of the underlying types:

    Equations
    Instances For
      source
      theorem ModuleCat.biprodIsoProd_inv_comp_fst_apply {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.binaryProductLimitCone M N).cone.pt) :
      CategoryTheory.Limits.biprod.fst ((CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit M N) (ModuleCat.binaryProductLimitCone M N).isLimit).inv x) = (LinearMap.fst R ↑M ↑N) x
      source
      @[simp]
      theorem ModuleCat.biprodIsoProd_inv_comp_fst {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) :
      CategoryTheory.CategoryStruct.comp (ModuleCat.biprodIsoProd M N).inv CategoryTheory.Limits.biprod.fst = LinearMap.fst R ↑M ↑N
      source
      theorem ModuleCat.biprodIsoProd_inv_comp_snd_apply {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.binaryProductLimitCone M N).cone.pt) :
      CategoryTheory.Limits.biprod.snd ((CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit M N) (ModuleCat.binaryProductLimitCone M N).isLimit).inv x) = (LinearMap.snd R ↑M ↑N) x
      source
      @[simp]
      theorem ModuleCat.biprodIsoProd_inv_comp_snd {R : Type u} [Ring R] (M : ModuleCat R) (N : ModuleCat R) :
      CategoryTheory.CategoryStruct.comp (ModuleCat.biprodIsoProd M N).inv CategoryTheory.Limits.biprod.snd = LinearMap.snd R ↑M ↑N
      source
      @[simp]
      theorem ModuleCat.HasLimit.lift_apply {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) (x : ↑s.pt) (j : J) :
      (ModuleCat.HasLimit.lift f s) x j = (s.π.app { as := j }) x
      source
      def ModuleCat.HasLimit.lift {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) :
      s.pt ⟶ ModuleCat.of R ((j : J) → ↑(f j))

      The map from an arbitrary cone over an indexed family of abelian groups to the cartesian product of those groups.

      Equations
      • ModuleCat.HasLimit.lift f s = { toAddHom := { toFun := fun (x : ↑s.pt) (j : J) => (s.π.app { as := j }) x, map_add' := ⋯ }, map_smul' := ⋯ }
      Instances For
        source
        @[simp]
        theorem ModuleCat.HasLimit.productLimitCone_isLimit_lift {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) :
        (ModuleCat.HasLimit.productLimitCone f).isLimit.lift s = ModuleCat.HasLimit.lift f s
        source
        @[simp]
        theorem ModuleCat.HasLimit.productLimitCone_cone_pt {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) :
        (ModuleCat.HasLimit.productLimitCone f).cone.pt = ModuleCat.of R ((j : J) → ↑(f j))
        source
        @[simp]
        theorem ModuleCat.HasLimit.productLimitCone_cone_π {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) :
        (ModuleCat.HasLimit.productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun (j : CategoryTheory.Discrete J) => LinearMap.proj j.as
        source
        def ModuleCat.HasLimit.productLimitCone {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) :
        CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)

        Construct limit data for a product in ModuleCat R, using ModuleCat.of R (∀ j, F.obj j).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem ModuleCat.biproductIsoPi_hom_apply {R : Type u} [Ring R] {J : Type} [Finite J] (f : J → ModuleCat R) (x : ↑(CategoryTheory.Limits.Bicone.toCone (CategoryTheory.Limits.biproduct.bicone f)).pt) (j : J) :
          (ModuleCat.biproductIsoPi f).hom x j = (CategoryTheory.Limits.biproduct.π f j) x
          source
          noncomputable def ModuleCat.biproductIsoPi {R : Type u} [Ring R] {J : Type} [Finite J] (f : J → ModuleCat R) :
          ⨁ f ≅ ModuleCat.of R ((j : J) → ↑(f j))

          We verify that the biproduct we've just defined is isomorphic to the ModuleCat R structure on the dependent function type.

          Equations
          Instances For
            source
            theorem ModuleCat.biproductIsoPi_inv_comp_π_apply {R : Type u} [Ring R] {J : Type} [Finite J] (f : J → ModuleCat R) (j : J) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.HasLimit.productLimitCone f).cone.pt) :
            (CategoryTheory.Limits.biproduct.π f j) ((CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f) (ModuleCat.HasLimit.productLimitCone f).isLimit).inv x) = (LinearMap.proj j) x
            source
            @[simp]
            theorem ModuleCat.biproductIsoPi_inv_comp_π {R : Type u} [Ring R] {J : Type} [Finite J] (f : J → ModuleCat R) (j : J) :
            CategoryTheory.CategoryStruct.comp (ModuleCat.biproductIsoPi f).inv (CategoryTheory.Limits.biproduct.π f j) = LinearMap.proj j
            source
            noncomputable def lequivProdOfRightSplitExact {R : Type u} {A : Type v} {M : Type v} {B : Type v} [Ring R] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup M] [Module R M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : B →ₗ[R] M} (hj : Function.Injective ⇑j) (exac : LinearMap.range j = LinearMap.ker g) (h : g ∘ₗ f = LinearMap.id) :
            (A × B) ≃ₗ[R] M

            The isomorphism A × B ≃ₗ[R] M coming from a right split exact sequence 0 ⟶ A ⟶ M ⟶ B ⟶ 0 of modules.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def lequivProdOfLeftSplitExact {R : Type u} {A : Type v} {M : Type v} {B : Type v} [Ring R] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup M] [Module R M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : M →ₗ[R] A} (hg : Function.Surjective ⇑g) (exac : LinearMap.range j = LinearMap.ker g) (h : f ∘ₗ j = LinearMap.id) :
              (A × B) ≃ₗ[R] M

              The isomorphism A × B ≃ₗ[R] M coming from a left split exact sequence 0 ⟶ A ⟶ M ⟶ B ⟶ 0 of modules.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For