The category of R
-modules has finite biproducts #
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
@[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))
:
(M.binaryProductLimitCone N).isLimit.lift s = LinearMap.prod (s.π.app { as := CategoryTheory.Limits.WalkingPair.left })
(s.π.app { as := CategoryTheory.Limits.WalkingPair.right })
@[simp]
theorem
ModuleCat.binaryProductLimitCone_cone_pt
{R : Type u}
[Ring R]
(M : ModuleCat R)
(N : ModuleCat R)
:
(M.binaryProductLimitCone N).cone.pt = ModuleCat.of R (↑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
@[simp]
theorem
ModuleCat.binaryProductLimitCone_cone_π_app_left
{R : Type u}
[Ring R]
(M : ModuleCat R)
(N : ModuleCat R)
:
(M.binaryProductLimitCone N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = LinearMap.fst R ↑M ↑N
@[simp]
theorem
ModuleCat.binaryProductLimitCone_cone_π_app_right
{R : Type u}
[Ring R]
(M : ModuleCat R)
(N : ModuleCat R)
:
(M.binaryProductLimitCone N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = LinearMap.snd R ↑M ↑N
@[simp]
theorem
ModuleCat.biprodIsoProd_hom_apply
{R : Type u}
[Ring R]
(M : ModuleCat R)
(N : ModuleCat R)
(i : ↑(CategoryTheory.Limits.BinaryBiproduct.bicone M N).toCone.pt)
:
(M.biprodIsoProd N).hom i = (CategoryTheory.Limits.biprod.fst i, CategoryTheory.Limits.biprod.snd i)
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
- M.biprodIsoProd N = (CategoryTheory.Limits.BinaryBiproduct.isLimit M N).conePointUniqueUpToIso (M.binaryProductLimitCone N).isLimit
Instances For
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.of R (↑M × ↑N)))
:
CategoryTheory.Limits.biprod.fst ((M.biprodIsoProd N).inv x) = (LinearMap.fst R ↑M ↑N) x
@[simp]
theorem
ModuleCat.biprodIsoProd_inv_comp_fst
{R : Type u}
[Ring R]
(M : ModuleCat R)
(N : ModuleCat R)
:
CategoryTheory.CategoryStruct.comp (M.biprodIsoProd N).inv CategoryTheory.Limits.biprod.fst = LinearMap.fst R ↑M ↑N
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.of R (↑M × ↑N)))
:
CategoryTheory.Limits.biprod.snd ((M.biprodIsoProd N).inv x) = (LinearMap.snd R ↑M ↑N) x
@[simp]
theorem
ModuleCat.biprodIsoProd_inv_comp_snd
{R : Type u}
[Ring R]
(M : ModuleCat R)
(N : ModuleCat R)
:
CategoryTheory.CategoryStruct.comp (M.biprodIsoProd N).inv CategoryTheory.Limits.biprod.snd = LinearMap.snd R ↑M ↑N
@[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
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 = { toFun := fun (x : ↑s.pt) (j : J) => (s.π.app { as := j }) x, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[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))
@[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
@[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
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
@[simp]
theorem
ModuleCat.biproductIsoPi_hom_apply
{R : Type u}
[Ring R]
{J : Type}
[Finite J]
(f : J → ModuleCat R)
(x : ↑(CategoryTheory.Limits.biproduct.bicone f).toCone.pt)
(j : J)
:
(ModuleCat.biproductIsoPi f).hom x j = (CategoryTheory.Limits.biproduct.π f j) x
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
- ModuleCat.biproductIsoPi f = (CategoryTheory.Limits.biproduct.isLimit f).conePointUniqueUpToIso (ModuleCat.HasLimit.productLimitCone f).isLimit
Instances For
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.of R ((j : J) → ↑(f j))))
:
(CategoryTheory.Limits.biproduct.π f j) ((ModuleCat.biproductIsoPi f).inv x) = (LinearMap.proj j) x
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)
:
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
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)
:
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.