unitHomEquiv_symm_comp — Mathlib

English

The inverse bijection is compatible with composition, mirroring the forward compatibility.

Русский

Обратная биекция совместима с композицией, аналогично прямой совместимости.

LaTeX

$$$M.\mathrm{unitHomEquiv}.symm(s) \gg p = N.\mathrm{unitHomEquiv}.symm(\mathrm{sectionsMap}(p)(s))$$$

Lean4

theorem unitHomEquiv_symm_comp {M N : SheafOfModules.{u} R} (s : M.sections) (p : M ⟶ N) :
    M.unitHomEquiv.symm s ≫ p = N.unitHomEquiv.symm (sectionsMap p s) :=
  N.unitHomEquiv.injective (by simp [unitHomEquiv_comp_apply])

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