sectionsSubalgebra — Mathlib

English

The flat sections of a functor into AlgCat R form a subalgebra of all sections.

Русский

Плоские секции фуктора в AlgCat R образуют подалгебру всех секций.

LaTeX

$$def sectionsSubalgebra : Subalgebra R ((j : J) → (F.obj j).carrier)$$

Lean4

/-- The flat sections of a functor into `AlgCat R` form a submodule of all sections.
-/
def sectionsSubalgebra : Subalgebra R (∀ j, F.obj j) :=
  { SemiRingCat.sectionsSubsemiring (F ⋙ forget₂ (AlgCat R) RingCat.{w} ⋙ forget₂ RingCat SemiRingCat.{w}) with
    algebraMap_mem' := fun r _ _ f => (F.map f).hom.commutes r }

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