freeHomEquiv_symm_comp — Mathlib

English

For any f: M1 → M and p: M → N, the equality N.freeHomEquiv (f ≫ p) i = sectionsMap p (M.freeHomEquiv f i) holds for all i ∈ I.

Русский

Для любых f: M1 → M и p: M → N верно для всех i: N.freeHomEquiv (f ≫ p) i = sectionsMap p (M.freeHomEquiv f i).

LaTeX

$$$N.freeHomEquiv (f \circ p)\, i = \mathrm{sectionsMap}(p, (M.freeHomEquiv\, f)\, i)$$$

Lean4

theorem freeHomEquiv_symm_comp {M N : SheafOfModules.{u} R} {I : Type u} (s : I → M.sections) (p : M ⟶ N) :
    M.freeHomEquiv.symm s ≫ p = N.freeHomEquiv.symm (fun i ↦ sectionsMap p (s i)) :=
  N.freeHomEquiv.injective (by ext; simp [freeHomEquiv_comp_apply])

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