compLinearMap_injective — Mathlib

English

If f is a surjective linear map, then composing with f on the right induces an injection on the space of alternating maps.

Русский

Если f — сюръективное линейное отображение, то правое композиование с f инжектирует пространство чередующихся отображений.

LaTeX

$$Surjective f \\Rightarrow (g_1.compLinearMap f = g_2.compLinearMap f \\iff g_1 = g_2)$$

Lean4

/-- Composing with a surjective linear map is injective. -/
theorem compLinearMap_injective (f : M₂ →ₗ[R] M) (hf : Function.Surjective f) :
    Function.Injective fun g : M [⋀^ι]→ₗ[R] N => g.compLinearMap f := fun g₁ g₂ h =>
  ext fun x => by simpa [Function.surjInv_eq hf] using AlternatingMap.ext_iff.mp h (Function.surjInv hf ∘ x)

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