span_range_inclusion_eq_top — Mathlib

English

The inclusionSpan map for submodules is injective.

Русский

Отображение inclusionSpan для подмодулей инъективно.

LaTeX

$$Injective inclusionSpan: p ↦ inclusionSpan(S,p)$$

Lean4

theorem span_range_inclusion_eq_top (p : Submodule R M) (q : Submodule S M) (h₁ : p ≤ q.restrictScalars R)
    (h₂ : q ≤ span S p) : span S (range (inclusion h₁)) = ⊤ :=
  by
  suffices (span S (range (inclusion h₁))).map q.subtype = q
    by
    apply map_injective_of_injective q.injective_subtype
    rw [this, q.map_subtype_top]
  rw [map_span]
  suffices q.subtype '' ((LinearMap.range (inclusion h₁)) : Set <| q.restrictScalars R) = p
    by
    refine this ▸ le_antisymm ?_ h₂
    simpa using span_mono (R := S) h₁
  ext x
  simpa [range_inclusion] using fun hx ↦ h₁ hx

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