Decompositions of additive monoids, groups, and modules into direct sums #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
direct_sum.decomposition ℳ: A typeclass to provide a constructive decomposition from an additive monoidMinto a family of additive submonoidsℳdirect_sum.decompose ℳ: The canonical equivalence provided by the above typeclass
Main statements #
direct_sum.decomposition.is_internal: The link todirect_sum.is_internal.
Implementation details #
As we want to talk about different types of decomposition (additive monoids, modules, rings, ...),
we choose to avoid heavily bundling direct_sum.decompose, instead making copies for the
add_equiv, linear_equiv, etc. This means we have to repeat statements that follow from these
bundled homs, but means we don't have to repeat statements for different types of decomposition.
@[class]
structure
direct_sum.decomposition
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ) :
Type (max u_1 u_3)
- decompose' : M → direct_sum ι (λ (i : ι), ↥(ℳ i))
- left_inv : function.left_inverse ⇑(direct_sum.coe_add_monoid_hom ℳ) direct_sum.decomposition.decompose'
- right_inv : function.right_inverse ⇑(direct_sum.coe_add_monoid_hom ℳ) direct_sum.decomposition.decompose'
A decomposition is an equivalence between an additive monoid M and a direct sum of additive
submonoids ℳ i of that M, such that the "recomposition" is canonical. This definition also
works for additive groups and modules.
This is a version of direct_sum.is_internal which comes with a constructive inverse to the
canonical "recomposition" rather than just a proof that the "recomposition" is bijective.
Instances of this typeclass
Instances of other typeclasses for direct_sum.decomposition
- direct_sum.decomposition.has_sizeof_inst
- direct_sum.decomposition.subsingleton
@[protected, instance]
def
direct_sum.decomposition.subsingleton
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ) :
direct_sum.decomposition instances, while carrying data, are always equal.
@[protected]
theorem
direct_sum.decomposition.is_internal
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ] :
def
direct_sum.decompose
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ] :
M ≃ direct_sum ι (λ (i : ι), ↥(ℳ i))
If M is graded by ι with degree i component ℳ i, then it is isomorphic as
to a direct sum of components. This is the canonical spelling of the decompose' field.
Equations
- direct_sum.decompose ℳ = {to_fun := direct_sum.decomposition.decompose' _inst_5, inv_fun := ⇑(direct_sum.coe_add_monoid_hom ℳ), left_inv := _, right_inv := _}
@[protected]
theorem
direct_sum.decomposition.induction_on
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
{p : M → Prop}
(h_zero : p 0)
(h_homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), p ↑m)
(h_add : ∀ (m m' : M), p m → p m' → p (m + m'))
(m : M) :
p m
@[simp]
theorem
direct_sum.decomposition.decompose'_eq
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ] :
@[simp]
theorem
direct_sum.decompose_symm_of
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
{i : ι}
(x : ↥(ℳ i)) :
⇑((direct_sum.decompose ℳ).symm) (⇑(direct_sum.of (λ {i : ι}, ↥(ℳ i)) i) x) = ↑x
@[simp]
theorem
direct_sum.decompose_coe
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
{i : ι}
(x : ↥(ℳ i)) :
⇑(direct_sum.decompose ℳ) ↑x = ⇑(direct_sum.of (λ {i : ι}, ↥(ℳ i)) i) x
theorem
direct_sum.decompose_of_mem
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
{x : M}
{i : ι}
(hx : x ∈ ℳ i) :
⇑(direct_sum.decompose ℳ) x = ⇑(direct_sum.of (λ (i : ι), ↥(ℳ i)) i) ⟨x, hx⟩
theorem
direct_sum.decompose_of_mem_same
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
{x : M}
{i : ι}
(hx : x ∈ ℳ i) :
↑(⇑(⇑(direct_sum.decompose ℳ) x) i) = x
theorem
direct_sum.decompose_of_mem_ne
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
{x : M}
{i j : ι}
(hx : x ∈ ℳ i)
(hij : i ≠ j) :
↑(⇑(⇑(direct_sum.decompose ℳ) x) j) = 0
def
direct_sum.decompose_add_equiv
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ] :
M ≃+ direct_sum ι (λ (i : ι), ↥(ℳ i))
If M is graded by ι with degree i component ℳ i, then it is isomorphic as
an additive monoid to a direct sum of components.
Equations
- direct_sum.decompose_add_equiv ℳ = {to_fun := (direct_sum.decompose ℳ).symm.to_fun, inv_fun := (direct_sum.decompose ℳ).symm.inv_fun, left_inv := _, right_inv := _, map_add' := _}.symm
@[simp]
theorem
direct_sum.decompose_add_equiv_apply
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ] :
@[simp]
theorem
direct_sum.decompose_add_equiv_symm_apply
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ] :
⇑((direct_sum.decompose_add_equiv ℳ).symm) = ⇑((direct_sum.decompose ℳ).symm)
@[simp]
theorem
direct_sum.decompose_zero
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ] :
⇑(direct_sum.decompose ℳ) 0 = 0
@[simp]
theorem
direct_sum.decompose_symm_zero
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ] :
⇑((direct_sum.decompose ℳ).symm) 0 = 0
@[simp]
theorem
direct_sum.decompose_add
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
(x y : M) :
⇑(direct_sum.decompose ℳ) (x + y) = ⇑(direct_sum.decompose ℳ) x + ⇑(direct_sum.decompose ℳ) y
@[simp]
theorem
direct_sum.decompose_symm_add
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
(x y : direct_sum ι (λ (i : ι), ↥(ℳ i))) :
⇑((direct_sum.decompose ℳ).symm) (x + y) = ⇑((direct_sum.decompose ℳ).symm) x + ⇑((direct_sum.decompose ℳ).symm) y
@[simp]
theorem
direct_sum.decompose_sum
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
{ι' : Type u_2}
(s : finset ι')
(f : ι' → M) :
⇑(direct_sum.decompose ℳ) (s.sum (λ (i : ι'), f i)) = s.sum (λ (i : ι'), ⇑(direct_sum.decompose ℳ) (f i))
@[simp]
theorem
direct_sum.decompose_symm_sum
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
{ι' : Type u_2}
(s : finset ι')
(f : ι' → direct_sum ι (λ (i : ι), ↥(ℳ i))) :
⇑((direct_sum.decompose ℳ).symm) (s.sum (λ (i : ι'), f i)) = s.sum (λ (i : ι'), ⇑((direct_sum.decompose ℳ).symm) (f i))
theorem
direct_sum.sum_support_decompose
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_monoid M]
[set_like σ M]
[add_submonoid_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
[Π (i : ι) (x : ↥(ℳ i)), decidable (x ≠ 0)]
(r : M) :
(dfinsupp.support (⇑(direct_sum.decompose ℳ) r)).sum (λ (i : ι), ↑(⇑(⇑(direct_sum.decompose ℳ) r) i)) = r
@[protected, instance]
def
direct_sum.add_comm_group_set_like
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[add_comm_group M]
[set_like σ M]
[add_subgroup_class σ M]
(ℳ : ι → σ) :
add_comm_group (direct_sum ι (λ (i : ι), ↥(ℳ i)))
The - in the statements below doesn't resolve without this line.
This seems to a be a problem of synthesized vs inferred typeclasses disagreeing. If we replace
the statement of decompose_neg with @eq (⨁ i, ℳ i) (decompose ℳ (-x)) (-decompose ℳ x)
instead of decompose ℳ (-x) = -decompose ℳ x, which forces the typeclasses needed by ⨁ i, ℳ i to
be found by unification rather than synthesis, then everything works fine without this instance.
Equations
- direct_sum.add_comm_group_set_like ℳ = direct_sum.add_comm_group (λ (i : ι), ↥(ℳ i))
@[simp]
theorem
direct_sum.decompose_neg
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_group M]
[set_like σ M]
[add_subgroup_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
(x : M) :
⇑(direct_sum.decompose ℳ) (-x) = -⇑(direct_sum.decompose ℳ) x
@[simp]
theorem
direct_sum.decompose_symm_neg
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_group M]
[set_like σ M]
[add_subgroup_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
(x : direct_sum ι (λ (i : ι), ↥(ℳ i))) :
⇑((direct_sum.decompose ℳ).symm) (-x) = -⇑((direct_sum.decompose ℳ).symm) x
@[simp]
theorem
direct_sum.decompose_sub
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_group M]
[set_like σ M]
[add_subgroup_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
(x y : M) :
⇑(direct_sum.decompose ℳ) (x - y) = ⇑(direct_sum.decompose ℳ) x - ⇑(direct_sum.decompose ℳ) y
@[simp]
theorem
direct_sum.decompose_symm_sub
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[decidable_eq ι]
[add_comm_group M]
[set_like σ M]
[add_subgroup_class σ M]
(ℳ : ι → σ)
[direct_sum.decomposition ℳ]
(x y : direct_sum ι (λ (i : ι), ↥(ℳ i))) :
⇑((direct_sum.decompose ℳ).symm) (x - y) = ⇑((direct_sum.decompose ℳ).symm) x - ⇑((direct_sum.decompose ℳ).symm) y
@[simp]
theorem
direct_sum.decompose_linear_equiv_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[decidable_eq ι]
[semiring R]
[add_comm_monoid M]
[module R M]
(ℳ : ι → submodule R M)
[direct_sum.decomposition ℳ] :
⇑(direct_sum.decompose_linear_equiv ℳ) = ⇑({to_fun := ⇑((direct_sum.decompose ℳ).symm), map_add' := _, map_smul' := _, inv_fun := ⇑(direct_sum.decompose ℳ), left_inv := _, right_inv := _}.to_linear_map.inverse ⇑(direct_sum.decompose ℳ) _ _)
def
direct_sum.decompose_linear_equiv
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[decidable_eq ι]
[semiring R]
[add_comm_monoid M]
[module R M]
(ℳ : ι → submodule R M)
[direct_sum.decomposition ℳ] :
M ≃ₗ[R] direct_sum ι (λ (i : ι), ↥(ℳ i))
If M is graded by ι with degree i component ℳ i, then it is isomorphic as
a module to a direct sum of components.
@[simp]
theorem
direct_sum.decompose_linear_equiv_symm_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[decidable_eq ι]
[semiring R]
[add_comm_monoid M]
[module R M]
(ℳ : ι → submodule R M)
[direct_sum.decomposition ℳ] :
⇑((direct_sum.decompose_linear_equiv ℳ).symm) = ⇑((direct_sum.decompose ℳ).symm)
@[simp]
theorem
direct_sum.decompose_smul
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[decidable_eq ι]
[semiring R]
[add_comm_monoid M]
[module R M]
(ℳ : ι → submodule R M)
[direct_sum.decomposition ℳ]
(r : R)
(x : M) :
⇑(direct_sum.decompose ℳ) (r • x) = r • ⇑(direct_sum.decompose ℳ) x