ofRepresentableBy — Mathlib

English

If X represents a presheaf of monoids F on C, then X carries a canonical monoid object structure in C.

Русский

Если X представляет предобразную систему моноидов F на C, то X обладает канонической структурой моноида в C.

LaTeX

$$$\text{GrpObj.ofRepresentableBy}(X,F,\alpha) \text{ is a monoid object on } X$$$

Lean4

/-- If `X` represents a presheaf of monoids, then `X` is a monoid object. -/
def ofRepresentableBy (F : Cᵒᵖ ⥤ GrpCat.{w}) (α : (F ⋙ forget _).RepresentableBy X) : GrpObj X
    where
  __ := MonObj.ofRepresentableBy X (F ⋙ forget₂ GrpCat MonCat) α
  inv := α.homEquiv.symm (α.homEquiv (𝟙 _))⁻¹
  left_inv :=
    by
    change
      lift (α.homEquiv.symm (α.homEquiv (𝟙 X))⁻¹) (𝟙 X) ≫
          α.homEquiv.symm (α.homEquiv (fst X X) * α.homEquiv (snd X X)) =
        toUnit X ≫ α.homEquiv.symm 1
    apply α.homEquiv.injective
    simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
    simp only [Functor.comp_map, ConcreteCategory.forget_map_eq_coe, map_one, map_mul]
    simp only [← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map, ← α.homEquiv_comp]
    simp [-Functor.comp_obj]
  right_inv :=
    by
    change
      lift (𝟙 X) (α.homEquiv.symm (α.homEquiv (𝟙 X))⁻¹) ≫
          α.homEquiv.symm (α.homEquiv (fst X X) * α.homEquiv (snd X X)) =
        toUnit X ≫ α.homEquiv.symm 1
    apply α.homEquiv.injective
    simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
    simp only [Functor.comp_map, ConcreteCategory.forget_map_eq_coe, map_one, map_mul]
    simp only [← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map, ← α.homEquiv_comp]
    simp [-Functor.comp_obj]

Похожие утверждения