freeHomEquiv_comp_apply — Mathlib

English

For a family s: I → M.sections and a morphism p: M → N, the relation M.freeHomEquiv.symm s ≫ p = N.freeHomEquiv.symm (fun i ↦ sectionsMap p (s i)) holds.

Русский

Для семейства s: I → разделы M и гомоморфизма p: M → N выполняется равенство M.freeHomEquiv.symm s ≫ p = N.freeHomEquiv.symm (fun i → sectionsMap p (s i)).

LaTeX

$$$M.freeHomEquiv^{-1}(s) \circ p = N.freeHomEquiv^{-1}(\lambda i.\mathrm{sectionsMap}(p, s(i)))$$$

Lean4

theorem freeHomEquiv_comp_apply {M N : SheafOfModules.{u} R} {I : Type u} (f : free I ⟶ M) (p : M ⟶ N) (i : I) :
    N.freeHomEquiv (f ≫ p) i = sectionsMap p (M.freeHomEquiv f i) :=
  rfl

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