Mathlib.LinearAlgebra.Basis.Submodule

Basis.mem_submodule_iff theorem

 {P : Submodule R M} (b : Basis ι R P) {x : M} : x ∈ P ↔ ∃ c : ι →₀ R, x = Finsupp.sum c fun i x => x • (b i : M)

Full source

/-- If the submodule `P` has a basis, `x ∈ P` iff it is a linear combination of basis vectors. -/
theorem mem_submodule_iff {P : Submodule R M} (b : Basis ι R P) {x : M} :
    x ∈ Px ∈ P ↔ ∃ c : ι →₀ R, x = Finsupp.sum c fun i x => x • (b i : M) := by
  conv_lhs =>
    rw [← P.range_subtype, ← Submodule.map_top, ← b.span_eq, Submodule.map_span, ← Set.range_comp,
        ← Finsupp.range_linearCombination]
  simp [@eq_comm _ x, Function.comp, Finsupp.linearCombination_apply]

Characterization of Submodule Membership via Basis Representation

Informal description

Let $P$ be a submodule of an $R$-module $M$ with a basis $b$ indexed by $\iota$. An element $x \in M$ belongs to $P$ if and only if there exists a finitely supported function $c \colon \iota \to R$ such that $x$ can be expressed as the finite sum $x = \sum_{i} c(i) \cdot b(i)$, where $b(i)$ is the $i$-th basis vector of $P$ considered as an element of $M$.

Basis.mem_submodule_iff' theorem

 [Fintype ι] {P : Submodule R M} (b : Basis ι R P) {x : M} : x ∈ P ↔ ∃ c : ι → R, x = ∑ i, c i • (b i : M)

Full source

/-- If the submodule `P` has a finite basis,
`x ∈ P` iff it is a linear combination of basis vectors. -/
theorem mem_submodule_iff' [Fintype ι] {P : Submodule R M} (b : Basis ι R P) {x : M} :
    x ∈ Px ∈ P ↔ ∃ c : ι → R, x = ∑ i, c i • (b i : M) :=
  b.mem_submodule_iff.trans <|
    Finsupp.equivFunOnFinite.exists_congr_left.trans <|
      exists_congr fun c => by simp [Finsupp.sum_fintype, Finsupp.equivFunOnFinite]

Characterization of Submodule Membership via Finite Basis Representation

Informal description

Let $P$ be a submodule of an $R$-module $M$ with a finite basis $b$ indexed by a finite type $\iota$. An element $x \in M$ belongs to $P$ if and only if there exists a function $c \colon \iota \to R$ such that $x$ can be expressed as the finite sum $x = \sum_{i \in \iota} c(i) \cdot b(i)$, where $b(i)$ is the $i$-th basis vector of $P$ considered as an element of $M$.

Submodule.inductionOnRankAux definition

 (b : Basis ι R M) (P : Submodule R M → Sort*)
  (ih : ∀ N : Submodule R M, (∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = (0 : M) → c = 0) → P N') → P N)
  (n : ℕ) (N : Submodule R M) (rank_le : ∀ {m : ℕ} (v : Fin m → N), LinearIndependent R ((↑) ∘ v : Fin m → M) → m ≤ n) :
  P N

Full source

/-- If `N` is a submodule with finite rank, do induction on adjoining a linear independent
element to a submodule. -/
def Submodule.inductionOnRankAux (b : Basis ι R M) (P : Submodule R M → Sort*)
    (ih : ∀ N : Submodule R M,
      (∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = (0 : M) → c = 0) → P N') → P N)
    (n : ℕ) (N : Submodule R M)
    (rank_le : ∀ {m : ℕ} (v : Fin m → N), LinearIndependent R ((↑) ∘ v : Fin m → M) → m ≤ n) :
    P N := by
  haveI : DecidableEq M := Classical.decEq M
  have Pbot : P ⊥ := by
    apply ih
    intro N _ x x_mem x_ortho
    exfalso
    rw [mem_bot] at x_mem
    simpa [x_mem] using x_ortho 1 0 N.zero_mem
  induction n generalizing N with
  | zero =>
    suffices N = ⊥ by rwa [this]
    apply Basis.eq_bot_of_rank_eq_zero b _ fun m hv => Nat.le_zero.mp (rank_le _ hv)
  | succ n rank_ih =>
    apply ih
    intro N' N'_le x x_mem x_ortho
    apply rank_ih
    intro m v hli
    refine Nat.succ_le_succ_iff.mp (rank_le (Fin.cons ⟨x, x_mem⟩ fun i => ⟨v i, N'_le (v i).2⟩) ?_)
    convert hli.fin_cons' x _ ?_
    · ext i
      refine Fin.cases ?_ ?_ i <;> simp
    · intro c y hcy
      refine x_ortho c y (Submodule.span_le.mpr ?_ y.2) hcy
      rintro _ ⟨z, rfl⟩
      exact (v z).2

Induction on submodules by rank

Informal description

Given a basis $b$ of a module $M$ over a ring $R$, a predicate $P$ on submodules of $M$, and a natural number $n$, the function `Submodule.inductionOnRankAux` performs induction on submodules $N$ of $M$ where the rank (dimension) of any linearly independent set in $N$ is bounded by $n$. The induction hypothesis `ih` states that for any submodule $N$, if $P$ holds for all proper submodules $N'$ of $N$ (with the condition that any $x \in N$ is linearly independent from $N'$), then $P$ holds for $N$. This construction is used to perform induction on submodules with finite rank by adjoining linearly independent elements.

Basis.mem_center_iff theorem

 {A} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [SMulCommClass R R A]
  [IsScalarTower R A A] (b : Basis ι R A) {z : A} :
  z ∈ Set.center A ↔
    (∀ i, Commute (b i) z) ∧
      ∀ i j, z * (b i * b j) = (z * b i) * b j ∧ (b i * z) * b j = b i * (z * b j) ∧ (b i * b j) * z = b i * (b j * z)

Full source

/-- An element of a non-unital-non-associative algebra is in the center exactly when it commutes
with the basis elements. -/
lemma Basis.mem_center_iff {A}
    [Semiring R] [NonUnitalNonAssocSemiring A]
    [Module R A] [SMulCommClass R A A] [SMulCommClass R R A] [IsScalarTower R A A]
    (b : Basis ι R A) {z : A} :
    z ∈ Set.center Az ∈ Set.center A ↔
      (∀ i, Commute (b i) z) ∧ ∀ i j,
        z * (b i * b j) = (z * b i) * b j
          ∧ (b i * z) * b j = b i * (z * b j)
          ∧ (b i * b j) * z = b i * (b j * z) := by
  constructor
  · intro h
    constructor
    · intro i
      apply (h.1 (b i)).symm
    · intros
      exact ⟨h.2 _ _, ⟨h.3 _ _, h.4 _ _⟩⟩
  · intro h
    rw [center, mem_setOf_eq]
    constructor
    case comm =>
      intro y
      rw [← b.linearCombination_repr y, linearCombination_apply, sum, Finset.sum_mul,
          Finset.mul_sum]
      simp_rw [mul_smul_comm, smul_mul_assoc, (h.1 _).eq]
    case left_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, sum, Finset.sum_mul, Finset.mul_sum, Finset.mul_sum,
          Finset.mul_sum]
      simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
        Finset.smul_sum, smul_mul_assoc, mul_smul_comm, (h.2 _ _).1,
        (@SMulCommClass.smul_comm R R A)]
      rw [Finset.sum_comm]
    case mid_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, sum, Finset.sum_mul, Finset.mul_sum, Finset.mul_sum,
          Finset.mul_sum]
      simp_rw [smul_mul_assoc, Finset.sum_mul, mul_smul_comm, smul_mul_assoc, (h.2 _ _).2.1]
    case right_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, Finsupp.sum, Finset.sum_mul]
      simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
               Finset.smul_sum, smul_mul_assoc, mul_smul_comm, Finset.sum_mul, smul_mul_assoc,
               (h.2 _ _).2.2]

Characterization of Central Elements via Basis Commutation in Non-Unital Non-Associative Algebras

Informal description

Let $A$ be a non-unital non-associative algebra over a semiring $R$, and let $b$ be a basis of $A$ as an $R$-module. An element $z \in A$ lies in the center of $A$ if and only if the following conditions hold: 1. $z$ commutes with every basis element $b_i$, i.e., $b_i \cdot z = z \cdot b_i$ for all $i$. 2. For every pair of basis elements $b_i$ and $b_j$, the following associativity-like conditions are satisfied: - $z \cdot (b_i \cdot b_j) = (z \cdot b_i) \cdot b_j$, - $(b_i \cdot z) \cdot b_j = b_i \cdot (z \cdot b_j)$, - $(b_i \cdot b_j) \cdot z = b_i \cdot (b_j \cdot z)$.

Basis.restrictScalars definition

: Basis ι R (span R (Set.range b))

Full source

/-- Let `b` be an `S`-basis of `M`. Let `R` be a CommRing such that `Algebra R S` has no zero smul
divisors, then the submodule of `M` spanned by `b` over `R` admits `b` as an `R`-basis. -/
noncomputable def Basis.restrictScalars : Basis ι R (span R (Set.range b)) :=
  Basis.span (b.linearIndependent.restrict_scalars (smul_left_injective R one_ne_zero))

Basis restriction of scalars

Informal description

Given a commutative ring $R$ and an $S$-module $M$ with an $S$-basis $b$, where $S$ is an $R$-algebra with no zero scalar divisors, the submodule of $M$ spanned by $b$ over $R$ admits $b$ as an $R$-basis. More precisely, if $b$ is a basis for $M$ over $S$, then $b$ is also a basis for the $R$-submodule $\text{span}_R (\text{range } b)$ of $M$, where the $R$-module structure is induced by the algebra map $R \to S$.

Basis.restrictScalars_apply theorem

(i : ι) : (b.restrictScalars R i : M) = b i

Full source

@[simp]
theorem Basis.restrictScalars_apply (i : ι) : (b.restrictScalars R i : M) = b i := by
  simp only [Basis.restrictScalars, Basis.span_apply]

Equality of Restricted and Original Basis Vectors

Informal description

For any index $i$ in the index set $\iota$, the $i$-th basis vector of the restricted basis $b.\text{restrictScalars}\,R$ (viewed as an element of $M$) equals the original $i$-th basis vector $b\,i$.

Basis.restrictScalars_repr_apply theorem

(m : span R (Set.range b)) (i : ι) : algebraMap R S ((b.restrictScalars R).repr m i) = b.repr m i

Full source

@[simp]
theorem Basis.restrictScalars_repr_apply (m : span R (Set.range b)) (i : ι) :
    algebraMap R S ((b.restrictScalars R).repr m i) = b.repr m i := by
  suffices
    Finsupp.mapRange.linearMapFinsupp.mapRange.linearMap (Algebra.linearMap R S) ∘ₗ (b.restrictScalars R).repr.toLinearMap =
      ((b.repr : M →ₗ[S] ι →₀ S).restrictScalars R).domRestrict _
    by exact DFunLike.congr_fun (LinearMap.congr_fun this m) i
  refine Basis.ext (b.restrictScalars R) fun _ => ?_
  simp only [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply, map_one,
    Basis.repr_self, Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single,
    Algebra.linearMap_apply, LinearMap.domRestrict_apply, LinearEquiv.coe_coe,
    Basis.restrictScalars_apply, LinearMap.coe_restrictScalars]

Coefficient Preservation under Basis Restriction: $\text{algebraMap}_{R \to S} \circ (b.\text{restrictScalars}\,R).\text{repr} = b.\text{repr}$

Informal description

For any element $m$ in the $R$-submodule spanned by the range of a basis $b$, and for any index $i \in \iota$, the image of the $i$-th coefficient of $m$ under the algebra map $R \to S$ equals the $i$-th coefficient of $m$ in the original basis representation. In mathematical notation: $$\text{algebraMap}_{R \to S} \left( (b.\text{restrictScalars}\,R).\text{repr}\,m\,i \right) = b.\text{repr}\,m\,i.$$

Basis.mem_span_iff_repr_mem theorem

(m : M) : m ∈ span R (Set.range b) ↔ ∀ i, b.repr m i ∈ Set.range (algebraMap R S)

Full source

/-- Let `b` be an `S`-basis of `M`. Then `m : M` lies in the `R`-module spanned by `b` iff all the
coordinates of `m` on the basis `b` are in `R` (see `Basis.mem_span` for the case `R = S`). -/
theorem Basis.mem_span_iff_repr_mem (m : M) :
    m ∈ span R (Set.range b)m ∈ span R (Set.range b) ↔ ∀ i, b.repr m i ∈ Set.range (algebraMap R S) := by
  refine
    ⟨fun hm i => ⟨(b.restrictScalars R).repr ⟨m, hm⟩ i, b.restrictScalars_repr_apply R ⟨m, hm⟩ i⟩,
      fun h => ?_⟩
  rw [← b.linearCombination_repr m, Finsupp.linearCombination_apply S _]
  refine sum_mem fun i _ => ?_
  obtain ⟨_, h⟩ := h i
  simp_rw [← h, algebraMap_smul]
  exact smul_mem _ _ (subset_span (Set.mem_range_self i))

Characterization of Module Elements in Span via Basis Coefficients

Informal description

Let $M$ be an $S$-module with an $S$-basis $b$, and let $R$ be a subring of $S$. For any element $m \in M$, $m$ lies in the $R$-submodule spanned by $b$ if and only if for every index $i$, the coefficient $b.\text{repr}\,m\,i$ of $m$ with respect to the basis $b$ lies in the image of the algebra map $R \to S$. In mathematical notation: $$m \in \text{span}_R (\text{range } b) \leftrightarrow \forall i,\ b.\text{repr}\,m\,i \in \text{range}(\text{algebraMap}_{R \to S}).$$

Basis.addSubgroupOfClosure definition

(h : A = .closure (Set.range b)) : Basis ι ℤ A.toIntSubmodule

Full source

/--
Let `A` be an subgroup of an additive commutative group `M` that is also an `R`-module.
Construct a basis of `A` as a `ℤ`-basis from a `R`-basis of `E` that generates `A`.
-/
noncomputable def Basis.addSubgroupOfClosure (h : A = .closure (Set.range b)) :
    Basis ι ℤ A.toIntSubmodule :=
  (b.restrictScalars ℤ).map <|
    LinearEquiv.ofEq _ _
      (by rw [h, ← Submodule.span_int_eq_addSubgroup_closure, toAddSubgroup_toIntSubmodule])

$\mathbb{Z}$-basis from $R$-basis generating an additive subgroup

Informal description

Given a commutative ring $R$ and an additive subgroup $A$ of an $R$-module $M$ such that $A$ is the additive subgroup closure of the range of an $R$-basis $b$ of $M$, the structure `Basis.addSubgroupOfClosure` constructs a $\mathbb{Z}$-basis for $A$ by restricting the scalars of $b$ to $\mathbb{Z}$ and using the natural identification of $A$ with its $\mathbb{Z}$-submodule structure.

Basis.addSubgroupOfClosure_apply theorem

(h : A = .closure (Set.range b)) (i : ι) : b.addSubgroupOfClosure A h i = b i

Full source

@[simp]
theorem Basis.addSubgroupOfClosure_apply (h : A = .closure (Set.range b)) (i : ι) :
    b.addSubgroupOfClosure A h i = b i := by
  simp [addSubgroupOfClosure]

Equality of $\mathbb{Z}$-basis vectors with original $R$-basis vectors in additive subgroup closure

Informal description

Let $A$ be an additive subgroup of an $R$-module $M$ such that $A$ is the additive subgroup closure of the range of an $R$-basis $b$ of $M$. Then for any index $i$, the $i$-th basis vector of the $\mathbb{Z}$-basis constructed from $b$ for $A$ equals the original $i$-th basis vector $b(i)$.

Basis.addSubgroupOfClosure_repr_apply theorem

(h : A = .closure (Set.range b)) (x : A) (i : ι) : (b.addSubgroupOfClosure A h).repr x i = b.repr x i

Full source

@[simp]
theorem Basis.addSubgroupOfClosure_repr_apply (h : A = .closure (Set.range b)) (x : A) (i : ι) :
    (b.addSubgroupOfClosure A h).repr x i = b.repr x i := by
  suffices Finsupp.mapRange.linearMapFinsupp.mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ
      (b.addSubgroupOfClosure A h).repr.toLinearMap =
        ((b.repr : M →ₗ[R] ι →₀ R).restrictScalars ℤ).domRestrict A.toIntSubmodule by
    exact DFunLike.congr_fun (LinearMap.congr_fun this x) i
  exact (b.addSubgroupOfClosure A h).ext fun _ ↦ by simp

Equality of Coefficients in $\mathbb{Z}$-basis and $R$-basis Representations for Additive Subgroup Closure

Informal description

Let $A$ be an additive subgroup of an $R$-module $M$ such that $A$ is the additive subgroup closure of the range of an $R$-basis $b$ of $M$. For any element $x \in A$ and any index $i$, the $i$-th coefficient of $x$ in the $\mathbb{Z}$-basis representation constructed from $b$ equals the $i$-th coefficient of $x$ in the original $R$-basis representation. In mathematical notation: $$\text{repr}\, (b.\text{addSubgroupOfClosure}\, A\, h)\, x\, i = \text{repr}\, b\, x\, i.$$