Mathlib.LinearAlgebra.Span.Basic

Submodule.span_coe_eq_restrictScalars theorem

[Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : span S (p : Set M) = p.restrictScalars S

Full source

/-- A version of `Submodule.span_eq` for when the span is by a smaller ring. -/
@[simp]
theorem span_coe_eq_restrictScalars [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
    span S (p : Set M) = p.restrictScalars S :=
  span_eq (p.restrictScalars S)

Span Equals Restriction of Scalars for Compatible Module Structures

Informal description

Let $R$ and $S$ be semirings, with $S$ acting on $R$ via scalar multiplication. Let $M$ be an $S$-module that is also an $R$-module, such that the scalar multiplication is compatible (i.e., $s \cdot (r \cdot m) = (s \cdot r) \cdot m$ for all $s \in S$, $r \in R$, $m \in M$). Then for any submodule $p$ of $M$ viewed as an $R$-module, the $S$-span of $p$ (as a subset of $M$) equals $p$ when considered as an $S$-submodule via restriction of scalars. In symbols: \[ \operatorname{span}_S (p) = p_{\text{restrictScalars } S}. \]

Submodule.image_span_subset theorem

(f : F) (s : Set M) (N : Submodule R₂ M₂) : f '' span R s ⊆ N ↔ ∀ m ∈ s, f m ∈ N

Full source

/-- A version of `Submodule.map_span_le` that does not require the `RingHomSurjective`
assumption. -/
theorem image_span_subset (f : F) (s : Set M) (N : Submodule R₂ M₂) :
    f '' span R sf '' span R s ⊆ Nf '' span R s ⊆ N ↔ ∀ m ∈ s, f m ∈ N := image_subset_iff.trans <| span_le (p := N.comap f)

Image of Span Under Module Homomorphism is Contained in Submodule iff Elements are Mapped into Submodule

Informal description

Let $R$ and $R_2$ be rings, $M$ an $R$-module, $M_2$ an $R_2$-module, and $F$ a type of module homomorphisms from $M$ to $M_2$. For any module homomorphism $f \in F$, any subset $s \subseteq M$, and any submodule $N \subseteq M_2$, the image of the span of $s$ under $f$ is contained in $N$ if and only if for every $m \in s$, $f(m)$ belongs to $N$. In symbols: \[ f(\operatorname{span}_R s) \subseteq N \leftrightarrow \forall m \in s, f(m) \in N. \]

Submodule.image_span_subset_span theorem

(f : F) (s : Set M) : f '' span R s ⊆ span R₂ (f '' s)

Full source

theorem image_span_subset_span (f : F) (s : Set M) : f '' span R sf '' span R s ⊆ span R₂ (f '' s) :=
  (image_span_subset f s _).2 fun x hx ↦ subset_span ⟨x, hx, rfl⟩

Image of Span Under Module Homomorphism is Contained in Span of Image

Informal description

Let $R$ and $R_2$ be rings, $M$ an $R$-module, $M_2$ an $R_2$-module, and $F$ a type of module homomorphisms from $M$ to $M_2$. For any module homomorphism $f \in F$ and any subset $s \subseteq M$, the image of the span of $s$ under $f$ is contained in the span of the image of $s$ under $f$. In symbols: \[ f(\operatorname{span}_R s) \subseteq \operatorname{span}_{R_2} (f(s)). \]

Submodule.map_span theorem

[RingHomSurjective σ₁₂] (f : F) (s : Set M) : (span R s).map f = span R₂ (f '' s)

Full source

theorem map_span [RingHomSurjective σ₁₂] (f : F) (s : Set M) :
    (span R s).map f = span R₂ (f '' s) :=
  Eq.symm <| span_eq_of_le _ (Set.image_subset f subset_span) (image_span_subset_span f s)

Image of Span Equals Span of Image under Module Homomorphism

Informal description

Let $R$ and $R_2$ be rings, $M$ an $R$-module, $M_2$ an $R_2$-module, and $F$ a type of module homomorphisms from $M$ to $M_2$. Given a surjective ring homomorphism $\sigma_{12} \colon R \to R_2$, a module homomorphism $f \in F$, and a subset $s \subseteq M$, the image of the span of $s$ under $f$ equals the span of the image of $s$ under $f$. In symbols: \[ f(\operatorname{span}_R s) = \operatorname{span}_{R_2} (f(s)). \]

Submodule.map_span_le theorem

 [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) : map f (span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N

Full source

theorem map_span_le [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) :
    mapmap f (span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N := image_span_subset f s N

Image of Span Under Module Homomorphism is Contained in Submodule iff Elements are Mapped into Submodule

Informal description

Let $R$ and $R_2$ be rings, $M$ an $R$-module, $M_2$ an $R_2$-module, and $F$ a type of module homomorphisms from $M$ to $M_2$. For any surjective ring homomorphism $\sigma_{12} \colon R \to R_2$, any module homomorphism $f \in F$, any subset $s \subseteq M$, and any submodule $N \subseteq M_2$, the image of the span of $s$ under $f$ is contained in $N$ if and only if for every $m \in s$, $f(m)$ belongs to $N$. In symbols: \[ f(\operatorname{span}_R s) \subseteq N \leftrightarrow \forall m \in s, f(m) \in N. \]

Submodule.span_preimage_le theorem

(f : F) (s : Set M₂) : span R (f ⁻¹' s) ≤ (span R₂ s).comap f

Full source

theorem span_preimage_le (f : F) (s : Set M₂) :
    span R (f ⁻¹' s) ≤ (span R₂ s).comap f := by
  rw [span_le, comap_coe]
  exact preimage_mono subset_span

Span of Preimage is Contained in Preimage of Span

Informal description

For any linear map $f \colon M \to M₂$ between $R$-modules and any subset $s \subseteq M₂$, the span of the preimage $f^{-1}(s)$ in $M$ is contained in the preimage of the span of $s$ under $f$. In other words: $$\operatorname{span}_R(f^{-1}(s)) \leq f^{-1}(\operatorname{span}_{R₂}(s))$$

Submodule.linearMap_eq_iff_of_eq_span theorem

 {V : Submodule R M} (f g : V →ₗ[R] N) {S : Set M} (hV : V = span R S) :
  f = g ↔
    ∀ (s : S),
      f ⟨s, by simpa only [hV] using subset_span (by simp)⟩ = g ⟨s, by simpa only [hV] using subset_span (by simp)⟩

Full source

lemma linearMap_eq_iff_of_eq_span {V : Submodule R M} (f g : V →ₗ[R] N)
    {S : Set M} (hV : V = span R S) :
    f = g ↔ ∀ (s : S), f ⟨s, by simpa only [hV] using subset_span (by simp)⟩ =
      g ⟨s, by simpa only [hV] using subset_span (by simp)⟩ := by
  constructor
  · rintro rfl _
    rfl
  · intro h
    subst hV
    suffices ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩ by
      ext ⟨x, hx⟩
      exact this x hx
    intro x hx
    induction hx using span_induction with
    | mem x hx => exact h ⟨x, hx⟩
    | zero => erw [map_zero, map_zero]
    | add x y hx hy hx' hy' =>
        erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]
        rw [hx', hy']
    | smul a x hx hx' =>
        erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨x, hx⟩]
        rw [hx']

Equality of Linear Maps on Span-Generated Submodule

Informal description

Let $V$ be a submodule of an $R$-module $M$ such that $V = \operatorname{span}_R S$ for some subset $S \subseteq M$. For any two linear maps $f, g \colon V \to N$, the following are equivalent: 1. $f = g$ as linear maps. 2. For every $s \in S$, $f(s) = g(s)$.

Submodule.linearMap_eq_iff_of_span_eq_top theorem

(f g : M →ₗ[R] N) {S : Set M} (hM : span R S = ⊤) : f = g ↔ ∀ (s : S), f s = g s

Full source

lemma linearMap_eq_iff_of_span_eq_top (f g : M →ₗ[R] N)
    {S : Set M} (hM : span R S = ⊤) :
    f = g ↔ ∀ (s : S), f s = g s := by
  convert linearMap_eq_iff_of_eq_span (f.comp (Submodule.subtype _))
    (g.comp (Submodule.subtype _)) hM.symm
  constructor
  · rintro rfl
    rfl
  · intro h
    ext x
    exact DFunLike.congr_fun h ⟨x, by simp⟩

Equality of Linear Maps Determined by Spanning Set

Informal description

Let $M$ and $N$ be $R$-modules, and let $S$ be a subset of $M$ such that $\operatorname{span}_R S = M$. For any two linear maps $f, g \colon M \to N$, the following are equivalent: 1. $f = g$ as linear maps. 2. For every $s \in S$, $f(s) = g(s)$.

Submodule.linearMap_eq_zero_iff_of_span_eq_top theorem

(f : M →ₗ[R] N) {S : Set M} (hM : span R S = ⊤) : f = 0 ↔ ∀ (s : S), f s = 0

Full source

lemma linearMap_eq_zero_iff_of_span_eq_top (f : M →ₗ[R] N)
    {S : Set M} (hM : span R S = ⊤) :
    f = 0 ↔ ∀ (s : S), f s = 0 :=
  linearMap_eq_iff_of_span_eq_top f 0 hM

Zero Linear Map Criterion via Spanning Set: $f = 0$ iff $f|_S = 0$ when $\operatorname{span}_R S = M$

Informal description

Let $M$ and $N$ be $R$-modules, and let $S$ be a subset of $M$ such that $\operatorname{span}_R S = M$. For any linear map $f \colon M \to N$, the following are equivalent: 1. $f$ is the zero map. 2. For every $s \in S$, $f(s) = 0$.

Submodule.linearMap_eq_zero_iff_of_eq_span theorem

 {V : Submodule R M} (f : V →ₗ[R] N) {S : Set M} (hV : V = span R S) :
  f = 0 ↔ ∀ (s : S), f ⟨s, by simpa only [hV] using subset_span (by simp)⟩ = 0

Full source

lemma linearMap_eq_zero_iff_of_eq_span {V : Submodule R M} (f : V →ₗ[R] N)
    {S : Set M} (hV : V = span R S) :
    f = 0 ↔ ∀ (s : S), f ⟨s, by simpa only [hV] using subset_span (by simp)⟩ = 0 :=
  linearMap_eq_iff_of_eq_span f 0 hV

Zero Linear Map Criterion on Span-Generated Submodule

Informal description

Let $V$ be a submodule of an $R$-module $M$ such that $V = \operatorname{span}_R S$ for some subset $S \subseteq M$. For any linear map $f \colon V \to N$, the following are equivalent: 1. $f$ is the zero map. 2. For every $s \in S$, $f(s) = 0$.

Submodule.span_smul_eq_of_isUnit theorem

(s : Set M) (r : R) (hr : IsUnit r) : span R (r • s) = span R s

Full source

/-- See `Submodule.span_smul_eq` (in `RingTheory.Ideal.Operations`) for
`span R (r • s) = r • span R s` that holds for arbitrary `r` in a `CommSemiring`. -/
theorem span_smul_eq_of_isUnit (s : Set M) (r : R) (hr : IsUnit r) : span R (r • s) = span R s := by
  apply le_antisymm
  · apply span_smul_le
  · convert span_smul_le (r • s) ((hr.unit⁻¹ :) : R)
    simp [smul_smul]

Span Equality under Scalar Multiplication by a Unit: $\operatorname{span}_R (r \cdot s) = \operatorname{span}_R s$ for $r$ invertible

Informal description

For any subset $s$ of an $R$-module $M$ and any unit $r \in R$ (i.e., $r$ is invertible in $R$), the span of the scaled set $r \cdot s$ is equal to the span of $s$, i.e., $$\operatorname{span}_R (r \cdot s) = \operatorname{span}_R s.$$

Submodule.coe_scott_continuous theorem

: OmegaCompletePartialOrder.ωScottContinuous ((↑) : Submodule R M → Set M)

Full source

/-- We can regard `coe_iSup_of_chain` as the statement that `(↑) : (Submodule R M) → Set M` is
Scott continuous for the ω-complete partial order induced by the complete lattice structures. -/
theorem coe_scott_continuous :
    OmegaCompletePartialOrder.ωScottContinuous ((↑) : Submodule R M → Set M) :=
  OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup
    ⟨SetLike.coe_mono, coe_iSup_of_chain⟩

$\omega$-Scott Continuity of Submodule Coercion to Sets

Informal description

The coercion function $(↑) : \text{Submodule}_R M \to \text{Set } M$, which maps a submodule to its underlying set, is $\omega$-Scott continuous. That is, for any increasing chain $(a_k)_{k \in \mathbb{N}}$ of submodules, the underlying set of the supremum $\bigsqcup_k a_k$ is equal to the union $\bigcup_k (a_k : \text{Set } M)$ of the underlying sets of the submodules in the chain.

Submodule.inclusionSpan definition

: p →ₗ[R] span S (p : Set M)

Full source

/-- The inclusion of an `R`-submodule into its `S`-span, as an `R`-linear map. -/
@[simps] def inclusionSpan :
    p →ₗ[R] span S (p : Set M) where
  toFun x := ⟨x, subset_span x.property⟩
  map_add' x y := by simp
  map_smul' t x := by simp

Inclusion map into span

Informal description

The inclusion map from an $R$-submodule $p$ into its $S$-span, viewed as an $R$-linear map. Specifically, it sends each element $x \in p$ to itself considered as an element of the span of $p$ over $S$.

Submodule.injective_inclusionSpan theorem

: Injective (p.inclusionSpan S)

Full source

lemma injective_inclusionSpan :
    Injective (p.inclusionSpan S) := by
  intro x y hxy
  rw [Subtype.ext_iff] at hxy
  simpa using hxy

Injectivity of the Inclusion Map into Span

Informal description

The inclusion map from an $R$-submodule $p$ into its $S$-span is injective. That is, for any $x, y \in p$, if $x$ and $y$ have the same image under the inclusion map, then $x = y$.

Submodule.span_range_inclusionSpan theorem

: span S (range <| p.inclusionSpan S) = ⊤

Full source

lemma span_range_inclusionSpan :
    span S (range <| p.inclusionSpan S) = ⊤ := by
  have : (span S (p : Set M)).subtype '' range (inclusionSpan S p) = p := by
    ext; simpa [Subtype.ext_iff] using fun h ↦ subset_span h
  apply map_injective_of_injective (span S (p : Set M)).injective_subtype
  rw [map_subtype_top, map_span, this]

Span of Inclusion Range Equals Entire Module

Informal description

For any $R$-submodule $p$ of an $S$-module $M$, the span of the range of the inclusion map from $p$ into its $S$-span is equal to the entire module, i.e., \[ \operatorname{span}_S (\operatorname{range} (p \hookrightarrow \operatorname{span}_S p)) = M. \]

Submodule.span_le_restrictScalars theorem

: span R s ≤ (span S s).restrictScalars R

Full source

/-- If `R` is "smaller" ring than `S` then the span by `R` is smaller than the span by `S`. -/
theorem span_le_restrictScalars :
    span R s ≤ (span S s).restrictScalars R :=
  Submodule.span_le.2 Submodule.subset_span

Inclusion of $R$-span in $S$-span restriction

Informal description

For any subset $s$ of an $R$-module $M$ and any ring extension $S$ of $R$, the $R$-span of $s$ is contained in the $R$-restriction of the $S$-span of $s$. In other words: $$\operatorname{span}_R s \leq (\operatorname{span}_S s)\big|_R$$

Submodule.span_subset_span theorem

: ↑(span R s) ⊆ (span S s : Set M)

Full source

/-- A version of `Submodule.span_le_restrictScalars` with coercions. -/
@[simp]
theorem span_subset_span :
    ↑(span R s) ⊆ (span S s : Set M) :=
  span_le_restrictScalars R S s

Inclusion of $R$-span in $S$-span

Informal description

For any subset $s$ of an $R$-module $M$ and any ring extension $S$ of $R$, the set underlying the $R$-span of $s$ is contained in the set underlying the $S$-span of $s$. In other words: $$\operatorname{span}_R s \subseteq \operatorname{span}_S s$$

Submodule.span_span_of_tower theorem

: span S (span R s : Set M) = span S s

Full source

/-- Taking the span by a large ring of the span by the small ring is the same as taking the span
by just the large ring. -/
@[simp]
theorem span_span_of_tower :
    span S (span R s : Set M) = span S s :=
  le_antisymm (span_le.2 <| span_subset_span R S s) (span_mono subset_span)

Double Span Equality: $\operatorname{span}_S (\operatorname{span}_R s) = \operatorname{span}_S s$

Informal description

For any subset $s$ of an $R$-module $M$ and any ring extension $S$ of $R$, the $S$-span of the $R$-span of $s$ is equal to the $S$-span of $s$. In other words: $$\operatorname{span}_S (\operatorname{span}_R s) = \operatorname{span}_S s$$

Submodule.span_eq_top_of_span_eq_top theorem

(s : Set M) (hs : span R s = ⊤) : span S s = ⊤

Full source

theorem span_eq_top_of_span_eq_top (s : Set M) (hs : span R s = ⊤) : span S s = ⊤ :=
  le_top.antisymm (hs.ge.trans (span_le_restrictScalars R S s))

Span Equality Transfer: $\operatorname{span}_R s = \top$ implies $\operatorname{span}_S s = \top$

Informal description

For any subset $s$ of an $R$-module $M$, if the $R$-span of $s$ is the entire module $M$ (i.e., $\operatorname{span}_R s = \top$), then the $S$-span of $s$ is also the entire module $M$ (i.e., $\operatorname{span}_S s = \top$), where $S$ is a ring extension of $R$.

Submodule.span_range_inclusion_eq_top theorem

 (p : Submodule R M) (q : Submodule S M) (h₁ : p ≤ q.restrictScalars R) (h₂ : q ≤ span S p) :
  span S (range (inclusion h₁)) = ⊤

Full source

lemma 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

Span of Inclusion Range Equals Top Module under Compatible Submodule Conditions

Informal description

Let $R$ and $S$ be rings, and let $M$ be an $R$-module that is also an $S$-module. Given two submodules $p \subseteq M$ as an $R$-module and $q \subseteq M$ as an $S$-module, if $p$ is contained in $q$ when $q$ is viewed as an $R$-module via restriction of scalars (i.e., $p \leq q_{\text{restrictScalars } R}$), and $q$ is contained in the $S$-span of $p$ (i.e., $q \leq \operatorname{span}_S p$), then the $S$-span of the range of the inclusion map from $p$ to $q$ is the entire module $M$ (i.e., $\operatorname{span}_S (\text{range } (\iota_{h_1})) = \top$).

Submodule.span_range_inclusion_restrictScalars_eq_top theorem

: span S (range (inclusion <| span_le_restrictScalars R S s)) = ⊤

Full source

@[simp]
theorem span_range_inclusion_restrictScalars_eq_top :
    span S (range (inclusion <| span_le_restrictScalars R S s)) = ⊤ :=
  span_range_inclusion_eq_top _ _ _ <| by simp

$S$-span of inclusion range equals top module under scalar restriction

Informal description

Let $R$ and $S$ be rings with $R \subseteq S$, and let $M$ be an $S$-module (and hence also an $R$-module by restriction of scalars). For any subset $s \subseteq M$, the $S$-span of the range of the inclusion map from the $R$-span of $s$ to its $S$-span is the entire module $M$. In symbols: \[ \operatorname{span}_S \left( \text{range} \left( \iota : \operatorname{span}_R s \hookrightarrow \operatorname{span}_S s \right) \right) = M. \]

Submodule.span_singleton_eq_span_singleton theorem

 {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x y : M} :
  ((R ∙ x) = R ∙ y) ↔ ∃ z : Rˣ, z • x = y

Full source

theorem span_singleton_eq_span_singleton {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
    [NoZeroSMulDivisors R M] {x y : M} : ((R ∙ x) = R ∙ y) ↔ ∃ z : Rˣ, z • x = y := by
  constructor
  · simp only [le_antisymm_iff, span_singleton_le_iff_mem, mem_span_singleton]
    rintro ⟨⟨a, rfl⟩, b, hb⟩
    rcases eq_or_ne y 0 with rfl | hy; · simp
    refine ⟨⟨b, a, ?_, ?_⟩, hb⟩
    · apply smul_left_injective R hy
      simpa only [mul_smul, one_smul]
    · rw [← hb] at hy
      apply smul_left_injective R (smul_ne_zero_iff.1 hy).2
      simp only [mul_smul, one_smul, hb]
  · rintro ⟨u, rfl⟩
    exact (span_singleton_group_smul_eq _ _ _).symm

Equality of Singleton Spans via Unit Scalar Multiplication

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any two elements $x, y \in M$, the span of the singleton $\{x\}$ equals the span of the singleton $\{y\}$ if and only if there exists a unit $z \in R^\times$ such that $z \cdot x = y$.

Submodule.span_image theorem

[RingHomSurjective σ₁₂] (f : F) : span R₂ (f '' s) = map f (span R s)

Full source

theorem span_image [RingHomSurjective σ₁₂] (f : F) :
    span R₂ (f '' s) = map f (span R s) :=
  (map_span f s).symm

Span-Image Commutation for Module Homomorphisms

Informal description

Let $R$ and $R_2$ be rings, $M$ an $R$-module, $M_2$ an $R_2$-module, and $F$ a type of module homomorphisms from $M$ to $M_2$. Given a surjective ring homomorphism $\sigma_{12} \colon R \to R_2$ and a module homomorphism $f \in F$, the span of the image of a subset $s \subseteq M$ under $f$ equals the image of the span of $s$ under $f$. In symbols: \[ \operatorname{span}_{R_2} (f(s)) = f(\operatorname{span}_R s). \]

Submodule.span_image' theorem

[RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) : span R₂ (f '' s) = map f (span R s)

Full source

@[simp] -- Should be replaced with `Submodule.span_image` when https://github.com/leanprover/lean4/pull/3701 is fixed.
theorem span_image' [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) :
    span R₂ (f '' s) = map f (span R s) :=
  span_image _

Span-Image Commutation for Linear Maps

Informal description

Let $R$ and $R_2$ be rings, $M$ an $R$-module, $M_2$ an $R_2$-module, and $\sigma_{12} \colon R \to R_2$ a surjective ring homomorphism. For any $\sigma_{12}$-linear map $f \colon M \to M_2$ and subset $s \subseteq M$, the span of the image $f(s)$ in $M_2$ equals the image under $f$ of the span of $s$ in $M$. In symbols: \[ \operatorname{span}_{R_2} (f(s)) = f(\operatorname{span}_R s). \]

Submodule.apply_mem_span_image_of_mem_span theorem

 [RingHomSurjective σ₁₂] (f : F) {x : M} {s : Set M} (h : x ∈ Submodule.span R s) : f x ∈ Submodule.span R₂ (f '' s)

Full source

theorem apply_mem_span_image_of_mem_span [RingHomSurjective σ₁₂] (f : F) {x : M}
    {s : Set M} (h : x ∈ Submodule.span R s) : f x ∈ Submodule.span R₂ (f '' s) := by
  rw [Submodule.span_image]
  exact Submodule.mem_map_of_mem h

Module Homomorphism Preserves Span Membership Under Image

Informal description

Let $R$ and $R_2$ be rings, $M$ an $R$-module, $M_2$ an $R_2$-module, and $F$ a type of module homomorphisms from $M$ to $M_2$. Given a surjective ring homomorphism $\sigma_{12} \colon R \to R_2$ and a module homomorphism $f \in F$, if an element $x \in M$ belongs to the span of a subset $s \subseteq M$, then the image $f(x)$ belongs to the span of the image $f(s)$ in $M_2$. In symbols: \[ x \in \operatorname{span}_R s \implies f(x) \in \operatorname{span}_{R_2} (f(s)). \]

Submodule.apply_mem_span_image_iff_mem_span theorem

 [RingHomSurjective σ₁₂] {f : F} {x : M} {s : Set M} (hf : Function.Injective f) :
  f x ∈ Submodule.span R₂ (f '' s) ↔ x ∈ Submodule.span R s

Full source

theorem apply_mem_span_image_iff_mem_span [RingHomSurjective σ₁₂] {f : F} {x : M}
    {s : Set M} (hf : Function.Injective f) :
    f x ∈ Submodule.span R₂ (f '' s)f x ∈ Submodule.span R₂ (f '' s) ↔ x ∈ Submodule.span R s := by
  rw [← Submodule.mem_comap, ← Submodule.map_span, Submodule.comap_map_eq_of_injective hf]

Injective Module Homomorphism Preserves Span Membership

Informal description

Let $R$ and $R_2$ be rings, $M$ an $R$-module, $M_2$ an $R_2$-module, and $F$ a type of module homomorphisms from $M$ to $M_2$. Given a surjective ring homomorphism $\sigma_{12} \colon R \to R_2$, an injective module homomorphism $f \in F$, an element $x \in M$, and a subset $s \subseteq M$, the following equivalence holds: \[ f(x) \in \operatorname{span}_{R_2} (f(s)) \leftrightarrow x \in \operatorname{span}_R s. \]

Submodule.map_subtype_span_singleton theorem

{p : Submodule R M} (x : p) : map p.subtype (R ∙ x) = R ∙ (x : M)

Full source

@[simp]
theorem map_subtype_span_singleton {p : Submodule R M} (x : p) :
    map p.subtype (R ∙ x) = R ∙ (x : M) := by simp [← span_image]

Image of Span under Submodule Inclusion Equals Span in Ambient Module

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $p$ a submodule of $M$. For any element $x \in p$, the image of the span $R \cdot x$ under the inclusion map $p \hookrightarrow M$ is equal to the span $R \cdot x$ in $M$.

Submodule.not_mem_span_of_apply_not_mem_span_image theorem

 [RingHomSurjective σ₁₂] (f : F) {x : M} {s : Set M} (h : f x ∉ Submodule.span R₂ (f '' s)) : x ∉ Submodule.span R s

Full source

/-- `f` is an explicit argument so we can `apply` this theorem and obtain `h` as a new goal. -/
theorem not_mem_span_of_apply_not_mem_span_image [RingHomSurjective σ₁₂] (f : F) {x : M}
    {s : Set M} (h : f x ∉ Submodule.span R₂ (f '' s)) : x ∉ Submodule.span R s :=
  h.imp (apply_mem_span_image_of_mem_span f)

Contrapositive of Span Preservation Under Module Homomorphism

Informal description

Let $R$ and $R_2$ be rings, $M$ an $R$-module, $M_2$ an $R_2$-module, and $F$ a type of module homomorphisms from $M$ to $M_2$. Given a surjective ring homomorphism $\sigma_{12} \colon R \to R_2$ and a module homomorphism $f \in F$, if the image $f(x)$ does not belong to the span of $f(s)$ in $M_2$, then $x$ does not belong to the span of $s$ in $M$. In symbols: \[ f(x) \notin \operatorname{span}_{R_2} (f(s)) \implies x \notin \operatorname{span}_R s. \]

Submodule.iSup_toAddSubmonoid theorem

{ι : Sort*} (p : ι → Submodule R M) : (⨆ i, p i).toAddSubmonoid = ⨆ i, (p i).toAddSubmonoid

Full source

theorem iSup_toAddSubmonoid {ι : Sort*} (p : ι → Submodule R M) :
    (⨆ i, p i).toAddSubmonoid = ⨆ i, (p i).toAddSubmonoid := by
  refine le_antisymm (fun x => ?_) (iSup_le fun i => toAddSubmonoid_mono <| le_iSup _ i)
  simp_rw [iSup_eq_span, AddSubmonoid.iSup_eq_closure, mem_toAddSubmonoid, coe_toAddSubmonoid]
  intro hx
  refine Submodule.span_induction (fun x hx => ?_) ?_ (fun x y _ _ hx hy => ?_)
    (fun r x _ hx => ?_) hx
  · exact AddSubmonoid.subset_closure hx
  · exact AddSubmonoid.zero_mem _
  · exact AddSubmonoid.add_mem _ hx hy
  · refine AddSubmonoid.closure_induction ?_ ?_ ?_ hx
    · rintro x ⟨_, ⟨i, rfl⟩, hix : x ∈ p i⟩
      apply AddSubmonoid.subset_closure (Set.mem_iUnion.mpr ⟨i, _⟩)
      exact smul_mem _ r hix
    · rw [smul_zero]
      exact AddSubmonoid.zero_mem _
    · intro x y _ _ hx hy
      rw [smul_add]
      exact AddSubmonoid.add_mem _ hx hy

Supremum of Submodules Preserves Additive Submonoid Structure

Informal description

For any family of submodules $\{p_i\}_{i \in \iota}$ of an $R$-module $M$, the additive submonoid associated with the supremum of the submodules $p_i$ is equal to the supremum of the additive submonoids associated with each $p_i$. That is: $$(\bigsqcup_i p_i).\text{toAddSubmonoid} = \bigsqcup_i (p_i.\text{toAddSubmonoid})$$

Submodule.iSup_induction theorem

 {ι : Sort*} (p : ι → Submodule R M) {motive : M → Prop} {x : M} (hx : x ∈ ⨆ i, p i) (mem : ∀ (i), ∀ x ∈ p i, motive x)
  (zero : motive 0) (add : ∀ x y, motive x → motive y → motive (x + y)) : motive x

Full source

/-- An induction principle for elements of `⨆ i, p i`.
If `C` holds for `0` and all elements of `p i` for all `i`, and is preserved under addition,
then it holds for all elements of the supremum of `p`. -/
@[elab_as_elim]
theorem iSup_induction {ι : Sort*} (p : ι → Submodule R M) {motive : M → Prop} {x : M}
    (hx : x ∈ ⨆ i, p i) (mem : ∀ (i), ∀ x ∈ p i, motive x) (zero : motive 0)
    (add : ∀ x y, motive x → motive y → motive (x + y)) : motive x := by
  rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx
  exact AddSubmonoid.iSup_induction (x := x) _ hx mem zero add

Induction Principle for Elements in the Supremum of Submodules

Informal description

Let $\{p_i\}_{i \in \iota}$ be a family of submodules of an $R$-module $M$, and let $x \in \bigsqcup_i p_i$. Suppose a predicate $\text{motive}$ on $M$ satisfies: 1. $\text{motive}(x)$ holds for all $x \in p_i$ for every $i$, 2. $\text{motive}(0)$ holds, and 3. $\text{motive}$ is preserved under addition (i.e., $\text{motive}(x)$ and $\text{motive}(y)$ imply $\text{motive}(x + y)$). Then $\text{motive}(x)$ holds for all $x \in \bigsqcup_i p_i$.

Submodule.iSup_induction' theorem

 {ι : Sort*} (p : ι → Submodule R M) {motive : ∀ x, (x ∈ ⨆ i, p i) → Prop}
  (mem : ∀ (i) (x) (hx : x ∈ p i), motive x (mem_iSup_of_mem i hx)) (zero : motive 0 (zero_mem _))
  (add : ∀ x y hx hy, motive x hx → motive y hy → motive (x + y) (add_mem ‹_› ‹_›)) {x : M} (hx : x ∈ ⨆ i, p i) :
  motive x hx

Full source

/-- A dependent version of `submodule.iSup_induction`. -/
@[elab_as_elim]
theorem iSup_induction' {ι : Sort*} (p : ι → Submodule R M) {motive : ∀ x, (x ∈ ⨆ i, p i) → Prop}
    (mem : ∀ (i) (x) (hx : x ∈ p i), motive x (mem_iSup_of_mem i hx)) (zero : motive 0 (zero_mem _))
    (add : ∀ x y hx hy, motive x hx → motive y hy → motive (x + y) (add_mem ‹_› ‹_›)) {x : M}
    (hx : x ∈ ⨆ i, p i) : motive x hx := by
  refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, p i) (hc : motive x hx) => hc
  refine iSup_induction p (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_
  · exact ⟨_, mem _ _ hx⟩
  · exact ⟨_, zero⟩
  · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, add _ _ _ _ Cx Cy⟩

Dependent Induction Principle for Elements in the Supremum of Submodules

Informal description

Let $\{p_i\}_{i \in \iota}$ be a family of submodules of an $R$-module $M$, and let $x \in \bigsqcup_i p_i$. Suppose a predicate $\text{motive}$ on elements of $M$ with a proof of membership in $\bigsqcup_i p_i$ satisfies: 1. For every $i$, $\text{motive}(x, h)$ holds for all $x \in p_i$ and any proof $h$ of $x \in \bigsqcup_i p_i$, 2. $\text{motive}(0, h_0)$ holds for the zero element with its membership proof $h_0$, and 3. For any $x, y \in M$ with membership proofs $h_x$ and $h_y$, if $\text{motive}(x, h_x)$ and $\text{motive}(y, h_y)$ hold, then $\text{motive}(x + y, h_{x+y})$ holds for the sum with its membership proof $h_{x+y}$. Then $\text{motive}(x, h_x)$ holds for any $x \in \bigsqcup_i p_i$ with its membership proof $h_x$.

Submodule.singleton_span_isCompactElement theorem

(x : M) : CompleteLattice.IsCompactElement (span R { x } : Submodule R M)

Full source

theorem singleton_span_isCompactElement (x : M) :
    CompleteLattice.IsCompactElement (span R {x} : Submodule R M) := by
  rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]
  intro d hemp hdir hsup
  have : x ∈ (sSup d) := (SetLike.le_def.mp hsup) (mem_span_singleton_self x)
  obtain ⟨y, ⟨hyd, hxy⟩⟩ := (mem_sSup_of_directed hemp hdir).mp this
  exact ⟨y, ⟨hyd, by simpa only [span_le, singleton_subset_iff] ⟩⟩

Compactness of the Span of a Singleton in a Module

Informal description

For any vector $x$ in an $R$-module $M$, the span of the singleton set $\{x\}$ is a compact element in the complete lattice of submodules of $M$.

Submodule.finset_span_isCompactElement theorem

(S : Finset M) : CompleteLattice.IsCompactElement (span R S : Submodule R M)

Full source

/-- The span of a finite subset is compact in the lattice of submodules. -/
theorem finset_span_isCompactElement (S : Finset M) :
    CompleteLattice.IsCompactElement (span R S : Submodule R M) := by
  rw [span_eq_iSup_of_singleton_spans]
  simp only [Finset.mem_coe]
  rw [← Finset.sup_eq_iSup]
  exact
    CompleteLattice.isCompactElement_finsetSup S fun x _ => singleton_span_isCompactElement x

Compactness of the Span of a Finite Set in a Module

Informal description

For any finite subset $S$ of an $R$-module $M$, the span of $S$ is a compact element in the complete lattice of submodules of $M$. That is, for any family of submodules $\{N_i\}_{i \in I}$, if $\text{span}_R(S) \subseteq \bigsqcup_{i \in I} N_i$, then there exists a finite subset $J \subseteq I$ such that $\text{span}_R(S) \subseteq \bigsqcup_{i \in J} N_i$.

Submodule.finite_span_isCompactElement theorem

(S : Set M) (h : S.Finite) : CompleteLattice.IsCompactElement (span R S : Submodule R M)

Full source

/-- The span of a finite subset is compact in the lattice of submodules. -/
theorem finite_span_isCompactElement (S : Set M) (h : S.Finite) :
    CompleteLattice.IsCompactElement (span R S : Submodule R M) :=
  Finite.coe_toFinset h ▸ finset_span_isCompactElement h.toFinset

Compactness of the Span of a Finite Set in a Module Lattice

Informal description

For any finite subset $S$ of an $R$-module $M$, the span of $S$ is a compact element in the complete lattice of submodules of $M$. That is, for any family of submodules $\{N_i\}_{i \in I}$, if $\text{span}_R(S) \subseteq \bigsqcup_{i \in I} N_i$, then there exists a finite subset $J \subseteq I$ such that $\text{span}_R(S) \subseteq \bigsqcup_{i \in J} N_i$.

Submodule.instIsCompactlyGenerated instance

: IsCompactlyGenerated (Submodule R M)

Full source

instance : IsCompactlyGenerated (Submodule R M) :=
  ⟨fun s =>
    ⟨(fun x => span R {x}) '' s,
      ⟨fun t ht => by
        rcases (Set.mem_image _ _ _).1 ht with ⟨x, _, rfl⟩
        apply singleton_span_isCompactElement, by
        rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, span_eq]⟩⟩⟩

Compactly Generated Lattice of Submodules

Informal description

The lattice of submodules of an $R$-module $M$ is compactly generated. This means that every submodule of $M$ can be expressed as the supremum of compact elements, where a compact element is one that satisfies the property that whenever it is less than or equal to the supremum of a directed set of submodules, it is less than or equal to some element in that directed set.

Submodule.prod definition

: Submodule R (M × M')

Full source

/-- The product of two submodules is a submodule. -/
def prod : Submodule R (M × M') :=
  { p.toAddSubmonoid.prod q₁.toAddSubmonoid with
    carrier := p ×ˢ q₁
    smul_mem' := by rintro a ⟨x, y⟩ ⟨hx, hy⟩; exact ⟨smul_mem _ a hx, smul_mem _ a hy⟩ }

Product of submodules

Informal description

The product of two submodules $p$ of $M$ and $q$ of $M'$ is the submodule of $M \times M'$ consisting of all pairs $(x, y)$ where $x \in p$ and $y \in q$, and which is closed under scalar multiplication.

Submodule.prod_coe theorem

: (prod p q₁ : Set (M × M')) = (p : Set M) ×ˢ (q₁ : Set M')

Full source

@[simp]
theorem prod_coe : (prod p q₁ : Set (M × M')) = (p : Set M) ×ˢ (q₁ : Set M') :=
  rfl

Product Submodule as Cartesian Product of Underlying Sets

Informal description

Let $p$ be a submodule of an $R$-module $M$ and $q$ be a submodule of an $R$-module $M'$. Then the underlying set of the product submodule $p \times q$ is equal to the Cartesian product of the underlying sets of $p$ and $q$, i.e., $(p \times q) = p \timesˢ q$.

Submodule.mem_prod theorem

{p : Submodule R M} {q : Submodule R M'} {x : M × M'} : x ∈ prod p q ↔ x.1 ∈ p ∧ x.2 ∈ q

Full source

@[simp]
theorem mem_prod {p : Submodule R M} {q : Submodule R M'} {x : M × M'} :
    x ∈ prod p qx ∈ prod p q ↔ x.1 ∈ p ∧ x.2 ∈ q :=
  Set.mem_prod

Membership Condition for Product Submodule: $x \in p \times q \leftrightarrow x_1 \in p \land x_2 \in q$

Informal description

For any submodules $p$ of $M$ and $q$ of $M'$, and any vector $x = (x_1, x_2) \in M \times M'$, we have $x \in p \times q$ if and only if $x_1 \in p$ and $x_2 \in q$.

Submodule.span_prod_le theorem

(s : Set M) (t : Set M') : span R (s ×ˢ t) ≤ prod (span R s) (span R t)

Full source

theorem span_prod_le (s : Set M) (t : Set M') : span R (s ×ˢ t) ≤ prod (span R s) (span R t) :=
  span_le.2 <| Set.prod_mono subset_span subset_span

Span of Product Set is Contained in Product of Spans

Informal description

For any subsets $s$ of an $R$-module $M$ and $t$ of an $R$-module $M'$, the span of the Cartesian product $s \times t$ is contained in the product of the spans of $s$ and $t$, i.e., $$\operatorname{span}_R (s \times t) \leq \operatorname{span}_R s \times \operatorname{span}_R t.$$

Submodule.prod_top theorem

: (prod ⊤ ⊤ : Submodule R (M × M')) = ⊤

Full source

@[simp]
theorem prod_top : (prod ⊤ ⊤ : Submodule R (M × M')) = ⊤ := by ext; simp

Product of Top Submodules is Top Submodule

Informal description

The product of the top submodules of $M$ and $M'$ is equal to the top submodule of $M \times M'$, i.e., $\text{prod}(\top, \top) = \top$ where $\top$ denotes the maximal submodule of the respective space.

Submodule.prod_bot theorem

: (prod ⊥ ⊥ : Submodule R (M × M')) = ⊥

Full source

@[simp]
theorem prod_bot : (prod ⊥ ⊥ : Submodule R (M × M')) = ⊥ := by ext ⟨x, y⟩; simp

Product of Trivial Submodules is Trivial

Informal description

The product of the trivial submodules $\bot$ of $M$ and $\bot$ of $M'$ is equal to the trivial submodule $\bot$ of the product module $M \times M'$.

Submodule.prod_mono theorem

{p p' : Submodule R M} {q q' : Submodule R M'} : p ≤ p' → q ≤ q' → prod p q ≤ prod p' q'

Full source

theorem prod_mono {p p' : Submodule R M} {q q' : Submodule R M'} :
    p ≤ p' → q ≤ q' → prod p q ≤ prod p' q' :=
  Set.prod_mono

Monotonicity of Submodule Product with Respect to Inclusion

Informal description

For any submodules $p, p'$ of $M$ and $q, q'$ of $M'$, if $p \subseteq p'$ and $q \subseteq q'$, then the product submodule $p \times q$ is contained in $p' \times q'$.

Submodule.prod_inf_prod theorem

: prod p q₁ ⊓ prod p' q₁' = prod (p ⊓ p') (q₁ ⊓ q₁')

Full source

@[simp]
theorem prod_inf_prod : prodprod p q₁ ⊓ prod p' q₁' = prod (p ⊓ p') (q₁ ⊓ q₁') :=
  SetLike.coe_injective Set.prod_inter_prod

Infimum of Product Submodules Equals Product of Infima

Informal description

For submodules $p, p'$ of $M$ and $q_1, q_1'$ of $M'$, the infimum of the product submodules $p \times q_1$ and $p' \times q_1'$ is equal to the product of the infima $(p \cap p') \times (q_1 \cap q_1')$. In symbols: $$ (p \times q_1) \cap (p' \times q_1') = (p \cap p') \times (q_1 \cap q_1'). $$

Submodule.prod_sup_prod theorem

: prod p q₁ ⊔ prod p' q₁' = prod (p ⊔ p') (q₁ ⊔ q₁')

Full source

@[simp]
theorem prod_sup_prod : prodprod p q₁ ⊔ prod p' q₁' = prod (p ⊔ p') (q₁ ⊔ q₁') := by
  refine le_antisymm
    (sup_le (prod_mono le_sup_left le_sup_left) (prod_mono le_sup_right le_sup_right)) ?_
  simp only [SetLike.le_def, mem_prod, and_imp, Prod.forall]; intro xx yy hxx hyy
  rcases mem_sup.1 hxx with ⟨x, hx, x', hx', rfl⟩
  rcases mem_sup.1 hyy with ⟨y, hy, y', hy', rfl⟩
  exact mem_sup.2 ⟨(x, y), ⟨hx, hy⟩, (x', y'), ⟨hx', hy'⟩, rfl⟩

Supremum of Product Submodules Equals Product of Suprema

Informal description

For any submodules $p, p'$ of an $R$-module $M$ and $q_1, q_1'$ of an $R$-module $M'$, the supremum of the product submodules $p \times q_1$ and $p' \times q_1'$ is equal to the product of the suprema $(p \sqcup p') \times (q_1 \sqcup q_1')$. In symbols: $$ (p \times q_1) \sqcup (p' \times q_1') = (p \sqcup p') \times (q_1 \sqcup q_1'). $$

LinearMap.BilinMap.apply_apply_mem_of_mem_span theorem

 {R M N P : Type*} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N]
  [Module R P] (P' : Submodule R P) (s : Set M) (t : Set N) (B : M →ₗ[R] N →ₗ[R] P) (hB : ∀ x ∈ s, ∀ y ∈ t, B x y ∈ P')
  (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t) : B x y ∈ P'

Full source

/-- If a bilinear map takes values in a submodule along two sets, then the same is true along
the span of these sets. -/
lemma _root_.LinearMap.BilinMap.apply_apply_mem_of_mem_span {R M N P : Type*} [CommSemiring R]
    [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P]
    (P' : Submodule R P) (s : Set M) (t : Set N)
    (B : M →ₗ[R] N →ₗ[R] P) (hB : ∀ x ∈ s, ∀ y ∈ t, B x y ∈ P')
    (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t) :
    B x y ∈ P' := by
  induction hx, hy using span_induction₂ with
  | mem_mem u v hu hv => exact hB u hu v hv
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
  | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv

Bilinear Map Preserves Submodule Membership Under Span

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a submodule $P'$ of $P$, subsets $s \subseteq M$ and $t \subseteq N$, and a bilinear map $B \colon M \to N \to P$ such that $B(x, y) \in P'$ for all $x \in s$ and $y \in t$, then for any $x \in \operatorname{span}_R s$ and $y \in \operatorname{span}_R t$, the image $B(x, y)$ lies in $P'$.

Submodule.biSup_comap_subtype_eq_top theorem

{ι : Type*} (s : Set ι) (p : ι → Submodule R M) : ⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype = ⊤

Full source

@[simp]
lemma biSup_comap_subtype_eq_top {ι : Type*} (s : Set ι) (p : ι → Submodule R M) :
    ⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype = ⊤ := by
  refine eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_
  suffices x ∈ (⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype).map (⨆ i ∈ s, (p i)).subtype by
    obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
    exact hy
  suffices ∀ i ∈ s, (comap (⨆ i ∈ s, p i).subtype (p i)).map (⨆ i ∈ s, p i).subtype = p i by
    simpa only [map_iSup, biSup_congr this]
  intro i hi
  rw [map_comap_eq, range_subtype, inf_eq_right]
  exact le_biSup p hi

Supremum of Composed Submodules Equals Top Submodule

Informal description

For any set $s$ of indices and any family of submodules $p_i$ indexed by $s$ in a module $M$ over a ring $R$, the supremum of the submodules obtained by composing each $p_i$ with the inclusion map into the supremum of all $p_i$ is equal to the top submodule. In other words, $\bigsqcup_{i \in s} (p_i \cap (\bigsqcup_{i \in s} p_i)) = \top$.

LinearMap.exists_ne_zero_of_sSup_eq theorem

 {N : Submodule R M} {f : N →ₛₗ[σ₁₂] M₂} (h : f ≠ 0) (s : Set (Submodule R M)) (hs : sSup s = N) :
  ∃ m, ∃ h : m ∈ s, f ∘ₛₗ inclusion ((le_sSup h).trans_eq hs) ≠ 0

Full source

theorem _root_.LinearMap.exists_ne_zero_of_sSup_eq {N : Submodule R M} {f : N →ₛₗ[σ₁₂] M₂}
    (h : f ≠ 0) (s : Set (Submodule R M)) (hs : sSup s = N):
    ∃ m, ∃ h : m ∈ s, f ∘ₛₗ inclusion ((le_sSup h).trans_eq hs) ≠ 0 :=
  have ⟨_, ⟨m, hm, rfl⟩, ne⟩ := LinearMap.exists_ne_zero_of_sSup_eq_top h (comapcomap N.subtype '' s) <|
    by rw [sSup_eq_iSup] at hs; rw [sSup_image, ← hs, biSup_comap_subtype_eq_top]
  ⟨m, hm, fun eq ↦ ne (LinearMap.ext fun x ↦ congr($eq ⟨x, x.2⟩))⟩

Existence of Nonzero Composition for Linear Maps on Submodule Suprema

Informal description

Let $N$ be a submodule of a module $M$ over a ring $R$, and let $f \colon N \to M_2$ be a nonzero linear map. Given a set $s$ of submodules of $M$ such that the supremum of $s$ equals $N$, there exists a submodule $m \in s$ and an element $h \in m$ such that the composition of $f$ with the inclusion map from $m$ to $N$ is nonzero.

Submodule.span_neg theorem

(s : Set M) : span R (-s) = span R s

Full source

@[simp]
theorem span_neg (s : Set M) : span R (-s) = span R s :=
  calc
    span R (-s) = span R ((-LinearMap.id : M →ₗ[R] M) '' s) := by simp
    _ = map (-LinearMap.id) (span R s) := (map_span (-LinearMap.id) _).symm
    _ = span R s := by simp

Span Invariance under Negation

Informal description

For any subset $s$ of an $R$-module $M$, the span of the negation of $s$ is equal to the span of $s$ itself. That is, \[ \operatorname{span}_R (-s) = \operatorname{span}_R s, \] where $-s = \{-x \mid x \in s\}$.

Submodule.instIsModularLattice instance

: IsModularLattice (Submodule R M)

Full source

instance : IsModularLattice (Submodule R M) :=
  ⟨fun y z xz a ha => by
    rw [mem_inf, mem_sup] at ha
    rcases ha with ⟨⟨b, hb, c, hc, rfl⟩, haz⟩
    rw [mem_sup]
    refine ⟨b, hb, c, mem_inf.2 ⟨hc, ?_⟩, rfl⟩
    rw [← add_sub_cancel_right c b, add_comm]
    apply z.sub_mem haz (xz hb)⟩

Modularity of the Lattice of Submodules

Informal description

The lattice of submodules of an $R$-module $M$ is modular. That is, for any submodules $p, q, r$ of $M$ with $p \leq r$, the modular law holds: $(p \sqcup q) \sqcap r = p \sqcup (q \sqcap r)$.

Submodule.isCompl_comap_subtype_of_isCompl_of_le theorem

{p q r : Submodule R M} (h₁ : IsCompl q r) (h₂ : q ≤ p) : IsCompl (q.comap p.subtype) (r.comap p.subtype)

Full source

lemma isCompl_comap_subtype_of_isCompl_of_le {p q r : Submodule R M}
    (h₁ : IsCompl q r) (h₂ : q ≤ p) :
    IsCompl (q.comap p.subtype) (r.comap p.subtype) := by
  simpa [p.mapIic.isCompl_iff, Iic.isCompl_iff] using Iic.isCompl_inf_inf_of_isCompl_of_le h₁ h₂

Complement Preservation under Submodule Inclusion: If $q$ and $r$ are complements with $q \leq p$, then their preimages under $p \hookrightarrow M$ are complements in $p$

Informal description

Let $M$ be a module over a ring $R$, and let $p, q, r$ be submodules of $M$ such that $q$ and $r$ are complements (i.e., $q \sqcap r = \bot$ and $q \sqcup r = \top$) and $q \leq p$. Then the preimages of $q$ and $r$ under the inclusion map $p \hookrightarrow M$ are complements in $p$.

Submodule.comap_map_eq theorem

(f : F) (p : Submodule R M) : comap f (map f p) = p ⊔ LinearMap.ker f

Full source

theorem comap_map_eq (f : F) (p : Submodule R M) : comap f (map f p) = p ⊔ LinearMap.ker f := by
  refine le_antisymm ?_ (sup_le (le_comap_map _ _) (comap_mono bot_le))
  rintro x ⟨y, hy, e⟩
  exact mem_sup.2 ⟨y, hy, x - y, by simpa using sub_eq_zero.2 e.symm, by simp⟩

Preimage of Image Equals Supremum with Kernel

Informal description

Let $R$ be a ring, $M$ and $M_2$ be $R$-modules, and $f : M \to M_2$ be a linear map. For any submodule $p$ of $M$, the preimage of the image of $p$ under $f$ is equal to the supremum of $p$ and the kernel of $f$, i.e., \[ f^{-1}(f(p)) = p \sqcup \ker f. \]

Submodule.comap_map_eq_self theorem

{f : F} {p : Submodule R M} (h : LinearMap.ker f ≤ p) : comap f (map f p) = p

Full source

theorem comap_map_eq_self {f : F} {p : Submodule R M} (h : LinearMap.ker f ≤ p) :
    comap f (map f p) = p := by rw [Submodule.comap_map_eq, sup_of_le_left h]

Preimage of Image Equals Original Submodule When Kernel is Contained

Informal description

Let $R$ be a ring, $M$ and $M_2$ be $R$-modules, and $f : M \to M_2$ be a linear map. For any submodule $p$ of $M$ such that the kernel of $f$ is contained in $p$, the preimage of the image of $p$ under $f$ is equal to $p$ itself, i.e., \[ f^{-1}(f(p)) = p. \]

Submodule.comap_map_sup_of_comap_le theorem

{f : F} {p : Submodule R M} {q : Submodule R₂ M₂} (le : comap f q ≤ p) : comap f (map f p ⊔ q) = p

Full source

theorem comap_map_sup_of_comap_le {f : F} {p : Submodule R M} {q : Submodule R₂ M₂}
    (le : comap f q ≤ p) : comap f (mapmap f p ⊔ q) = p := by
  refine le_antisymm (fun x h ↦ ?_) (map_le_iff_le_comap.mp le_sup_left)
  obtain ⟨_, ⟨y, hy, rfl⟩, z, hz, eq⟩ := mem_sup.mp h
  rw [add_comm, ← eq_sub_iff_add_eq, ← map_sub] at eq; subst eq
  simpa using p.add_mem (le hz) hy

Preimage of Supremum of Mapped Submodule and Another Submodule Under Linear Map

Informal description

Let $f : M \to M₂$ be a linear map between $R$-modules, and let $p$ be a submodule of $M$ and $q$ a submodule of $M₂$. If the preimage of $q$ under $f$ is contained in $p$ (i.e., $\text{comap}_f(q) \leq p$), then the preimage of the supremum of $f(p)$ and $q$ equals $p$: \[ \text{comap}_f(\text{map}_f(p) \sqcup q) = p \]

Submodule.isCoatom_comap_or_eq_top theorem

(f : F) {p : Submodule R₂ M₂} (hp : IsCoatom p) : IsCoatom (comap f p) ∨ comap f p = ⊤

Full source

theorem isCoatom_comap_or_eq_top (f : F) {p : Submodule R₂ M₂} (hp : IsCoatom p) :
    IsCoatomIsCoatom (comap f p) ∨ comap f p = ⊤ :=
  or_iff_not_imp_right.mpr fun h ↦ ⟨h, fun q lt ↦ by
    rw [← comap_map_sup_of_comap_le lt.le, hp.2 (map f q ⊔ p), comap_top]
    simpa only [right_lt_sup, map_le_iff_le_comap] using lt.not_le⟩

Preimage of a Coatom under Linear Map is Coatom or Entire Module

Informal description

Let $f : M \to M_2$ be a linear map between $R$-modules, and let $p$ be a coatom in the submodule lattice of $M_2$. Then the preimage of $p$ under $f$ is either a coatom in the submodule lattice of $M$ or equals the top element $\top$ (i.e., the entire module $M$).

Submodule.isCoatom_comap_iff theorem

{f : F} (hf : Surjective f) {p : Submodule R₂ M₂} : IsCoatom (comap f p) ↔ IsCoatom p

Full source

theorem isCoatom_comap_iff {f : F} (hf : Surjective f) {p : Submodule R₂ M₂} :
    IsCoatomIsCoatom (comap f p) ↔ IsCoatom p := by
  have := comap_injective_of_surjective hf
  rw [IsCoatom, IsCoatom, ← comap_top f, this.ne_iff]
  refine and_congr_right fun _ ↦
    ⟨fun h m hm ↦ this (h _ <| comap_strictMono_of_surjective hf hm), fun h m hm ↦ ?_⟩
  rw [← h _ (lt_map_of_comap_lt_of_surjective hf hm),
    comap_map_eq_self ((comap_mono bot_le).trans hm.le)]

Preimage of Coatom under Surjective Linear Map is Coatom iff Original is Coatom

Informal description

Let $f : M \to M_2$ be a surjective linear map between $R$-modules, and let $p$ be a submodule of $M_2$. Then the preimage of $p$ under $f$ is a coatom in the submodule lattice of $M$ if and only if $p$ itself is a coatom in the submodule lattice of $M_2$.

Submodule.isCoatom_map_of_ker_le theorem

{f : F} (hf : Surjective f) {p : Submodule R M} (le : LinearMap.ker f ≤ p) (hp : IsCoatom p) : IsCoatom (map f p)

Full source

theorem isCoatom_map_of_ker_le {f : F} (hf : Surjective f) {p : Submodule R M}
    (le : LinearMap.ker f ≤ p) (hp : IsCoatom p) : IsCoatom (map f p) :=
  (isCoatom_comap_iff hf).mp <| by rwa [comap_map_eq_self le]

Image of Coatom under Surjective Linear Map with Kernel Condition is Coatom

Informal description

Let $R$ be a ring, $M$ and $M_2$ be $R$-modules, and $f : M \to M_2$ be a surjective linear map. For any submodule $p$ of $M$ such that the kernel of $f$ is contained in $p$ and $p$ is a coatom in the submodule lattice of $M$, the image of $p$ under $f$ is a coatom in the submodule lattice of $M_2$.

Submodule.map_iInf_of_ker_le theorem

 {f : F} (hf : Surjective f) {ι} {p : ι → Submodule R M} (h : LinearMap.ker f ≤ ⨅ i, p i) :
  map f (⨅ i, p i) = ⨅ i, map f (p i)

Full source

theorem map_iInf_of_ker_le {f : F} (hf : Surjective f) {ι} {p : ι → Submodule R M}
    (h : LinearMap.ker f ≤ ⨅ i, p i) : map f (⨅ i, p i) = ⨅ i, map f (p i) := by
  conv_rhs => rw [← map_comap_eq_of_surjective hf (⨅ _, _), comap_iInf]
  simp_rw [fun i ↦ comap_map_eq_self (le_iInf_iff.mp h i)]

Image of Infimum of Submodules under Surjective Linear Map

Informal description

Let $R$ be a ring, $M$ and $M_2$ be $R$-modules, and $f : M \to M_2$ be a surjective linear map. For any family of submodules $(p_i)_{i \in \iota}$ of $M$ such that the kernel of $f$ is contained in their infimum $\bigsqcap_i p_i$, the image of the infimum under $f$ equals the infimum of the images: \[ f\left(\bigsqcap_i p_i\right) = \bigsqcap_i f(p_i). \]

Submodule.comap_covBy_of_surjective theorem

{f : F} (hf : Surjective f) {p q : Submodule R₂ M₂} (h : p ⋖ q) : p.comap f ⋖ q.comap f

Full source

lemma comap_covBy_of_surjective {f : F} (hf : Surjective f)
    {p q : Submodule R₂ M₂} (h : p ⋖ q) :
    p.comap f ⋖ q.comap f := by
  refine ⟨lt_of_le_of_ne (comap_mono h.1.le) ((comap_injective_of_surjective hf).ne h.1.ne), ?_⟩
  intro N h₁ h₂
  refine h.2 (lt_map_of_comap_lt_of_surjective hf h₁) ?_
  rwa [← comap_lt_comap_iff_of_surjective hf, comap_map_eq, sup_eq_left.mpr]
  refine (LinearMap.ker_le_comap (f : M →ₛₗ[τ₁₂] M₂)).trans h₁.le

Preimage Preserves Covering Relation under Surjective Linear Maps

Informal description

Let $R$ be a ring, $M$ and $M_2$ be $R$-modules, and $f : M \to M_2$ be a surjective linear map. For any submodules $p, q$ of $M_2$ such that $p$ is covered by $q$ (i.e., $p \subsetneq q$ and there is no submodule strictly between them), the preimages $f^{-1}(p)$ and $f^{-1}(q)$ satisfy the same covering relation in $M$.

LinearMap.range_domRestrict_eq_range_iff theorem

 {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
  LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ (LinearMap.ker f) = ⊤

Full source

lemma _root_.LinearMap.range_domRestrict_eq_range_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
    LinearMap.rangeLinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ (LinearMap.ker f) = ⊤ := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [eq_top_iff]
    intro x _
    have : f x ∈ LinearMap.range f := LinearMap.mem_range_self f x
    rw [← h] at this
    obtain ⟨y, hy⟩ : ∃ y : S, f.domRestrict S y = f x := this
    have : (y : M) + (x - y) ∈ S ⊔ (LinearMap.ker f) := Submodule.add_mem_sup y.2 (by simp [← hy])
    simpa using this
  · refine le_antisymm (LinearMap.range_domRestrict_le_range f S) ?_
    rintro x ⟨y, rfl⟩
    obtain ⟨s, hs, t, ht, rfl⟩ : ∃ s, s ∈ S ∧ ∃ t, t ∈ LinearMap.ker f ∧ s + t = y :=
      Submodule.mem_sup.1 (by simp [h])
    exact ⟨⟨s, hs⟩, by simp [LinearMap.mem_ker.1 ht]⟩

Range Equality for Restricted Linear Map via Kernel and Submodule Supremum

Informal description

Let $f: M \to M₂$ be a linear map between $R$-modules, and let $S$ be a submodule of $M$. The range of the restriction of $f$ to $S$ equals the range of $f$ if and only if the supremum of $S$ and the kernel of $f$ is the entire module $M$, i.e., $S \sqcup \ker f = \top$.

LinearMap.surjective_domRestrict_iff theorem

 {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} (hf : Surjective f) : Surjective (f.domRestrict S) ↔ S ⊔ LinearMap.ker f = ⊤

Full source

@[simp] lemma _root_.LinearMap.surjective_domRestrict_iff
    {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} (hf : Surjective f) :
    SurjectiveSurjective (f.domRestrict S) ↔ S ⊔ LinearMap.ker f = ⊤ := by
  rw [← LinearMap.range_eq_top] at hf ⊢
  rw [← hf]
  exact LinearMap.range_domRestrict_eq_range_iff

Surjectivity of Restricted Linear Map via Kernel and Submodule Supremum

Informal description

Let $f: M \to M_2$ be a surjective linear map between $R$-modules, and let $S$ be a submodule of $M$. The restriction of $f$ to $S$ is surjective if and only if the supremum of $S$ and the kernel of $f$ is the entire module $M$, i.e., $S \sqcup \ker f = \top$.

Submodule.biSup_comap_eq_top_of_surjective theorem

 {ι : Type*} (s : Set ι) (hs : s.Nonempty) (p : ι → Submodule R₂ M₂) (hp : ⨆ i ∈ s, p i = ⊤) (f : M →ₛₗ[τ₁₂] M₂)
  (hf : Surjective f) : ⨆ i ∈ s, (p i).comap f = ⊤

Full source

lemma biSup_comap_eq_top_of_surjective {ι : Type*} (s : Set ι) (hs : s.Nonempty)
    (p : ι → Submodule R₂ M₂) (hp : ⨆ i ∈ s, p i = ⊤)
    (f : M →ₛₗ[τ₁₂] M₂) (hf : Surjective f) :
    ⨆ i ∈ s, (p i).comap f = ⊤ := by
  obtain ⟨k, hk⟩ := hs
  suffices (⨆ i ∈ s, (p i).comap f) ⊔ LinearMap.ker f = ⊤ by
    rw [← this, left_eq_sup]; exact le_trans f.ker_le_comap (le_biSup (fun i ↦ (p i).comap f) hk)
  rw [iSup_subtype'] at hp ⊢
  rw [← comap_map_eq, map_iSup_comap_of_sujective hf, hp, comap_top]

Supremum of Preimages Equals Top for Surjective Linear Maps

Informal description

Let $R$ and $R_2$ be rings, $M$ and $M_2$ be modules over $R$ and $R_2$ respectively, and $\tau_{12} : R \to R_2$ be a ring homomorphism. Let $\iota$ be a type, $s$ be a nonempty set of indices in $\iota$, and $p : \iota \to \text{Submodule } R_2 M_2$ be a family of submodules of $M_2$ such that $\bigsqcup_{i \in s} p_i = \top$ (the entire module $M_2$). Given a surjective linear map $f : M \to M_2$ over $\tau_{12}$, the supremum of the preimages of the submodules $p_i$ under $f$ is the entire module $M$, i.e., \[ \bigsqcup_{i \in s} (p_i \circ f)^{-1} = \top. \]

Submodule.biSup_comap_eq_top_of_range_eq_biSup theorem

 {R R₂ : Type*} [Semiring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] [Module R M] [Module R₂ M₂] {ι : Type*}
  (s : Set ι) (hs : s.Nonempty) (p : ι → Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = ⨆ i ∈ s, p i) :
  ⨆ i ∈ s, (p i).comap f = ⊤

Full source

lemma biSup_comap_eq_top_of_range_eq_biSup
    {R R₂ : Type*} [Semiring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂]
    [Module R M] [Module R₂ M₂] {ι : Type*} (s : Set ι) (hs : s.Nonempty)
    (p : ι → Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = ⨆ i ∈ s, p i) :
    ⨆ i ∈ s, (p i).comap f = ⊤ := by
  suffices ⨆ i ∈ s, (p i).comap (LinearMap.range f).subtype = ⊤ by
    rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]; rfl
  exact hf ▸ biSup_comap_subtype_eq_top s p

Supremum of Preimages Equals Top When Range Equals Supremum of Submodules

Informal description

Let $R$ and $R_2$ be semiring and ring respectively, with a ring homomorphism $\tau_{12} : R \to R_2$ that is surjective. Let $M$ be an $R$-module and $M_2$ an $R_2$-module. Given a nonempty set $s$ of indices and a family of submodules $p_i$ of $M_2$ indexed by $s$, if the range of a linear map $f : M \to M_2$ over $\tau_{12}$ equals the supremum $\bigsqcup_{i \in s} p_i$, then the supremum of the preimages of $p_i$ under $f$ is the entire module $M$, i.e., \[ \bigsqcup_{i \in s} (p_i \circ f)^{-1} = \top. \]

Submodule.wcovBy_span_singleton_sup theorem

(x : V) (s : Submodule K V) : WCovBy s ((K ∙ x) ⊔ s)

Full source

/-- There is no vector subspace between `s` and `(K ∙ x) ⊔ s`, `WCovBy` version. -/
theorem wcovBy_span_singleton_sup (x : V) (s : Submodule K V) : WCovBy s ((K ∙ x) ⊔ s) := by
  refine ⟨le_sup_right, fun q hpq hqp ↦ hqp.not_le ?_⟩
  rcases SetLike.exists_of_lt hpq with ⟨y, hyq, hyp⟩
  obtain ⟨c, z, hz, rfl⟩ : ∃ c : K, ∃ z ∈ s, c • x + z = y := by
    simpa [mem_sup, mem_span_singleton] using hqp.le hyq
  rcases eq_or_ne c 0 with rfl | hc
  · simp [hz] at hyp
  · have : x ∈ q := by
      rwa [q.add_mem_iff_left (hpq.le hz), q.smul_mem_iff hc] at hyq
    simp [hpq.le, this]

Weak Covering Property for Span Join in Vector Spaces

Informal description

For any vector $x$ in a vector space $V$ over a field $K$ and any submodule $s$ of $V$, the submodule $s$ is weakly covered by the join of $s$ and the span of $\{x\}$, denoted as $(K \cdot x) \sqcup s$. This means there is no proper submodule strictly between $s$ and $(K \cdot x) \sqcup s$.

Submodule.covBy_span_singleton_sup theorem

{x : V} {s : Submodule K V} (h : x ∉ s) : CovBy s ((K ∙ x) ⊔ s)

Full source

/-- There is no vector subspace between `s` and `(K ∙ x) ⊔ s`, `CovBy` version. -/
theorem covBy_span_singleton_sup {x : V} {s : Submodule K V} (h : x ∉ s) : CovBy s ((K ∙ x) ⊔ s) :=
  ⟨by simpa, (wcovBy_span_singleton_sup _ _).2⟩

Covering Property for Span Join: $s \lessdot (K \cdot x) \sqcup s$ when $x \notin s$

Informal description

For a vector $x$ in a vector space $V$ over a field $K$ and a submodule $s$ of $V$, if $x$ does not belong to $s$, then the submodule $s$ is covered by the join of $s$ and the span of $\{x\}$, denoted as $(K \cdot x) \sqcup s$. This means there is no proper submodule strictly between $s$ and $(K \cdot x) \sqcup s$.

Submodule.disjoint_span_singleton theorem

: Disjoint s (K ∙ x) ↔ x ∈ s → x = 0

Full source

theorem disjoint_span_singleton : DisjointDisjoint s (K ∙ x) ↔ x ∈ s → x = 0 := by
  refine disjoint_def.trans ⟨fun H hx => H x hx <| subset_span <| mem_singleton x, ?_⟩
  intro H y hy hyx
  obtain ⟨c, rfl⟩ := mem_span_singleton.1 hyx
  by_cases hc : c = 0
  · rw [hc, zero_smul]
  · rw [s.smul_mem_iff hc] at hy
    rw [H hy, smul_zero]

Disjointness of Submodule and Span of Singleton: $s \cap (K \cdot x) = \{0\}$ iff $x \in s \implies x = 0$

Informal description

For a submodule $s$ of a vector space $V$ over a field $K$ and a vector $x \in V$, the submodule $s$ is disjoint from the span of $\{x\}$ (denoted $K \cdot x$) if and only if whenever $x$ belongs to $s$, it must be the zero vector. In other words, $s \cap (K \cdot x) = \{0\}$ if and only if $x \in s \implies x = 0$.

Submodule.disjoint_span_singleton' theorem

(x0 : x ≠ 0) : Disjoint s (K ∙ x) ↔ x ∉ s

Full source

theorem disjoint_span_singleton' (x0 : x ≠ 0) : DisjointDisjoint s (K ∙ x) ↔ x ∉ s :=
  disjoint_span_singleton.trans ⟨fun h₁ h₂ => x0 (h₁ h₂), fun h₁ h₂ => (h₁ h₂).elim⟩

Disjointness of Submodule and Span of Nonzero Singleton: $s \cap (K \cdot x) = \{0\}$ iff $x \notin s$

Informal description

For a nonzero vector $x$ in a vector space $V$ over a field $K$ and a submodule $s$ of $V$, the submodule $s$ is disjoint from the span of $\{x\}$ (denoted $K \cdot x$) if and only if $x$ does not belong to $s$. In other words, $s \cap (K \cdot x) = \{0\}$ if and only if $x \notin s$.

Submodule.disjoint_span_singleton_of_not_mem theorem

(hx : x ∉ s) : Disjoint s (K ∙ x)

Full source

lemma disjoint_span_singleton_of_not_mem (hx : x ∉ s) : Disjoint s (K ∙ x) := by
  rw [disjoint_span_singleton]
  intro h
  contradiction

Disjointness of Submodule and Span of Singleton for Non-Members: $s \cap (K \cdot x) = \{0\}$ when $x \notin s$

Informal description

For a submodule $s$ of a vector space $V$ over a field $K$ and a vector $x \in V$, if $x$ does not belong to $s$, then $s$ is disjoint from the span of $\{x\}$ (denoted $K \cdot x$). In other words, $s \cap (K \cdot x) = \{0\}$ when $x \notin s$.

Submodule.isCompl_span_singleton_of_isCoatom_of_not_mem theorem

(hs : IsCoatom s) (hx : x ∉ s) : IsCompl s (K ∙ x)

Full source

lemma isCompl_span_singleton_of_isCoatom_of_not_mem (hs : IsCoatom s) (hx : x ∉ s) :
    IsCompl s (K ∙ x) := by
  refine ⟨disjoint_span_singleton_of_not_mem hx, ?_⟩
  rw [← covBy_top_iff] at hs
  simpa only [codisjoint_iff, sup_comm, not_lt_top_iff] using hs.2 (covBy_span_singleton_sup hx).1

Complementarity of Coatom Submodule and Span of Non-Member Vector: $s$ and $K \cdot x$ are complements when $s$ is a coatom and $x \notin s$

Informal description

Let $V$ be a vector space over a field $K$, and let $s$ be a submodule of $V$ that is a coatom (i.e., $s$ is maximal among proper submodules of $V$). For any vector $x \in V$ such that $x \notin s$, the submodule $s$ and the span of $\{x\}$ (denoted $K \cdot x$) are complements in $V$. That is, $s \sqcap (K \cdot x) = \{0\}$ and $s \sqcup (K \cdot x) = V$.

LinearMap.map_le_map_iff theorem

(f : F) {p p'} : map f p ≤ map f p' ↔ p ≤ p' ⊔ ker f

Full source

protected theorem map_le_map_iff (f : F) {p p'} : mapmap f p ≤ map f p' ↔ p ≤ p' ⊔ ker f := by
  rw [map_le_iff_le_comap, Submodule.comap_map_eq]

Image Containment Criterion for Linear Maps: $f(p) \subseteq f(p') \leftrightarrow p \subseteq p' \sqcup \ker f$

Informal description

Let $R$ be a ring, $M$ and $M_2$ be $R$-modules, and $f : M \to M_2$ be a linear map. For any submodules $p$ and $p'$ of $M$, the image of $p$ under $f$ is contained in the image of $p'$ if and only if $p$ is contained in the supremum of $p'$ and the kernel of $f$, i.e., \[ f(p) \subseteq f(p') \leftrightarrow p \subseteq p' \sqcup \ker f. \]

LinearMap.map_le_map_iff' theorem

{f : F} (hf : ker f = ⊥) {p p'} : map f p ≤ map f p' ↔ p ≤ p'

Full source

theorem map_le_map_iff' {f : F} (hf : ker f = ⊥) {p p'} : mapmap f p ≤ map f p' ↔ p ≤ p' := by
  rw [LinearMap.map_le_map_iff, hf, sup_bot_eq]

Image Containment Criterion for Injective Linear Maps: $f(p) \subseteq f(p') \leftrightarrow p \subseteq p'$

Informal description

Let $R$ be a ring, $M$ and $N$ be $R$-modules, and $f : M \to N$ be an injective linear map (i.e., $\ker f = \{0\}$). For any submodules $p$ and $p'$ of $M$, the image of $p$ under $f$ is contained in the image of $p'$ if and only if $p$ is contained in $p'$, i.e., \[ f(p) \subseteq f(p') \leftrightarrow p \subseteq p'. \]

LinearMap.map_injective theorem

{f : F} (hf : ker f = ⊥) : Injective (map f)

Full source

theorem map_injective {f : F} (hf : ker f = ⊥) : Injective (map f) := fun _ _ h =>
  le_antisymm ((map_le_map_iff' hf).1 (le_of_eq h)) ((map_le_map_iff' hf).1 (ge_of_eq h))

Injectivity of Submodule Image Map for Injective Linear Maps

Informal description

Let $R$ be a ring, $M$ and $N$ be $R$-modules, and $f : M \to N$ be an injective linear map (i.e., $\ker f = \{0\}$). Then the induced map on submodules, sending a submodule $p$ of $M$ to its image $f(p)$ in $N$, is injective.

LinearMap.map_eq_top_iff theorem

{f : F} (hf : range f = ⊤) {p : Submodule R M} : p.map f = ⊤ ↔ p ⊔ LinearMap.ker f = ⊤

Full source

theorem map_eq_top_iff {f : F} (hf : range f = ⊤) {p : Submodule R M} :
    p.map f = ⊤ ↔ p ⊔ LinearMap.ker f = ⊤ := by
  simp_rw [← top_le_iff, ← hf, range_eq_map, LinearMap.map_le_map_iff]

Image of Submodule is Entire Module iff Submodule and Kernel Span Domain

Informal description

Let $f : M \to N$ be a linear map between $R$-modules with $\text{range}(f) = N$, and let $p$ be a submodule of $M$. Then the image of $p$ under $f$ equals the entire module $N$ if and only if $p$ combined with the kernel of $f$ equals $M$, i.e., \[ f(p) = N \leftrightarrow p + \ker f = M. \]

LinearMap.toSpanSingleton definition

(x : M) : R →ₗ[R] M

Full source

/-- Given an element `x` of a module `M` over `R`, the natural map from
    `R` to scalar multiples of `x`. See also `LinearMap.ringLmapEquivSelf`. -/
@[simps!]
def toSpanSingleton (x : M) : R →ₗ[R] M :=
  LinearMap.id.smulRight x

Linear map to span of a singleton

Informal description

For an element $x$ in a module $M$ over a ring $R$, the linear map $\text{toSpanSingleton}_R^M x$ from $R$ to $M$ sends each scalar $r \in R$ to its scalar multiple $r \cdot x$ in $M$. This map can be equivalently described as the composition of the identity linear map on $R$ with scalar multiplication by $x$.

LinearMap.span_singleton_eq_range theorem

(x : M) : (R ∙ x) = range (toSpanSingleton R M x)

Full source

/-- The range of `toSpanSingleton x` is the span of `x`. -/
theorem span_singleton_eq_range (x : M) : (R ∙ x) = range (toSpanSingleton R M x) :=
  Submodule.ext fun y => by
    refine Iff.trans ?_ LinearMap.mem_range.symm
    exact mem_span_singleton

Span of Singleton Equals Range of Scalar Multiplication Map

Informal description

For any element $x$ in a module $M$ over a ring $R$, the span of the singleton set $\{x\}$ (denoted $R \cdot x$) is equal to the range of the linear map $\text{toSpanSingleton}_R^M x : R \to M$ defined by $r \mapsto r \cdot x$. In other words, \[ R \cdot x = \{ r \cdot x \mid r \in R \}. \]

LinearMap.toSpanSingleton_one theorem

(x : M) : toSpanSingleton R M x 1 = x

Full source

theorem toSpanSingleton_one (x : M) : toSpanSingleton R M x 1 = x :=
  one_smul _ _

Evaluation of $\text{toSpanSingleton}_R^M$ at 1 yields $x$

Informal description

For any element $x$ in a module $M$ over a ring $R$, the linear map $\text{toSpanSingleton}_R^M x$ evaluated at the multiplicative identity $1 \in R$ equals $x$, i.e., $\text{toSpanSingleton}_R^M x (1) = x$.

LinearMap.toSpanSingleton_injective theorem

: Function.Injective (toSpanSingleton R M)

Full source

theorem toSpanSingleton_injective : Function.Injective (toSpanSingleton R M) :=
  fun _ _ eq ↦ by simpa using congr($eq 1)

Injectivity of the Linear Map to Span of a Singleton

Informal description

The linear map $\text{toSpanSingleton}_R^M : M \to (R \toₗ[R] M)$, which sends a vector $x \in M$ to the linear map $r \mapsto r \cdot x$, is injective. In other words, if $\text{toSpanSingleton}_R^M x = \text{toSpanSingleton}_R^M y$, then $x = y$.

LinearMap.toSpanSingleton_zero theorem

: toSpanSingleton R M 0 = 0

Full source

@[simp]
theorem toSpanSingleton_zero : toSpanSingleton R M 0 = 0 := by
  ext
  simp

Zero Vector Maps to Zero Linear Map under $\text{toSpanSingleton}_R^M$

Informal description

The linear map $\text{toSpanSingleton}_R^M$ evaluated at the zero vector $0 \in M$ is equal to the zero linear map $0 : R \to M$.

LinearMap.toSpanSingleton_eq_zero_iff theorem

{x : M} : toSpanSingleton R M x = 0 ↔ x = 0

Full source

theorem toSpanSingleton_eq_zero_iff {x : M} : toSpanSingletontoSpanSingleton R M x = 0 ↔ x = 0 := by
  rw [← toSpanSingleton_zero, (toSpanSingleton_injective R M).eq_iff]

Zero Linear Map Criterion for $\text{toSpanSingleton}_R^M$

Informal description

For any vector $x$ in an $R$-module $M$, the linear map $\text{toSpanSingleton}_R^M x$ is equal to the zero linear map if and only if $x$ is the zero vector, i.e., $\text{toSpanSingleton}_R^M x = 0 \leftrightarrow x = 0$.

LinearMap.toSpanSingleton_isIdempotentElem_iff theorem

{e : R} : IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e

Full source

theorem toSpanSingleton_isIdempotentElem_iff {e : R} :
    IsIdempotentElemIsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e := by
  simp_rw [IsIdempotentElem, LinearMap.ext_iff, Module.End.mul_apply, toSpanSingleton_apply,
    smul_eq_mul, mul_assoc]
  exact ⟨fun h ↦ by conv_rhs => rw [← one_mul e, ← h, one_mul], fun h _ ↦ by rw [h]⟩

Idempotence Criterion for Linear Maps to Span of Singletons

Informal description

For any element $e$ in a ring $R$, the linear map $\text{toSpanSingleton}_R^R e$ is idempotent if and only if $e$ itself is idempotent, i.e., $\text{toSpanSingleton}_R^R e \circ \text{toSpanSingleton}_R^R e = \text{toSpanSingleton}_R^R e$ if and only if $e \cdot e = e$.

LinearMap.isIdempotentElem_apply_one_iff theorem

{f : Module.End R R} : IsIdempotentElem (f 1) ↔ IsIdempotentElem f

Full source

theorem isIdempotentElem_apply_one_iff {f : Module.End R R} :
    IsIdempotentElemIsIdempotentElem (f 1) ↔ IsIdempotentElem f := by
  rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, IsIdempotentElem,
    LinearMap.ext_iff]
  simp_rw [Module.End.mul_apply]
  exact ⟨fun h r ↦ by rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h], (· 1)⟩

Idempotence Criterion for Endomorphisms via Evaluation at One

Informal description

For any endomorphism $f$ of the $R$-module $R$, the element $f(1)$ is idempotent (i.e., $f(1) \cdot f(1) = f(1)$) if and only if $f$ is idempotent (i.e., $f \circ f = f$).

LinearMap.eqOn_span_iff theorem

{s : Set M} {f g : F} : Set.EqOn f g (span R s) ↔ Set.EqOn f g s

Full source

/-- Two linear maps are equal on `Submodule.span s` iff they are equal on `s`. -/
theorem eqOn_span_iff {s : Set M} {f g : F} : Set.EqOnSet.EqOn f g (span R s) ↔ Set.EqOn f g s := by
  rw [← le_eqLocus, span_le]; rfl

Equality of Linear Maps on Span $\leftrightarrow$ Equality on Generating Set

Informal description

Let $M$ be a module over a ring $R$, and let $s$ be a subset of $M$. For any two linear maps $f, g$ from $M$ to another module, the following are equivalent: 1. $f$ and $g$ agree on the span of $s$ (i.e., $f(x) = g(x)$ for all $x \in \operatorname{span}_R s$). 2. $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$).

LinearMap.eqOn_span' theorem

{s : Set M} {f g : F} (H : Set.EqOn f g s) : Set.EqOn f g (span R s : Set M)

Full source

/-- If two linear maps are equal on a set `s`, then they are equal on `Submodule.span s`.

This version uses `Set.EqOn`, and the hidden argument will expand to `h : x ∈ (span R s : Set M)`.
See `LinearMap.eqOn_span` for a version that takes `h : x ∈ span R s` as an argument. -/
theorem eqOn_span' {s : Set M} {f g : F} (H : Set.EqOn f g s) :
    Set.EqOn f g (span R s : Set M) :=
  eqOn_span_iff.2 H

Extension of Linear Map Equality from Generating Set to Span

Informal description

Let $M$ be a module over a ring $R$, and let $s$ be a subset of $M$. For any two linear maps $f, g$ from $M$ to another module, if $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then they also agree on the span of $s$ (i.e., $f(x) = g(x)$ for all $x \in \operatorname{span}_R s$).

LinearMap.eqOn_span theorem

{s : Set M} {f g : F} (H : Set.EqOn f g s) ⦃x⦄ (h : x ∈ span R s) : f x = g x

Full source

/-- If two linear maps are equal on a set `s`, then they are equal on `Submodule.span s`.

See also `LinearMap.eqOn_span'` for a version using `Set.EqOn`. -/
theorem eqOn_span {s : Set M} {f g : F} (H : Set.EqOn f g s) ⦃x⦄ (h : x ∈ span R s) :
    f x = g x :=
  eqOn_span' H h

Equality of Linear Maps on Span Elements Given Equality on Generating Set

Informal description

Let $M$ be a module over a ring $R$, and let $s$ be a subset of $M$. For any two linear maps $f, g : M \to N$, if $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then they also agree on every element $x$ in the span of $s$ (i.e., $f(x) = g(x)$ for all $x \in \operatorname{span}_R s$).

LinearMap.ext_on theorem

{s : Set M} {f g : F} (hv : span R s = ⊤) (h : Set.EqOn f g s) : f = g

Full source

/-- If `s` generates the whole module and linear maps `f`, `g` are equal on `s`, then they are
equal. -/
theorem ext_on {s : Set M} {f g : F} (hv : span R s = ⊤) (h : Set.EqOn f g s) : f = g :=
  DFunLike.ext _ _ fun _ => eqOn_span h (eq_top_iff'.1 hv _)

Uniqueness of Linear Maps on a Generating Set

Informal description

Let $M$ be a module over a ring $R$, and let $s$ be a subset of $M$ such that $\operatorname{span}_R s = M$ (i.e., $s$ generates $M$ as an $R$-module). For any two linear maps $f, g : M \to N$, if $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then $f = g$.

LinearMap.ext_on_range theorem

{ι : Sort*} {v : ι → M} {f g : F} (hv : span R (Set.range v) = ⊤) (h : ∀ i, f (v i) = g (v i)) : f = g

Full source

/-- If the range of `v : ι → M` generates the whole module and linear maps `f`, `g` are equal at
each `v i`, then they are equal. -/
theorem ext_on_range {ι : Sort*} {v : ι → M} {f g : F} (hv : span R (Set.range v) = ⊤)
    (h : ∀ i, f (v i) = g (v i)) : f = g :=
  ext_on hv (Set.forall_mem_range.2 h)

Uniqueness of Linear Maps on a Spanning Family of Vectors

Informal description

Let $M$ be a module over a ring $R$, and let $v : \iota \to M$ be a family of vectors in $M$ whose span is the entire module (i.e., $\operatorname{span}_R (\text{range } v) = M$). For any two linear maps $f, g : M \to N$, if $f(v_i) = g(v_i)$ for all $i \in \iota$, then $f = g$.

LinearMap.ker_toSpanSingleton theorem

{x : M} (h : x ≠ 0) : LinearMap.ker (toSpanSingleton R M x) = ⊥

Full source

theorem ker_toSpanSingleton {x : M} (h : x ≠ 0) : LinearMap.ker (toSpanSingleton R M x) = ⊥ :=
  SetLike.ext fun _ => smul_eq_zero.trans <| or_iff_left_of_imp fun h' => (h h').elim

Kernel of Linear Map to Span of Nonzero Singleton is Trivial

Informal description

Let $M$ be a module over a ring $R$, and let $x \in M$ be a nonzero element. The kernel of the linear map $\text{toSpanSingleton}_R^M x : R \to M$ (defined by $r \mapsto r \cdot x$) is the trivial submodule $\{0\}$.

LinearMap.span_singleton_sup_ker_eq_top theorem

(f : V →ₗ[K] K) {x : V} (hx : f x ≠ 0) : (K ∙ x) ⊔ ker f = ⊤

Full source

theorem span_singleton_sup_ker_eq_top (f : V →ₗ[K] K) {x : V} (hx : f x ≠ 0) :
    (K ∙ x) ⊔ ker f = ⊤ :=
  top_unique fun y _ =>
    Submodule.mem_sup.2
      ⟨(f y * (f x)⁻¹) • x, Submodule.mem_span_singleton.2 ⟨f y * (f x)⁻¹, rfl⟩,
        ⟨y - (f y * (f x)⁻¹) • x, by simp [hx]⟩⟩

Span of Nonzero Vector and Kernel of Linear Functional Cover the Whole Space

Informal description

Let $V$ be a vector space over a field $K$, and let $f : V \to K$ be a linear map. For any nonzero vector $x \in V$ such that $f(x) \neq 0$, the supremum of the span of $\{x\}$ and the kernel of $f$ is the entire space $V$, i.e., $(K \cdot x) \sqcup \ker f = V$.

LinearEquiv.toSpanNonzeroSingleton definition

: R ≃ₗ[R] R ∙ x

Full source

/-- Given a nonzero element `x` of a torsion-free module `M` over a ring `R`, the natural
isomorphism from `R` to the span of `x` given by $r \mapsto r \cdot x$. -/
noncomputable
def toSpanNonzeroSingleton : R ≃ₗ[R] R ∙ x :=
  LinearEquiv.trans
    (LinearEquiv.ofInjective (LinearMap.toSpanSingleton R M x)
      (ker_eq_bot.1 <| ker_toSpanSingleton R M h))
    (LinearEquiv.ofEq (range <| toSpanSingleton R M x) (R ∙ x) (span_singleton_eq_range R M x).symm)

Natural isomorphism from $R$ to the span of a nonzero element

Informal description

Given a nonzero element $x$ of a module $M$ over a ring $R$, the linear equivalence $\text{toSpanNonzeroSingleton}_R^M x$ from $R$ to the span of $x$ maps each scalar $r \in R$ to $r \cdot x \in R \cdot x$. This isomorphism is natural in the sense that it preserves the module structure.

LinearEquiv.toSpanNonzeroSingleton_apply theorem

 (t : R) :
  toSpanNonzeroSingleton R M x h t = (⟨t • x, Submodule.smul_mem _ _ (Submodule.mem_span_singleton_self x)⟩ : R ∙ x)

Full source

@[simp] theorem toSpanNonzeroSingleton_apply (t : R) :
    toSpanNonzeroSingleton R M x h t =
      (⟨t • x, Submodule.smul_mem _ _ (Submodule.mem_span_singleton_self x)⟩ : R ∙ x) := by
  rfl

Action of Span Isomorphism on Scalar $t$: $\text{toSpanNonzeroSingleton}_R^M x(t) = t \cdot x$

Informal description

For any scalar $t \in R$ and nonzero element $x$ in an $R$-module $M$, the linear equivalence $\text{toSpanNonzeroSingleton}_R^M x$ maps $t$ to the element $\langle t \cdot x, \text{Submodule.smul\_mem} \_ \_ (\text{Submodule.mem\_span\_singleton\_self} x) \rangle$ in the span $R \cdot x$.

LinearEquiv.toSpanNonzeroSingleton_symm_apply_smul theorem

(m : R ∙ x) : (toSpanNonzeroSingleton R M x h).symm m • x = m

Full source

@[simp]
lemma toSpanNonzeroSingleton_symm_apply_smul (m : R ∙ x) :
    (toSpanNonzeroSingleton R M x h).symm m • x = m :=
  congrArg Subtype.val <| apply_symm_apply (toSpanNonzeroSingleton R M x h) m

Inverse of Span Isomorphism Acts as Scalar Multiplication Identity

Informal description

For any nonzero element $x$ in an $R$-module $M$, and any element $m$ in the span of $x$, the action of the inverse of the linear equivalence $\text{toSpanNonzeroSingleton}_R^M x$ on $m$ followed by scalar multiplication with $x$ yields $m$ itself, i.e., $(\text{toSpanNonzeroSingleton}_R^M x)^{-1}(m) \cdot x = m$.

LinearEquiv.toSpanNonzeroSingleton_one theorem

: LinearEquiv.toSpanNonzeroSingleton R M x h 1 = (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x)

Full source

theorem toSpanNonzeroSingleton_one :
    LinearEquiv.toSpanNonzeroSingleton R M x h 1 =
      (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x) := by simp

Identity maps to generator under span isomorphism: $\text{toSpanNonzeroSingleton}_R^M x(1) = x$

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $x \in M$ a nonzero element. The linear isomorphism $\text{toSpanNonzeroSingleton}_R^M x$ from $R$ to the span $R \cdot x$ maps the multiplicative identity $1 \in R$ to the element $x \in R \cdot x$.

LinearEquiv.coord abbrev

: (R ∙ x) ≃ₗ[R] R

Full source

/-- Given a nonzero element `x` of a torsion-free module `M` over a ring `R`, the natural
isomorphism from the span of `x` to `R` given by $r \cdot x \mapsto r$. -/
noncomputable
abbrev coord : (R ∙ x) ≃ₗ[R] R :=
  (toSpanNonzeroSingleton R M x h).symm

Natural Linear Isomorphism from Span of Nonzero Element to Base Ring

Informal description

Given a nonzero element $x$ of a torsion-free module $M$ over a ring $R$, there exists a natural linear isomorphism $\text{coord}_R^M x$ from the span of $x$ (denoted $R \cdot x$) to $R$, which maps each element $r \cdot x \in R \cdot x$ to the scalar $r \in R$.

LinearEquiv.coord_self theorem

: (coord R M x h) (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x) = 1

Full source

theorem coord_self : (coord R M x h) (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x) = 1 := by
  rw [← toSpanNonzeroSingleton_one R M x h, LinearEquiv.symm_apply_apply]

Coordinate Function Maps Generator to Identity: $\text{coord}_R^M x(x) = 1$

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $x \in M$ a nonzero element. The coordinate function $\text{coord}_R^M x$ maps the element $x$ in the span $R \cdot x$ to the multiplicative identity $1 \in R$, i.e., $\text{coord}_R^M x(x) = 1$.

LinearEquiv.coord_apply_smul theorem

(y : Submodule.span R ({ x } : Set M)) : coord R M x h y • x = y

Full source

theorem coord_apply_smul (y : Submodule.span R ({x} : Set M)) : coord R M x h y • x = y :=
  Subtype.ext_iff.1 <| (toSpanNonzeroSingleton R M x h).apply_symm_apply _

Coordinate Function Recovers Element via Scalar Multiplication

Informal description

For any element $y$ in the span of a nonzero vector $x$ in an $R$-module $M$, the action of the coordinate function $\text{coord}_R^M x$ on $y$ followed by scalar multiplication with $x$ recovers $y$, i.e., $(\text{coord}_R^M x)(y) \cdot x = y$.

Notations