Conversion between add_monoid_algebra and homogenous direct_sum #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This module provides conversions between add_monoid_algebra and direct_sum.
The latter is essentially a dependent version of the former.
Note that since direct_sum.has_mul combines indices additively, there is no equivalent to
monoid_algebra.
Main definitions #
add_monoid_algebra.to_direct_sum : add_monoid_algebra M ι → (⨁ i : ι, M)direct_sum.to_add_monoid_algebra : (⨁ i : ι, M) → add_monoid_algebra M ι- Bundled equiv versions of the above:
add_monoid_algebra_equiv_direct_sum : add_monoid_algebra M ι ≃ (⨁ i : ι, M)add_monoid_algebra_add_equiv_direct_sum : add_monoid_algebra M ι ≃+ (⨁ i : ι, M)add_monoid_algebra_ring_equiv_direct_sum R : add_monoid_algebra M ι ≃+* (⨁ i : ι, M)add_monoid_algebra_alg_equiv_direct_sum R : add_monoid_algebra A ι ≃ₐ[R] (⨁ i : ι, A)
Theorems #
The defining feature of these operations is that they map finsupp.single to
direct_sum.of and vice versa:
as well as preserving arithmetic operations.
For the bundled equivalences, we provide lemmas that they reduce to
add_monoid_algebra.to_direct_sum:
add_monoid_algebra_add_equiv_direct_sum_applyadd_monoid_algebra_lequiv_direct_sum_applyadd_monoid_algebra_add_equiv_direct_sum_symm_applyadd_monoid_algebra_lequiv_direct_sum_symm_apply
Implementation notes #
This file largely just copies the API of data/finsupp/to_dfinsupp, and reuses the proofs.
Recall that add_monoid_algebra M ι is defeq to ι →₀ M and ⨁ i : ι, M is defeq to
Π₀ i : ι, M.
Note that there is no add_monoid_algebra equivalent to finsupp.single, so many statements
still involve this definition.
Basic definitions and lemmas #
def
add_monoid_algebra.to_direct_sum
{ι : Type u_1}
{M : Type u_3}
[semiring M]
(f : add_monoid_algebra M ι) :
direct_sum ι (λ (i : ι), M)
Interpret a add_monoid_algebra as a homogenous direct_sum.
Equations
@[simp]
theorem
add_monoid_algebra.to_direct_sum_single
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
(i : ι)
(m : M) :
add_monoid_algebra.to_direct_sum (finsupp.single i m) = ⇑(direct_sum.of (λ (i : ι), M) i) m
def
direct_sum.to_add_monoid_algebra
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)]
(f : direct_sum ι (λ (i : ι), M)) :
Interpret a homogenous direct_sum as a add_monoid_algebra.
Equations
@[simp]
theorem
direct_sum.to_add_monoid_algebra_of
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)]
(i : ι)
(m : M) :
(⇑(direct_sum.of (λ (i : ι), M) i) m).to_add_monoid_algebra = finsupp.single i m
@[simp]
theorem
add_monoid_algebra.to_direct_sum_to_add_monoid_algebra
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)]
(f : add_monoid_algebra M ι) :
@[simp]
theorem
direct_sum.to_add_monoid_algebra_to_direct_sum
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)]
(f : direct_sum ι (λ (i : ι), M)) :
Lemmas about arithmetic operations #
@[simp]
theorem
add_monoid_algebra.to_direct_sum_zero
{ι : Type u_1}
{M : Type u_3}
[semiring M] :
0.to_direct_sum = 0
@[simp]
theorem
add_monoid_algebra.to_direct_sum_add
{ι : Type u_1}
{M : Type u_3}
[semiring M]
(f g : add_monoid_algebra M ι) :
(f + g).to_direct_sum = f.to_direct_sum + g.to_direct_sum
@[simp]
theorem
add_monoid_algebra.to_direct_sum_mul
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[add_monoid ι]
[semiring M]
(f g : add_monoid_algebra M ι) :
(f * g).to_direct_sum = f.to_direct_sum * g.to_direct_sum
@[simp]
theorem
direct_sum.to_add_monoid_algebra_zero
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)] :
@[simp]
theorem
direct_sum.to_add_monoid_algebra_add
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)]
(f g : direct_sum ι (λ (i : ι), M)) :
@[simp]
theorem
direct_sum.to_add_monoid_algebra_mul
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[add_monoid ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)]
(f g : direct_sum ι (λ (i : ι), M)) :
@[simp]
theorem
add_monoid_algebra_equiv_direct_sum_apply
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)] :
@[simp]
theorem
add_monoid_algebra_equiv_direct_sum_symm_apply
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)] :
def
add_monoid_algebra_equiv_direct_sum
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)] :
add_monoid_algebra M ι ≃ direct_sum ι (λ (i : ι), M)
add_monoid_algebra.to_direct_sum and direct_sum.to_add_monoid_algebra together form an
equiv.
Equations
- add_monoid_algebra_equiv_direct_sum = {to_fun := add_monoid_algebra.to_direct_sum _inst_2, inv_fun := direct_sum.to_add_monoid_algebra (λ (m : M), _inst_3 m), left_inv := _, right_inv := _}
@[simp]
theorem
add_monoid_algebra_add_equiv_direct_sum_apply
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)] :
@[simp]
theorem
add_monoid_algebra_add_equiv_direct_sum_symm_apply
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)] :
def
add_monoid_algebra_add_equiv_direct_sum
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)] :
add_monoid_algebra M ι ≃+ direct_sum ι (λ (i : ι), M)
The additive version of add_monoid_algebra.to_add_monoid_algebra. Note that this is
noncomputable because add_monoid_algebra.has_add is noncomputable.
Equations
- add_monoid_algebra_add_equiv_direct_sum = {to_fun := add_monoid_algebra.to_direct_sum _inst_2, inv_fun := direct_sum.to_add_monoid_algebra (λ (m : M), _inst_3 m), left_inv := _, right_inv := _, map_add' := _}
@[simp]
theorem
add_monoid_algebra_ring_equiv_direct_sum_apply
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[add_monoid ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)] :
def
add_monoid_algebra_ring_equiv_direct_sum
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[add_monoid ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)] :
add_monoid_algebra M ι ≃+* direct_sum ι (λ (i : ι), M)
The ring version of add_monoid_algebra.to_add_monoid_algebra. Note that this is
noncomputable because add_monoid_algebra.has_add is noncomputable.
Equations
- add_monoid_algebra_ring_equiv_direct_sum = {to_fun := add_monoid_algebra.to_direct_sum _inst_3, inv_fun := direct_sum.to_add_monoid_algebra (λ (m : M), _inst_4 m), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
@[simp]
theorem
add_monoid_algebra_ring_equiv_direct_sum_symm_apply
{ι : Type u_1}
{M : Type u_3}
[decidable_eq ι]
[add_monoid ι]
[semiring M]
[Π (m : M), decidable (m ≠ 0)] :
@[simp]
theorem
add_monoid_algebra_alg_equiv_direct_sum_apply
{ι : Type u_1}
{R : Type u_2}
{A : Type u_4}
[decidable_eq ι]
[add_monoid ι]
[comm_semiring R]
[semiring A]
[algebra R A]
[Π (m : A), decidable (m ≠ 0)] :
def
add_monoid_algebra_alg_equiv_direct_sum
{ι : Type u_1}
{R : Type u_2}
{A : Type u_4}
[decidable_eq ι]
[add_monoid ι]
[comm_semiring R]
[semiring A]
[algebra R A]
[Π (m : A), decidable (m ≠ 0)] :
add_monoid_algebra A ι ≃ₐ[R] direct_sum ι (λ (i : ι), A)
The algebra version of add_monoid_algebra.to_add_monoid_algebra. Note that this is
noncomputable because add_monoid_algebra.has_add is noncomputable.
Equations
- add_monoid_algebra_alg_equiv_direct_sum = {to_fun := add_monoid_algebra.to_direct_sum _inst_4, inv_fun := direct_sum.to_add_monoid_algebra (λ (m : A), _inst_6 m), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
theorem
add_monoid_algebra_alg_equiv_direct_sum_symm_apply
{ι : Type u_1}
{R : Type u_2}
{A : Type u_4}
[decidable_eq ι]
[add_monoid ι]
[comm_semiring R]
[semiring A]
[algebra R A]
[Π (m : A), decidable (m ≠ 0)] :