mathlib3 documentation

algebra.direct_sum.decomposition

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 #

Main statements #

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)

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
@[protected, instance]

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
@[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.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) :
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) :
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
@[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 ℳ] :
@[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 ℳ] :
@[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) :
@[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))) :
@[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) :
@[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
@[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) :
@[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))) :
@[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) :
@[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))) :
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.

Equations
@[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) :