sectionsSubmodule — Mathlib

English

The flat sections of a functor into ModuleCat R form a submodule of all sections.

Русский

Плоские секции непрерывной функции в ModuleCat R образуют подмодуль всех секций.

LaTeX

$$$$ \\text{sectionsSubmodule}(F) \\subseteq (\\text{sections}) $$$$

Lean4

/-- The flat sections of a functor into `ModuleCat R` form a submodule of all sections.
-/
def sectionsSubmodule : Submodule R (∀ j, F.obj j) :=
  {
    AddGrpCat.sectionsAddSubgroup.{v, w}
      (F ⋙
        forget₂ (ModuleCat R) AddCommGrpCat.{w} ⋙
          forget₂ AddCommGrpCat
            AddGrpCat.{w}) with
    carrier := (F ⋙ forget (ModuleCat R)).sections
    smul_mem' := fun r s sh j j' f => by simpa [Functor.sections, forget_map] using congr_arg (r • ·) (sh f) }

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