Structures · Category theory
CategoryTheory.GrpObj
A group object internal to a cartesian monoidal category. Also see the bundled Grp.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Grp
- Shape
- One type argument · adds inv, left_inv, right_inv
Extends1
Extended by1
Forgetful instances
Every CategoryTheory.GrpObj is also a
Concrete types that are instances3
- CategoryTheory.Over
- CategoryTheory.Grp
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by115
- CategoryTheory.GrpObj.inv
- CategoryTheory.Hom.group
- CategoryTheory.GrpObj.comp_inv
- CategoryTheory.yonedaGrpObj
- CategoryTheory.GrpObj.commutator
- CategoryTheory.GrpObj.conj
- CategoryTheory.GrpObj.left_inv
- CategoryTheory.GrpObj.lift_comp_inv_right
- CategoryTheory.GrpObj.lift_comp_inv_left
- CategoryTheory.Functor.grpObjObj
- CategoryTheory.GrpObj.right_inv
- CategoryTheory.Functor.FullyFaithful.grpObj
- CategoryTheory.GrpObj.ofIso
- CategoryTheory.Over.grpObjMkPullbackSnd
- CategoryTheory.GrpObj.mulRight
- CategoryTheory.GrpObj.lift_left_mul_ext
- CategoryTheory.GrpObj.eq_lift_inv_right
- CategoryTheory.CommGrp.mkIso'
- CategoryTheory.GrpObj.lift_conj_eq_mul_mul_inv
- CategoryTheory.GrpObj.eq_lift_inv_left
- CategoryTheory.GrpObj.η_whiskerRight_commutator
- CategoryTheory.GrpObj.mul_inv
- CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η
- CategoryTheory.GrpObj.inv_comp
- CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv
- CategoryTheory.GrpObj.lift_inv_comp_left
- CategoryTheory.GrpObj.inv_hom
- CategoryTheory.GrpObj.whiskerLeft_η_commutator
- CategoryTheory.Hom.commGroup
- CategoryTheory.Grp.mkIso'
- CategoryTheory.GrpObj.inv_comp_inv
- CategoryTheory.GrpObj.lift_inv_comp_right
- CategoryTheory.GrpObj.tensorHom_inv_inv_mul
- CategoryTheory.GrpObj.comp_div
- CategoryTheory.GrpObj.one_inv
- CategoryTheory.GrpObj.mul_inv_rev
- CategoryTheory.Grp.ofHom
- CategoryTheory.GrpObj.lift_inv_left_eq
- CategoryTheory.GrpObj.div_comp
- CategoryTheory.Functor.map_inv'
- AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed
- CategoryTheory.yonedaGrpObjRepresentableBy
- CategoryTheory.IsMonHom.isNormalHom_iff
- CategoryTheory.yonedaGrp_naturality
- CategoryTheory.GrpObj.isPullback
- CategoryTheory.GrpObj.mulRight_hom
- CategoryTheory.Functor.obj.ι_def
- CategoryTheory.GrpObj.comp_zpow
- CategoryTheory.GrpObj.zpow_comp
- CategoryTheory.GrpObj.inv_eq_inv
Ancestors38
- CancelMonoid
- CategoryTheory.MonObj
- Div
- DivInvMonoid
- DivInvOneMonoid
- DivisionMonoid
- Dvd
- Group
- HDiv
- HMul
- HSMul
- Inv
- InvOneClass
- InvolutiveInv
- IsLeftCancelMul
- IsRightCancelMul
- LeftCancelMonoid
- LeftCancelSemigroup
- Monoid
- Mul
- MulAction
- MulOne
- MulOneClass
- NPow
- NSMul
- Nonempty
- OfNat
- One
- RightCancelMonoid
- RightCancelSemigroup
- SDiv
- SMul
- Semigroup
- SemigroupAction
- Torsor
- ZPow
- ZSMul
- Zero