Mon_ (Type u) ≌ Mon.{u}
The category of internal monoid objects in Type
is equivalent to the category of "native" bundled monoids.
Moreover, this equivalence is compatible with the forgetful functors to Type.
Converting a monoid object in Type to a bundled monoid.
Equations
- Mon_Type_equivalence_Mon.functor = {obj := λ (A : Mon_ (Type u)), {α := A.X, str := {mul := λ (x y : A.X), A.mul (x, y), mul_assoc := _, one := A.one punit.star, one_mul := _, mul_one := _}}, map := λ (A B : Mon_ (Type u)) (f : A ⟶ B), {to_fun := f.hom, map_one' := _, map_mul' := _}, map_id' := Mon_Type_equivalence_Mon.functor._proof_12, map_comp' := Mon_Type_equivalence_Mon.functor._proof_13}
Converting bundled monoid to a monoid object in Type.
Equations
- Mon_Type_equivalence_Mon.inverse = {obj := λ (A : Mon), {X := ↥A, one := λ (_x : 𝟙_ (Type u)), 1, mul := λ (p : ↥A ⊗ ↥A), p.fst * p.snd, one_mul' := _, mul_one' := _, mul_assoc' := _}, map := λ (A B : Mon) (f : A ⟶ B), {hom := ⇑f, one_hom' := _, mul_hom' := _}, map_id' := Mon_Type_equivalence_Mon.inverse._proof_12, map_comp' := Mon_Type_equivalence_Mon.inverse._proof_13}
The category of internal monoid objects in Type
is equivalent to the category of "native" bundled monoids.
Equations
- Mon_Type_equivalence_Mon = {functor := Mon_Type_equivalence_Mon.functor, inverse := Mon_Type_equivalence_Mon.inverse, unit_iso := category_theory.nat_iso.of_components (λ (A : Mon_ (Type u)), {hom := {hom := 𝟙 ((𝟭 (Mon_ (Type u))).obj A).X, one_hom' := _, mul_hom' := _}, inv := {hom := 𝟙 ((Mon_Type_equivalence_Mon.functor ⋙ Mon_Type_equivalence_Mon.inverse).obj A).X, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) Mon_Type_equivalence_Mon._proof_7, counit_iso := category_theory.nat_iso.of_components (λ (A : Mon), {hom := {to_fun := id ↥((Mon_Type_equivalence_Mon.inverse ⋙ Mon_Type_equivalence_Mon.functor).obj A), map_one' := _, map_mul' := _}, inv := {to_fun := id ↥((𝟭 Mon).obj A), map_one' := _, map_mul' := _}, hom_inv_id' := _, inv_hom_id' := _}) Mon_Type_equivalence_Mon._proof_14, functor_unit_iso_comp' := Mon_Type_equivalence_Mon._proof_15}
The equivalence Mon_ (Type u) ≌ Mon.{u}
is naturally compatible with the forgetful functors to Type u.
Equations
- Mon_Type_equivalence_Mon_forget = category_theory.nat_iso.of_components (λ (A : Mon_ (Type u_1)), category_theory.iso.refl ((Mon_Type_equivalence_Mon.functor ⋙ category_theory.forget Mon).obj A)) Mon_Type_equivalence_Mon_forget._proof_1
@[instance]