English
The flat sections of a functor into MonCat form a submonoid of all sections.
Русский
Плоские секции функторa в MonCat образуют подмоноид всех секций.
LaTeX
$$$\text{sections Submonoid}(F) \subseteq \forall j, F.obj j$ with closed under pointwise multiplication and containing the unit$$
Lean4
/-- The flat sections of a functor into `MonCat` form a submonoid of all sections. -/
@[to_additive /-- The flat sections of a functor into `AddMonCat` form an additive submonoid of all sections. -/
]
def sectionsSubmonoid : Submonoid (∀ j, F.obj j)
where
carrier := (F ⋙ forget MonCat).sections
one_mem' {j} {j'} f := by simp
mul_mem' {a} {b} ah bh {j} {j'}
f := by
simp only [Functor.comp_map, Pi.mul_apply]
dsimp [Functor.sections] at ah bh
rw [← ah f, ← bh f, forget_map, map_mul]
