Theorems · Definition · category theory
AddCommGrpCat.biprodIsoProd
(G H : AddCommGrpCat) → G ⊞ H ≅ AddCommGrpCat.of (↑G × ↑H)
We verify that the biproduct in AddCommGrpCat is isomorphic to
the Cartesian product of the underlying types:
- Defined in
- Mathlib.Algebra.Category.Grp.Biproducts
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Isostatement · cited by 3,963
- AddCommGrpCatstatement and proof · cited by 462
- AddCommGrpCat.carrierstatement · cited by 407
- CategoryTheory.Limits.biprodstatement · cited by 312
- AddCommGrpCat.ofstatement · cited by 97
- CategoryTheory.Limits.LimitCone.isLimitproof · cited by 58
- CategoryTheory.Limits.IsLimit.conePointUniqueUpToIsoproof · cited by 57
- CategoryTheory.Limits.BinaryBiproduct.isLimitproof · cited by 14
- AddCommGrpCat.binaryProductLimitConeproof · cited by 6
Cited by11
Results whose statement or proof uses this declaration.
- AddCommGrpCat.biprodIsoProd_inv_comp_descstatement and proof · cited by 2
- AddCommGrpCat.biprodIsoProd_inv_comp_fststatement · cited by 1
- AddCommGrpCat.biprodIsoProd_inv_comp_fst_applystatement and proof · cited by 1
- AddCommGrpCat.biprodIsoProd_inv_comp_sndstatement · cited by 1
- AddCommGrpCat.biprodIsoProd_inv_comp_snd_applystatement and proof · cited by 1
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_applystatement and proof · cited by 1
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_applystatement and proof · cited by 1
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequenceIsoproof · cited by 1
- AddCommGrpCat.biprodIsoProd_inv_comp_desc_applystatement and proof · cited by 0
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_applystatement and proof · cited by 0
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_homstatement and proof · cited by 0