map_apply — Mathlib

English

If h is surjective, then the induced map map S f g h is surjective between localized modules.

Русский

Если h сюръективно, то отображение map S f g h сюръективно между локализованными модулями.

LaTeX

$$$$ \\text{Surjective } h \\;\\Rightarrow\\; \\text{Surjective } (\\text{map } S f g h) $$$$

Lean4

@[simp]
theorem map_apply (h : M →ₗ[R] N) (x) : map S f g h (f x) = g (h x) :=
  lift_apply S f (g ∘ₗ h) (IsLocalizedModule.map_units g) x

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