The category of R
-modules has finite biproducts #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
We verify that the biproduct in ModuleCat R
is isomorphic to
the cartesian product of the underlying types:
Equations
Instances For
The map from an arbitrary cone over an indexed family of abelian groups to the cartesian product of those groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
We verify that the biproduct we've just defined is isomorphic to the ModuleCat R
structure
on the dependent function type.
Equations
Instances For
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
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.