linear_injective_iff — Mathlib

English

The map sending an affine endomorphism to its linear part is a MonoidHom: (P1 →ᵃ[k] P1) →* (V1 → V1).

Русский

Отображение, отправляющее аффинный эндоморфизм в его линейную часть, является моноидомом: (P1 →ᵃ[k] P1) →* (V1 → V1).

LaTeX

$$$\\mathrm{linearHom}: (P_1 \\to\\!^a_k P_1) \\to^* (V_1 \\to V_1)$ with toFun = \\mathrm{linear}$, map_one' = rfl, map_mul' = rfl$$

Lean4

@[simp]
theorem linear_injective_iff (f : P1 →ᵃ[k] P2) : Function.Injective f.linear ↔ Function.Injective f :=
  by
  obtain ⟨p⟩ := (inferInstance : Nonempty P1)
  have h : ⇑f.linear = (Equiv.vaddConst (f p)).symm ∘ f ∘ Equiv.vaddConst p :=
    by
    ext v
    simp [f.map_vadd]
  rw [h, Equiv.comp_injective, Equiv.injective_comp]

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