sectionsMk — Mathlib

English

There is a constructor that builds a section of a presheaf from a pointwise choice s and a compatibility condition hs.

Русский

Существуют конструктор, который строит секцию прешефа из покомпонентного выбора и совместимости hs.

LaTeX

$$$ sectionsMk\: {M} (s : \forall X, M(X)) (hs : \forall {X Y} (f : X ⟶ Y), M.map f (s X) = s Y) : M.sections $$$

Lean4

/-- Constructor for sections of a presheaf of modules. -/
@[simps]
def sectionsMk {M : PresheafOfModules.{v} R} (s : ∀ X, M.obj X) (hs : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), M.map f (s X) = s Y) :
    M.sections where
  val := s
  property f := hs f

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