The category of groups in a cartesian monoidal category #
We define group objects in cartesian monoidal categories.
We show that the associativity diagram of a group object is always cartesian and deduce that morphisms of group objects commute with taking inverses.
We show that a finite-product-preserving functor takes group objects to group objects.
class
Grp_Class
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(X : C)
extends Mon_Class X :
Type v₁
A group object internal to a cartesian monoidal category. Also see the bundled Grp_.
- mul_assoc' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul X) mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X mul) mul)
The inverse in a group object
Instances
The inverse in a group object
Equations
- Mon_Class.termι = Lean.ParserDescr.node `Mon_Class.termι 1024 (Lean.ParserDescr.symbol "ι")
Instances For
The inverse in a group object
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Grp_Class.left_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(X : C)
[Grp_Class X]
:
@[simp]
theorem
Grp_Class.left_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(X : C)
[Grp_Class X]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CartesianMonoidalCategory.lift inv (CategoryTheory.CategoryStruct.id X))
(CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X)
(CategoryTheory.CategoryStruct.comp Mon_Class.one h)
@[simp]
theorem
Grp_Class.right_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(X : C)
[Grp_Class X]
:
@[simp]
theorem
Grp_Class.right_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(X : C)
[Grp_Class X]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) inv)
(CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X)
(CategoryTheory.CategoryStruct.comp Mon_Class.one h)
instance
Grp_Class.instTensorUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
Equations
- One or more equations did not get rendered due to their size.
structure
Grp_
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
Type (max u₁ v₁)
A group object in a cartesian monoidal category.
- X : C
The underlying object in the ambient monoidal category
Instances For
def
Grp_.toMon_
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Grp_ C)
:
Mon_ C
A group object is a monoid object.
Instances For
@[simp]
theorem
Grp_.toMon__X
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Grp_ C)
:
def
Grp_.trivial
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
Grp_ C
The trivial group object.
Equations
- Grp_.trivial C = { X := (Mon_.trivial C).X, grp := inferInstanceAs (Grp_Class (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) }
Instances For
@[simp]
theorem
Grp_.trivial_X
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
instance
Grp_.instInhabited
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
Equations
- Grp_.instInhabited = { default := Grp_.trivial C }
def
Grp_.mk'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(X : C)
[Grp_Class X]
:
Grp_ C
Make a group object from Grp_Class.
Equations
- Grp_.mk' X = { X := { X := X, mon := inst✝.toMon_Class }.X, grp := { toMon_Class := inst✝.toMon_Class, inv := Grp_Class.inv, left_inv' := ⋯, right_inv' := ⋯ } }
Instances For
@[simp]
theorem
Grp_.mk'_X
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(X : C)
[Grp_Class X]
:
@[simp]
theorem
Grp_.id_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Grp_ C)
:
@[simp]
theorem
Grp_.comp_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{R S T : Grp_ C}
(f : R ⟶ S)
(g : S ⟶ T)
:
theorem
Grp_.hom_ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : Grp_ C}
(f g : A ⟶ B)
(h : f.hom = g.hom)
:
theorem
Grp_.hom_ext_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : Grp_ C}
{f g : A ⟶ B}
:
@[simp]
theorem
Grp_.id'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Grp_ C)
:
@[simp]
theorem
Grp_.comp'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A₁ A₂ A₃ : Grp_ C}
(f : A₁ ⟶ A₂)
(g : A₂ ⟶ A₃)
:
@[simp]
theorem
Grp_Class.lift_comp_inv_right
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class B]
(f : A ⟶ B)
:
@[simp]
theorem
Grp_Class.lift_comp_inv_right_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class B]
(f : A ⟶ B)
{Z : C}
(h : B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp f inv))
(CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A)
(CategoryTheory.CategoryStruct.comp Mon_Class.one h)
theorem
Grp_Class.lift_inv_comp_right
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class A]
[Grp_Class B]
(f : A ⟶ B)
[IsMon_Hom f]
:
theorem
Grp_Class.lift_inv_comp_right_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class A]
[Grp_Class B]
(f : A ⟶ B)
[IsMon_Hom f]
{Z : C}
(h : B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp inv f))
(CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A)
(CategoryTheory.CategoryStruct.comp Mon_Class.one h)
@[simp]
theorem
Grp_Class.lift_comp_inv_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class B]
(f : A ⟶ B)
:
@[simp]
theorem
Grp_Class.lift_comp_inv_left_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class B]
(f : A ⟶ B)
{Z : C}
(h : B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f inv) f)
(CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A)
(CategoryTheory.CategoryStruct.comp Mon_Class.one h)
theorem
Grp_Class.lift_inv_comp_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class A]
[Grp_Class B]
(f : A ⟶ B)
[IsMon_Hom f]
:
theorem
Grp_Class.lift_inv_comp_left_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class A]
[Grp_Class B]
(f : A ⟶ B)
[IsMon_Hom f]
{Z : C}
(h : B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp inv f) f)
(CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A)
(CategoryTheory.CategoryStruct.comp Mon_Class.one h)
theorem
Grp_Class.eq_lift_inv_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class B]
(f g h : A ⟶ B)
:
theorem
Grp_Class.lift_inv_left_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class B]
(f g h : A ⟶ B)
:
theorem
Grp_Class.eq_lift_inv_right
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class B]
(f g h : A ⟶ B)
:
theorem
Grp_Class.lift_inv_right_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class B]
(f g h : A ⟶ B)
:
theorem
Grp_Class.lift_left_mul_ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class B]
{f g : A ⟶ B}
(i : A ⟶ B)
(h :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f i) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g i) Mon_Class.mul)
:
@[simp]
theorem
Grp_Class.inv_comp_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : C)
[Grp_Class A]
:
@[simp]
theorem
Grp_Class.inv_comp_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : C)
[Grp_Class A]
{Z : C}
(h : A ⟶ Z)
:
instance
Grp_Class.instIsIsoInv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : C)
[Grp_Class A]
:
@[simp]
theorem
Grp_Class.inv_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : C)
[Grp_Class A]
:
For inv ≫ inv = 𝟙 see inv_comp_inv.
theorem
Grp_Class.mul_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(A : C)
[Grp_Class A]
:
theorem
Grp_Class.mul_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(A : C)
[Grp_Class A]
{Z : C}
(h : A ⟶ Z)
:
@[simp]
theorem
Grp_Class.tensorHom_inv_inv_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(A : C)
[Grp_Class A]
:
@[simp]
theorem
Grp_Class.tensorHom_inv_inv_mul_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(A : C)
[Grp_Class A]
{Z : C}
(h : A ⟶ Z)
:
def
Grp_Class.mulRight
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A : C}
[Grp_Class A]
(f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A)
:
The map (· * f).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Grp_Class.mulRight_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A : C}
[Grp_Class A]
(f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A)
:
@[simp]
theorem
Grp_Class.mulRight_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A : C}
[Grp_Class A]
(f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A)
:
@[simp]
theorem
Grp_Class.mulRight_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : C)
[Grp_Class A]
:
theorem
Grp_Class.isPullback
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : C)
[Grp_Class A]
:
The associativity diagram of a group object is cartesian.
In fact, any monoid object whose associativity diagram is cartesian can be made into a group object (we do not prove this in this file), so we should expect that many properties of group objects follow from this result.
@[simp]
theorem
Grp_Class.inv_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class A]
[Grp_Class B]
(f : A ⟶ B)
[IsMon_Hom f]
:
Morphisms of group objects preserve inverses.
@[simp]
theorem
Grp_Class.inv_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : C}
[Grp_Class A]
[Grp_Class B]
(f : A ⟶ B)
[IsMon_Hom f]
{Z : C}
(h : B ⟶ Z)
:
theorem
Grp_Class.toMon_Class_injective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{X : C}
:
Function.Injective (@toMon_Class C inst✝ inst✝¹ X)
theorem
Grp_Class.ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{X : C}
(h₁ h₂ : Grp_Class X)
(H : h₁.toMon_Class = h₂.toMon_Class)
:
theorem
Grp_Class.ext_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{X : C}
{h₁ h₂ : Grp_Class X}
:
def
Grp_.forget₂Mon_
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
CategoryTheory.Functor (Grp_ C) (Mon_ C)
The forgetful functor from group objects to monoid objects.
Instances For
def
Grp_.fullyFaithfulForget₂Mon_
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
The forgetful functor from group objects to monoid objects is fully faithful.
Instances For
instance
Grp_.instFullMon_Forget₂Mon_
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
(forget₂Mon_ C).Full
instance
Grp_.instFaithfulMon_Forget₂Mon_
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
(forget₂Mon_ C).Faithful
@[simp]
theorem
Grp_.forget₂Mon_obj_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Grp_ C)
:
@[simp]
theorem
Grp_.forget₂Mon_obj_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Grp_ C)
:
@[simp]
theorem
Grp_.forget₂Mon_map_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{A B : Grp_ C}
(f : A ⟶ B)
:
def
Grp_.forget
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
CategoryTheory.Functor (Grp_ C) C
The forgetful functor from group objects to the ambient category.
Equations
- Grp_.forget C = (Grp_.forget₂Mon_ C).comp (Mon_.forget C)
Instances For
@[simp]
theorem
Grp_.forget_map
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{X✝ Y✝ : Grp_ C}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
Grp_.forget_obj
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(X : Grp_ C)
:
instance
Grp_.instFaithfulForget
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
@[simp]
theorem
Grp_.forget₂Mon_comp_forget
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
def
Grp_.mkIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{M N : Grp_ C}
(f : M.X ≅ N.X)
(one_f : CategoryTheory.CategoryStruct.comp Mon_Class.one f.hom = Mon_Class.one := by aesop_cat)
(mul_f :
CategoryTheory.CategoryStruct.comp Mon_Class.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) Mon_Class.mul := by
aesop_cat)
:
Constructor for isomorphisms in the category Grp_ C.
Equations
- Grp_.mkIso f one_f mul_f = (Grp_.fullyFaithfulForget₂Mon_ C).preimageIso (Mon_.mkIso f one_f mul_f)
Instances For
@[simp]
theorem
Grp_.mkIso_hom_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{M N : Grp_ C}
(f : M.X ≅ N.X)
(one_f : CategoryTheory.CategoryStruct.comp Mon_Class.one f.hom = Mon_Class.one := by aesop_cat)
(mul_f :
CategoryTheory.CategoryStruct.comp Mon_Class.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) Mon_Class.mul := by
aesop_cat)
:
@[simp]
theorem
Grp_.mkIso_inv_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
{M N : Grp_ C}
(f : M.X ≅ N.X)
(one_f : CategoryTheory.CategoryStruct.comp Mon_Class.one f.hom = Mon_Class.one := by aesop_cat)
(mul_f :
CategoryTheory.CategoryStruct.comp Mon_Class.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) Mon_Class.mul := by
aesop_cat)
:
instance
Grp_.uniqueHomFromTrivial
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Grp_ C)
:
Equations
instance
Grp_.instHasInitial
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
noncomputable def
CategoryTheory.Functor.mapGrp
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
:
A finite-product-preserving functor takes group objects to group objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapGrp_obj_grp_one
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(A : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.mapGrp_obj_X
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(A : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.mapGrp_obj_grp_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(A : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.mapGrp_obj_grp_mul
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(A : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.mapGrp_map_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
{X✝ Y✝ : Grp_ C}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.mapGrp_id_one
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
(A : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.mapGrp_id_mul
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
(A : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.comp_mapGrp_one
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[CartesianMonoidalCategory E]
{F : Functor C D}
[F.Monoidal]
{G : Functor D E}
[G.Monoidal]
(A : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.comp_mapGrp_mul
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[CartesianMonoidalCategory E]
{F : Functor C D}
[F.Monoidal]
{G : Functor D E}
[G.Monoidal]
(A : Grp_ C)
:
Mon_Class.mul = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) A.X A.X) ((F.comp G).map Mon_Class.mul)
noncomputable def
CategoryTheory.Functor.mapGrpIdIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
:
The identity functor is also the identity on group objects.
Equations
- CategoryTheory.Functor.mapGrpIdIso = CategoryTheory.NatIso.ofComponents (fun (X : Grp_ C) => Grp_.mkIso (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).mapGrp.obj X).X) ⋯ ⋯) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapGrpIdIso_inv_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
(X : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.mapGrpIdIso_hom_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
(X : Grp_ C)
:
noncomputable def
CategoryTheory.Functor.mapGrpCompIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[CartesianMonoidalCategory E]
{F : Functor C D}
[F.Monoidal]
{G : Functor D E}
[G.Monoidal]
:
The composition functor is also the composition on group objects.
Equations
- CategoryTheory.Functor.mapGrpCompIso = CategoryTheory.NatIso.ofComponents (fun (X : Grp_ C) => Grp_.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapGrp.obj X).X) ⋯ ⋯) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapGrpCompIso_hom_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[CartesianMonoidalCategory E]
{F : Functor C D}
[F.Monoidal]
{G : Functor D E}
[G.Monoidal]
(X : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.mapGrpCompIso_inv_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[CartesianMonoidalCategory E]
{F : Functor C D}
[F.Monoidal]
{G : Functor D E}
[G.Monoidal]
(X : Grp_ C)
:
noncomputable def
CategoryTheory.Functor.mapGrpNatTrans
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{F F' : Functor C D}
[F.Monoidal]
[F'.Monoidal]
(f : F ⟶ F')
:
Natural transformations between functors lift to group objects.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapGrpNatTrans_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{F F' : Functor C D}
[F.Monoidal]
[F'.Monoidal]
(f : F ⟶ F')
(X : Grp_ C)
:
noncomputable def
CategoryTheory.Functor.mapGrpNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{F F' : Functor C D}
[F.Monoidal]
[F'.Monoidal]
(e : F ≅ F')
:
Natural isomorphisms between functors lift to group objects.
Equations
- CategoryTheory.Functor.mapGrpNatIso e = CategoryTheory.NatIso.ofComponents (fun (X : Grp_ C) => Grp_.mkIso (e.app X.toMon_.X) ⋯ ⋯) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapGrpNatIso_hom_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{F F' : Functor C D}
[F.Monoidal]
[F'.Monoidal]
(e : F ≅ F')
(X : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.mapGrpNatIso_inv_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{F F' : Functor C D}
[F.Monoidal]
[F'.Monoidal]
(e : F ≅ F')
(X : Grp_ C)
:
noncomputable def
CategoryTheory.Functor.mapGrpFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
:
mapGrp is functorial in the left-exact functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapGrpFunctor_map_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{F G : C ⥤ₗ D}
(α : F ⟶ G)
(A : Grp_ C)
:
@[simp]
theorem
CategoryTheory.Functor.mapGrpFunctor_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(F : C ⥤ₗ D)
:
noncomputable def
CategoryTheory.Adjunction.mapGrp
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(a : F ⊣ G)
[F.Monoidal]
[G.Monoidal]
:
An adjunction of monoidal functors lifts to an adjunction of their lifts to group objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Adjunction.mapGrp_unit
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(a : F ⊣ G)
[F.Monoidal]
[G.Monoidal]
:
@[simp]
theorem
CategoryTheory.Adjunction.mapGrp_counit
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(a : F ⊣ G)
[F.Monoidal]
[G.Monoidal]
:
noncomputable def
CategoryTheory.Equivalence.mapGrp
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
:
An equivalence of categories lifts to an equivalence of their group objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Equivalence.mapGrp_unitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
:
@[simp]
theorem
CategoryTheory.Equivalence.mapGrp_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
:
@[simp]
theorem
CategoryTheory.Equivalence.mapGrp_inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
:
@[simp]
theorem
CategoryTheory.Equivalence.mapGrp_counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[CartesianMonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[CartesianMonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
: