freeHomEquiv_freeMap — Mathlib

English

The equality (freeHomEquiv (freeMap f)) = freeSection ∘ f holds, i.e., the image under the free-Hom equivalence of the free-map is the canonical section map.

Русский

Сохранение эквивалентности через freeHomEquiv: свободная карта f соответствует канонической секции; то есть (freeHomEquiv (freeMap f)) = freeSection ∘ f.

LaTeX

$$$\mathrm{freeHomEquiv}(\mathrm{freeMap}(f)) = \mathrm{freeSection} \circ f$$$

Lean4

@[simp]
theorem freeHomEquiv_freeMap : (freeHomEquiv _ (freeMap (R := R) f)) = freeSection.comp f :=
  (freeHomEquiv _).symm.injective (by simp; rfl)

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