The category of commutative groups in a cartesian monoidal category #
A commutative group object internal to a cartesian monoidal category.
- X : C
- mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.mul self.X) self.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator self.X self.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X self.mul) self.mul)
Instances For
The trivial commutative group object.
Equations
- CommGrp_.trivial C = { toGrp_ := Grp_.trivial C, mul_comm := ⋯ }
Instances For
Equations
- CommGrp_.instInhabited C = { default := CommGrp_.trivial C }
The forgetful functor from commutative group objects to group objects.
Instances For
The forgetful functor from commutative group objects to group objects is fully faithful.
Equations
Instances For
The forgetful functor from commutative group objects to commutative monoid objects.
Instances For
The forgetful functor from commutative group objects to commutative monoid objects is fully faithful.
Equations
Instances For
The forgetful functor from commutative group objects to the ambient category.
Equations
- CommGrp_.forget C = (CommGrp_.forget₂Grp_ C).comp (Grp_.forget C)
Instances For
Constructor for isomorphisms in the category Grp_ C
.
Equations
- CommGrp_.mkIso f one_f mul_f = (CommGrp_.fullyFaithfulForget₂Grp_ C).preimageIso (Grp_.mkIso f one_f mul_f)
Instances For
Equations
A finite-product-preserving functor takes commutative group objects to commutative group objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identity functor is also the identity on commutative group objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The composition functor is also the composition on commutative group objects.
Equations
- CategoryTheory.Functor.mapCommGrpCompIso = CategoryTheory.NatIso.ofComponents (fun (X : CommGrp_ C) => CommGrp_.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapCommGrp.obj X).X) ⋯ ⋯) ⋯
Instances For
Natural transformations between functors lift to commutative group objects.
Equations
Instances For
Natural isomorphisms between functors lift to commutative group objects.
Equations
- CategoryTheory.Functor.mapCommGrpNatIso e = CategoryTheory.NatIso.ofComponents (fun (X : CommGrp_ C) => CommGrp_.mkIso (e.app X.X) ⋯ ⋯) ⋯
Instances For
mapCommGrp
is functorial in the left-exact functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An adjunction of braided functors lifts to an adjunction of their lifts to commutative group objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An equivalence of categories lifts to an equivalence of their commutative group objects.
Equations
- One or more equations did not get rendered due to their size.