Mon_ (Type u) ≌ Mon.{u}
#
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
.
Equations
- Mon_Type_equivalence_Mon.Mon_monoid A = {mul := λ (x y : A.X), A.mul (x, y), mul_assoc := _, one := A.one punit.star, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul A.X), npow_zero' := _, npow_succ' := _}
Converting a monoid object in Type
to a bundled monoid.
Equations
- Mon_Type_equivalence_Mon.functor = {obj := λ (A : Mon_ (Type u)), {α := A.X, str := Mon_Type_equivalence_Mon.Mon_monoid A}, 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_3, map_comp' := Mon_Type_equivalence_Mon.functor._proof_4}
Converting a 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)), category_theory.iso.refl ((Mon_Type_equivalence_Mon.functor ⋙ category_theory.forget Mon).obj A)) Mon_Type_equivalence_Mon_forget._proof_1
Equations
Equations
- CommMon_Type_equivalence_CommMon.CommMon_comm_monoid A = {mul := monoid.mul (Mon_Type_equivalence_Mon.Mon_monoid A.to_Mon_), mul_assoc := _, one := monoid.one (Mon_Type_equivalence_Mon.Mon_monoid A.to_Mon_), one_mul := _, mul_one := _, npow := monoid.npow (Mon_Type_equivalence_Mon.Mon_monoid A.to_Mon_), npow_zero' := _, npow_succ' := _, mul_comm := _}
Converting a commutative monoid object in Type
to a bundled commutative monoid.
Equations
- CommMon_Type_equivalence_CommMon.functor = {obj := λ (A : CommMon_ (Type u)), {α := A.to_Mon_.X, str := CommMon_Type_equivalence_CommMon.CommMon_comm_monoid A}, map := λ (A B : CommMon_ (Type u)) (f : A ⟶ B), Mon_Type_equivalence_Mon.functor.map f, map_id' := CommMon_Type_equivalence_CommMon.functor._proof_1, map_comp' := CommMon_Type_equivalence_CommMon.functor._proof_2}
Converting a bundled commutative monoid to a commutative monoid object in Type
.
Equations
- CommMon_Type_equivalence_CommMon.inverse = {obj := λ (A : CommMon), {to_Mon_ := {X := (Mon_Type_equivalence_Mon.inverse.obj ((category_theory.forget₂ CommMon Mon).obj A)).X, one := (Mon_Type_equivalence_Mon.inverse.obj ((category_theory.forget₂ CommMon Mon).obj A)).one, mul := (Mon_Type_equivalence_Mon.inverse.obj ((category_theory.forget₂ CommMon Mon).obj A)).mul, one_mul' := _, mul_one' := _, mul_assoc' := _}, mul_comm' := _}, map := λ (A B : CommMon) (f : A ⟶ B), Mon_Type_equivalence_Mon.inverse.map f, map_id' := CommMon_Type_equivalence_CommMon.inverse._proof_5, map_comp' := CommMon_Type_equivalence_CommMon.inverse._proof_6}
The category of internal commutative monoid objects in Type
is equivalent to the category of "native" bundled commutative monoids.
Equations
- CommMon_Type_equivalence_CommMon = {functor := CommMon_Type_equivalence_CommMon.functor, inverse := CommMon_Type_equivalence_CommMon.inverse, unit_iso := category_theory.nat_iso.of_components (λ (A : CommMon_ (Type u)), {hom := {hom := 𝟙 ((𝟭 (CommMon_ (Type u))).obj A).to_Mon_.X, one_hom' := _, mul_hom' := _}, inv := {hom := 𝟙 ((CommMon_Type_equivalence_CommMon.functor ⋙ CommMon_Type_equivalence_CommMon.inverse).obj A).to_Mon_.X, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) CommMon_Type_equivalence_CommMon._proof_7, counit_iso := category_theory.nat_iso.of_components (λ (A : CommMon), {hom := {to_fun := id ↥((CommMon_Type_equivalence_CommMon.inverse ⋙ CommMon_Type_equivalence_CommMon.functor).obj A), map_one' := _, map_mul' := _}, inv := {to_fun := id ↥((𝟭 CommMon).obj A), map_one' := _, map_mul' := _}, hom_inv_id' := _, inv_hom_id' := _}) CommMon_Type_equivalence_CommMon._proof_14, functor_unit_iso_comp' := CommMon_Type_equivalence_CommMon._proof_15}
The equivalences Mon_ (Type u) ≌ Mon.{u}
and CommMon_ (Type u) ≌ CommMon.{u}
are naturally compatible with the forgetful functors to Mon
and Mon_ (Type u)
.
Equations
- CommMon_Type_equivalence_CommMon_forget = category_theory.nat_iso.of_components (λ (A : CommMon_ (Type u)), category_theory.iso.refl ((CommMon_Type_equivalence_CommMon.functor ⋙ category_theory.forget₂ CommMon Mon).obj A)) CommMon_Type_equivalence_CommMon_forget._proof_1