dualSubmoduleToDual_injective — Mathlib

English

If B is nondegenerate and N spans M over S, then the map B.dualSubmoduleToDual N is injective; equivalently, x ≠ x' ⇒ B(x,·) ≠ B(x',·) on N.

Русский

Если B нондеґенеративна и N порождает M как S-область, то отображение B.dualSubmoduleToDual N инъективно; эквивалентно тому, что B(x,·) различно от B(x',·) на N при x ≠ x'.

LaTeX

$$$$ B.Nondegenerate \,\rightarrow\, \text{ span}_S(N)=M \Rightarrow \text{Injective}(B.dualSubmoduleToDual N). $$$$

Lean4

theorem dualSubmoduleToDual_injective (hB : B.Nondegenerate) [NoZeroSMulDivisors R S] (N : Submodule R M)
    (hN : Submodule.span S (N : Set M) = ⊤) : Function.Injective (B.dualSubmoduleToDual N) :=
  by
  intro x y e
  ext
  apply LinearMap.ker_eq_bot.mp hB.ker_eq_bot
  apply LinearMap.ext_on hN
  intro z hz
  simpa using congr_arg (algebraMap R S) (LinearMap.congr_fun e ⟨z, hz⟩)

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