Yoneda embedding of Grp_ C

We show that group objects are exactly those whose yoneda presheaf is a presheaf of groups, by constructing the yoneda embedding Grp_ C ⥤ Cᵒᵖ ⥤ Grp.{v} and showing that it is fully faithful and its (essential) image is the representable functors.

def Grp_.homMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} [Grp_Class G] [Grp_Class H] (f : G ⟶ H) [IsMon_Hom f] : { X := G, grp := inst✝ } ⟶ { X := H, grp := inst✝¹ }

Construct a morphism G ⟶ H of Grp_ C C from a map f : G ⟶ H and a IsMon_Hom f instance.

@[simp]

theorem Grp_.homMk_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} [Grp_Class G] [Grp_Class H] (f : G ⟶ H) [IsMon_Hom f] : (homMk f).hom = f

def Grp_Class.ofRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ Grp) (α : (F.comp (CategoryTheory.forget Grp)).RepresentableBy X) : Grp_Class X

If X represents a presheaf of monoids, then X is a monoid object.

@[reducible, inline]

abbrev Hom.group {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [Grp_Class G] : Group (X ⟶ G)

If G is a group object, then Hom(X, G) has a group structure.

theorem Hom.inv_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [Grp_Class G] (f : X ⟶ G) : f⁻¹ = CategoryTheory.CategoryStruct.comp f Grp_Class.inv

def yonedaGrpObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [Grp_Class G] : CategoryTheory.Functor Cᵒᵖ Grp

If G is a group object, then Hom(-, G) is a presheaf of groups.

@[simp]

theorem yonedaGrpObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [Grp_Class G] {X✝ Y✝ : Cᵒᵖ} (φ : X✝ ⟶ Y✝) : (yonedaGrpObj G).map φ = Grp.ofHom (MonCat.Hom.hom ((yonedaMonObj G).map φ))

@[simp]

theorem yonedaGrpObj_obj_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [Grp_Class G] (X : Cᵒᵖ) : ↑((yonedaGrpObj G).obj X) = (Opposite.unop X ⟶ G)

def yonedaGrpObjRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [Grp_Class G] : ((yonedaGrpObj G).comp (CategoryTheory.forget Grp)).RepresentableBy G

If G is a monoid object, then Hom(-, G) as a presheaf of monoids is represented by G.

theorem Grp_Class.ofRepresentableBy_yonedaGrpObjRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [Grp_Class G] : ofRepresentableBy G (yonedaGrpObj G) (yonedaGrpObjRepresentableBy G) = inst✝

def yonedaGrpObjIsoOfRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ Grp) (α : (F.comp (CategoryTheory.forget Grp)).RepresentableBy X) : yonedaGrpObj X ≅ F

If X represents a presheaf of groups F, then Hom(-, X) is isomorphic to F as a presheaf of groups.

@[simp]

theorem yonedaGrpObjIsoOfRepresentableBy_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ Grp) (α : (F.comp (CategoryTheory.forget Grp)).RepresentableBy X) : (yonedaGrpObjIsoOfRepresentableBy X F α).hom = { app := fun (X_1 : Cᵒᵖ) => Grp.ofHom ↑{ toEquiv := α.homEquiv, map_mul' := ⋯ }, naturality := ⋯ }

@[simp]

theorem yonedaGrpObjIsoOfRepresentableBy_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ Grp) (α : (F.comp (CategoryTheory.forget Grp)).RepresentableBy X) : (yonedaGrpObjIsoOfRepresentableBy X F α).inv = { app := fun (X_1 : Cᵒᵖ) => Grp.ofHom ↑{ toEquiv := α.homEquiv.symm, map_mul' := ⋯ }, naturality := ⋯ }

def yonedaGrp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.Functor (Grp_ C) (CategoryTheory.Functor Cᵒᵖ Grp)

The yoneda embedding of Grp_C into presheaves of groups.

@[simp]

theorem yonedaGrp_map_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : Grp_ C} (ψ : G ⟶ H) (Y : Cᵒᵖ) : (yonedaGrp.map ψ).app Y = Grp.ofHom (MonCat.Hom.hom ((yonedaMon.map ψ).app Y))

@[simp]

theorem yonedaGrp_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : Grp_ C) : yonedaGrp.obj G = yonedaGrpObj G.X

theorem yonedaGrp_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X Y : C} [Grp_Class G] [Grp_Class H] (α : yonedaGrpObj G ⟶ yonedaGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G) : (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g)

theorem yonedaGrp_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X Y : C} [Grp_Class G] [Grp_Class H] (α : yonedaGrpObj G ⟶ yonedaGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : H ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g) h)

def yonedaGrpFullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] : yonedaGrp.FullyFaithful

The yoneda embedding for Grp_C is fully faithful.

instance instFullGrp_FunctorOppositeGrpYonedaGrp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] : yonedaGrp.Full

instance instFaithfulGrp_FunctorOppositeGrpYonedaGrp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] : yonedaGrp.Faithful

theorem essImage_yonedaGrp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] : yonedaGrp.essImage = (fun (x : CategoryTheory.Functor Cᵒᵖ Grp) => x.comp (CategoryTheory.forget Grp)) ⁻¹' setOf CategoryTheory.Functor.IsRepresentable

theorem Grp_Class.inv_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [Grp_Class G] [Grp_Class H] (f : X ⟶ G) (g : G ⟶ H) [IsMon_Hom g] : CategoryTheory.CategoryStruct.comp f⁻¹ g = (CategoryTheory.CategoryStruct.comp f g)⁻¹

theorem Grp_Class.inv_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [Grp_Class G] [Grp_Class H] (f : X ⟶ G) (g : G ⟶ H) [IsMon_Hom g] {Z : C} (h : H ⟶ Z) : CategoryTheory.CategoryStruct.comp f⁻¹ (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g)⁻¹ h

theorem Grp_Class.div_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [Grp_Class G] [Grp_Class H] (f g : X ⟶ G) (h : G ⟶ H) [IsMon_Hom h] : CategoryTheory.CategoryStruct.comp (f / g) h = CategoryTheory.CategoryStruct.comp f h / CategoryTheory.CategoryStruct.comp g h

theorem Grp_Class.div_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [Grp_Class G] [Grp_Class H] (f g : X ⟶ G) (h : G ⟶ H) [IsMon_Hom h] {Z : C} (h✝ : H ⟶ Z) : CategoryTheory.CategoryStruct.comp (f / g) (CategoryTheory.CategoryStruct.comp h h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h / CategoryTheory.CategoryStruct.comp g h) h✝

theorem Grp_Class.zpow_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [Grp_Class G] [Grp_Class H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H) [IsMon_Hom g] : CategoryTheory.CategoryStruct.comp (f ^ n) g = CategoryTheory.CategoryStruct.comp f g ^ n

theorem Grp_Class.zpow_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [Grp_Class G] [Grp_Class H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H) [IsMon_Hom g] {Z : C} (h : H ⟶ Z) : CategoryTheory.CategoryStruct.comp (f ^ n) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g ^ n) h

theorem Grp_Class.comp_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X Y : C} [Grp_Class G] (f : X ⟶ Y) (g : Y ⟶ G) : CategoryTheory.CategoryStruct.comp f g⁻¹ = (CategoryTheory.CategoryStruct.comp f g)⁻¹

theorem Grp_Class.comp_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X Y : C} [Grp_Class G] (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g⁻¹ h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g)⁻¹ h

theorem Grp_Class.comp_div {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X Y : C} [Grp_Class G] (f : X ⟶ Y) (g h : Y ⟶ G) : CategoryTheory.CategoryStruct.comp f (g / h) = CategoryTheory.CategoryStruct.comp f g / CategoryTheory.CategoryStruct.comp f h

theorem Grp_Class.comp_div_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X Y : C} [Grp_Class G] (f : X ⟶ Y) (g h : Y ⟶ G) {Z : C} (h✝ : G ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g / h) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g / CategoryTheory.CategoryStruct.comp f h) h✝

theorem Grp_Class.comp_zpow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X Y : C} [Grp_Class G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) : CategoryTheory.CategoryStruct.comp f (g ^ n) = CategoryTheory.CategoryStruct.comp f g ^ n

theorem Grp_Class.comp_zpow_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X Y : C} [Grp_Class G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g ^ n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g ^ n) h

theorem Grp_Class.inv_eq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [Grp_Class G] : inv = (CategoryTheory.CategoryStruct.id G)⁻¹

instance instIsMon_HomInvOfIsCommMon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [Grp_Class G] [CategoryTheory.BraidedCategory C] [IsCommMon G] : IsMon_Hom Grp_Class.inv

instance instIsMon_HomInvHomOfIsCommMon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M G : C} [Mon_Class M] [Grp_Class G] [CategoryTheory.BraidedCategory C] [IsCommMon G] {f : M ⟶ G} [IsMon_Hom f] : IsMon_Hom f⁻¹

@[reducible, inline]

abbrev Hom.commGroup {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [Grp_Class G] [CategoryTheory.BraidedCategory C] [IsCommMon G] : CommGroup (X ⟶ G)

If G is a commutative group object, then Hom(X, G) has a commutative group structure.