doc-next-gen

Mathlib.LinearAlgebra.Basis.Prod

Module docstring

{"# Bases for the product of modules "}

Basis.prod definition
: Basis (ι ⊕ ι') R (M × M')
Full source 
/-- `Basis.prod` maps an `ι`-indexed basis for `M` and an `ι'`-indexed basis for `M'`
to an `ι ⊕ ι'`-index basis for `M × M'`.
For the specific case of `R × R`, see also `Basis.finTwoProd`. -/
protected def prod : Basis (ι ⊕ ι') R (M × M') :=
  ofRepr ((b.repr.prodCongr b'.repr).trans (Finsupp.sumFinsuppLEquivProdFinsupp R).symm)
Basis for the product of modules
Informal description
Given an $\iota$-indexed basis $b$ for a module $M$ and an $\iota'$-indexed basis $b'$ for a module $M'$ over a ring $R$, the function `Basis.prod` constructs an $(\iota \oplus \iota')$-indexed basis for the product module $M \times M'$. This basis is obtained by combining the two bases via the direct sum of their index types and using the product of their representation isomorphisms.
Basis.prod_repr_inl theorem
(x) (i) : (b.prod b').repr x (Sum.inl i) = b.repr x.1 i
Full source 
@[simp]
theorem prod_repr_inl (x) (i) : (b.prod b').repr x (Sum.inl i) = b.repr x.1 i :=
  rfl
Coordinate Representation in Product Basis for First Component
Informal description
Let $M$ and $M'$ be modules over a ring $R$ with bases $b$ and $b'$ indexed by $\iota$ and $\iota'$ respectively. For any element $x = (x_1, x_2) \in M \times M'$ and any index $i \in \iota$, the coordinate of $x$ at the basis vector corresponding to $\text{Sum.inl}(i)$ in the product basis $b.\text{prod} b'$ equals the coordinate of $x_1$ at index $i$ in the basis $b$. In other words, the representation of $x$ in the product basis satisfies $(b.\text{prod} b').\text{repr} x (\text{Sum.inl} i) = b.\text{repr} x_1 i$.
Basis.prod_repr_inr theorem
(x) (i) : (b.prod b').repr x (Sum.inr i) = b'.repr x.2 i
Full source 
@[simp]
theorem prod_repr_inr (x) (i) : (b.prod b').repr x (Sum.inr i) = b'.repr x.2 i :=
  rfl
Coordinate Formula for Second Factor in Product Basis
Informal description
Let $M$ and $M'$ be modules over a ring $R$ with bases $b$ and $b'$ indexed by $\iota$ and $\iota'$ respectively. For any element $x = (x_1, x_2) \in M \times M'$ and any index $i \in \iota'$, the coordinate of $x$ with respect to the basis vector $(b \sqcup b')(\text{Sum.inr } i)$ in the product basis equals the coordinate of $x_2$ with respect to the basis vector $b'(i)$ in $M'$. In symbols: $(b \sqcup b')^\text{repr}(x)(\text{inr } i) = b'^\text{repr}(x_2)(i)$.
Basis.prod_apply_inl_fst theorem
(i) : (b.prod b' (Sum.inl i)).1 = b i
Full source 
theorem prod_apply_inl_fst (i) : (b.prod b' (Sum.inl i)).1 = b i :=
  b.repr.injective <| by
    ext j
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Equiv.toFun_as_coe, Finsupp.fst_sumFinsuppLEquivProdFinsupp]
    apply Finsupp.single_apply_left Sum.inl_injective
First Component of Product Basis for Left Injection Equals Original Basis Vector
Informal description
Let $M$ and $M'$ be modules over a ring $R$ with bases $b$ and $b'$ indexed by $\iota$ and $\iota'$ respectively. For any index $i \in \iota$, the first component of the basis vector $(b \times b')(\text{inl}(i))$ in the product module $M \times M'$ equals the basis vector $b(i)$ in $M$. In symbols: $(b \times b')(\text{inl}(i)).1 = b(i)$.
Basis.prod_apply_inr_fst theorem
(i) : (b.prod b' (Sum.inr i)).1 = 0
Full source 
theorem prod_apply_inr_fst (i) : (b.prod b' (Sum.inr i)).1 = 0 :=
  b.repr.injective <| by
    ext i
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Equiv.toFun_as_coe, Finsupp.fst_sumFinsuppLEquivProdFinsupp,
      LinearEquiv.map_zero, Finsupp.zero_apply]
    apply Finsupp.single_eq_of_ne Sum.inr_ne_inl
Vanishing of first component in product basis for right inclusion
Informal description
Let $b$ be a basis for a module $M$ over a ring $R$ indexed by $\iota$, and $b'$ a basis for a module $M'$ over $R$ indexed by $\iota'$. For any $i \in \iota'$, the first component of the basis vector $(b \times b')(\text{inr}(i))$ in the product module $M \times M'$ is zero.
Basis.prod_apply_inl_snd theorem
(i) : (b.prod b' (Sum.inl i)).2 = 0
Full source 
theorem prod_apply_inl_snd (i) : (b.prod b' (Sum.inl i)).2 = 0 :=
  b'.repr.injective <| by
    ext j
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b'.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Equiv.toFun_as_coe, Finsupp.snd_sumFinsuppLEquivProdFinsupp,
      LinearEquiv.map_zero, Finsupp.zero_apply]
    apply Finsupp.single_eq_of_ne Sum.inl_ne_inr
Vanishing Second Component of Basis Vector in Product Module for Left Injection
Informal description
For any index $i$ in the sum type $\iota \oplus \iota'$, the second component of the basis vector $(b \times b')(\text{inl}(i))$ in the product module $M \times M'$ is zero, i.e., $(b \times b')(\text{inl}(i)).2 = 0$.
Basis.prod_apply_inr_snd theorem
(i) : (b.prod b' (Sum.inr i)).2 = b' i
Full source 
theorem prod_apply_inr_snd (i) : (b.prod b' (Sum.inr i)).2 = b' i :=
  b'.repr.injective <| by
    ext i
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b'.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Equiv.toFun_as_coe, Finsupp.snd_sumFinsuppLEquivProdFinsupp]
    apply Finsupp.single_apply_left Sum.inr_injective
Second Component of Product Basis for Right Inclusion Matches Original Basis
Informal description
Let $b$ be a basis for an $R$-module $M$ indexed by $\iota$, and $b'$ a basis for an $R$-module $M'$ indexed by $\iota'$. For any $i \in \iota'$, the second component of the basis vector $(b \times b')(\text{inr}(i))$ in the product module $M \times M'$ equals $b'(i)$.
Basis.prod_apply theorem
(i) : b.prod b' i = Sum.elim (LinearMap.inl R M M' ∘ b) (LinearMap.inr R M M' ∘ b') i
Full source 
@[simp]
theorem prod_apply (i) :
    b.prod b' i = Sum.elim (LinearMap.inlLinearMap.inl R M M' ∘ b) (LinearMap.inrLinearMap.inr R M M' ∘ b') i := by
  ext <;> cases i <;>
    simp only [prod_apply_inl_fst, Sum.elim_inl, LinearMap.inl_apply, prod_apply_inr_fst,
      Sum.elim_inr, LinearMap.inr_apply, prod_apply_inl_snd, prod_apply_inr_snd, Function.comp]
Explicit Form of Product Basis Vectors via Injection Maps
Informal description
Let $M$ and $M'$ be modules over a ring $R$ with bases $b$ and $b'$ indexed by $\iota$ and $\iota'$ respectively. For any index $i \in \iota \oplus \iota'$, the basis vector $(b \times b')(i)$ in the product module $M \times M'$ is given by: $$(b \times b')(i) = \begin{cases} (\text{inl} \circ b)(i) & \text{if } i \in \iota \\ (\text{inr} \circ b')(i) & \text{if } i \in \iota' \end{cases}$$ where $\text{inl} : M \to M \times M'$ maps $x$ to $(x,0)$ and $\text{inr} : M' \to M \times M'$ maps $y$ to $(0,y)$.