map_smul — Mathlib

English

For a ring homomorphism f: A → B, the lift map kerLift: A/(ker f) → B is linear over the base ring; in particular, it respects scalars: kerLift(r·x) = r·kerLift(x) for r in the base ring and x in A/(ker f).

Русский

Пусть f: A → B — кольцевой гомоморфизм. Лифт-отображение kerLift: A/(ker f) → B является линейным относительно основания: kerLift(r·x) = r·kerLift(x).

LaTeX

$$$\; kerLift(f)(r \cdot x) = r \cdot kerLift(f)(x)$$$

Lean4

theorem map_smul (f : A →ₐ[R₁] B) (r : R₁) (x : A ⧸ (RingHom.ker f)) : f.kerLift (r • x) = r • f.kerLift x :=
  by
  obtain ⟨a, rfl⟩ := Quotient.mkₐ_surjective R₁ _ x
  exact _root_.map_smul f _ _

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