Decompositions of additive monoids, groups, and modules into direct sums

Main definitions

• DirectSum.Decomposition ℳ: A typeclass to provide a constructive decomposition from an additive monoid M into a family of additive submonoids ℳ
• DirectSum.decompose ℳ: The canonical equivalence provided by the above typeclass

Main statements

• DirectSum.Decomposition.isInternal: The link to DirectSum.IsInternal.

Implementation details

As we want to talk about different types of decomposition (additive monoids, modules, rings, ...), we choose to avoid heavily bundling DirectSum.decompose, instead making copies for the AddEquiv, LinearEquiv, 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 DirectSum.Decomposition {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ 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 DirectSum.IsInternal which comes with a constructive inverse to the canonical "recomposition" rather than just a proof that the "recomposition" is bijective.

Often it is easier to construct a term of this type via Decomposition.ofAddHom or Decomposition.ofLinearMap.

• decompose' : M → DirectSum ι fun (i : ι) => ↥(ℳ i)
• left_inv : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'
• right_inv : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'

instance DirectSum.instSubsingletonDecomposition {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) : Subsingleton (Decomposition ℳ)

DirectSum.Decomposition instances, while carrying data, are always equal.

@[reducible, inline]

abbrev DirectSum.Decomposition.ofAddHom {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) (decompose : M →+ DirectSum ι fun (i : ι) => ↥(ℳ i)) (h_left_inv : (DirectSum.coeAddMonoidHom ℳ).comp decompose = AddMonoidHom.id M) (h_right_inv : decompose.comp (DirectSum.coeAddMonoidHom ℳ) = AddMonoidHom.id (DirectSum ι fun (i : ι) => ↥(ℳ i))) : Decomposition ℳ

A convenience method to construct a decomposition from an AddMonoidHom, such that the proofs of left and right inverse can be constructed via ext.

Equations

• DirectSum.Decomposition.ofAddHom ℳ decompose h_left_inv h_right_inv = { decompose' := ⇑decompose, left_inv := ⋯, right_inv := ⋯ }

noncomputable def DirectSum.IsInternal.chooseDecomposition {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) (h : IsInternal ℳ) : Decomposition ℳ

Noncomputably conjure a decomposition instance from a DirectSum.IsInternal proof.

Equations

• DirectSum.IsInternal.chooseDecomposition ℳ h = { decompose' := ⇑(Equiv.ofBijective (⇑(DirectSum.coeAddMonoidHom ℳ)) h).symm, left_inv := ⋯, right_inv := ⋯ }

theorem DirectSum.Decomposition.isInternal {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] : IsInternal ℳ

def DirectSum.decompose {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] : M ≃ DirectSum ι fun (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

• DirectSum.decompose ℳ = { toFun := DirectSum.Decomposition.decompose', invFun := ⇑(DirectSum.coeAddMonoidHom ℳ), left_inv := ⋯, right_inv := ⋯ }

def DirectSum.SetLike.IsHomogeneous {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {P : Type u_5} [SetLike P M] (p : P) : Prop

A substructure p ⊆ M is homogeneous if for every m ∈ p, all homogeneous components of m are in p.

Equations

• DirectSum.SetLike.IsHomogeneous ℳ p = ∀ (i : ι) ⦃m : M⦄, m ∈ p → ↑(((DirectSum.decompose ℳ) m) i) ∈ p

theorem DirectSum.Decomposition.inductionOn {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {motive : M → Prop} (zero : motive 0) (homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive ↑m) (add : ∀ (m m' : M), motive m → motive m' → motive (m + m')) (m : M) : motive m

@[simp]

theorem DirectSum.Decomposition.decompose'_eq {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] : decompose' = ⇑(decompose ℳ)

@[simp]

theorem DirectSum.decompose_symm_of {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {i : ι} (x : ↥(ℳ i)) : (decompose ℳ).symm ((of (fun (i : ι) => ↥(ℳ i)) i) x) = ↑x

@[simp]

theorem DirectSum.decompose_coe {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {i : ι} (x : ↥(ℳ i)) : (decompose ℳ) ↑x = (of (fun (i : ι) => ↥(ℳ i)) i) x

theorem DirectSum.decompose_of_mem {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {x : M} {i : ι} (hx : x ∈ ℳ i) : (decompose ℳ) x = (of (fun (i : ι) => ↥(ℳ i)) i) ⟨x, hx⟩

theorem DirectSum.decompose_of_mem_same {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {x : M} {i : ι} (hx : x ∈ ℳ i) : ↑(((decompose ℳ) x) i) = x

theorem DirectSum.decompose_of_mem_ne {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {x : M} {i j : ι} (hx : x ∈ ℳ i) (hij : i ≠ j) : ↑(((decompose ℳ) x) j) = 0

theorem DirectSum.degree_eq_of_mem_mem {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {x : M} {i j : ι} (hxi : x ∈ ℳ i) (hxj : x ∈ ℳ j) (hx : x ≠ 0) : i = j

def DirectSum.decomposeAddEquiv {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] : M ≃+ DirectSum ι fun (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

• DirectSum.decomposeAddEquiv ℳ = (let __src := (DirectSum.decompose ℳ).symm; { toEquiv := __src, map_add' := ⋯ }).symm

@[simp]

theorem DirectSum.decomposeAddEquiv_apply {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] (a✝ : M) : (decomposeAddEquiv ℳ) a✝ = (decompose ℳ) a✝

@[simp]

theorem DirectSum.decomposeAddEquiv_symm_apply {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] (a✝ : DirectSum ι fun (i : ι) => ↥(ℳ i)) : (decomposeAddEquiv ℳ).symm a✝ = (decompose ℳ).symm a✝

@[simp]

theorem DirectSum.decompose_zero {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] : (decompose ℳ) 0 = 0

@[simp]

theorem DirectSum.decompose_symm_zero {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] : (decompose ℳ).symm 0 = 0

@[simp]

theorem DirectSum.decompose_add {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] (x y : M) : (decompose ℳ) (x + y) = (decompose ℳ) x + (decompose ℳ) y

@[simp]

theorem DirectSum.decompose_symm_add {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] (x y : DirectSum ι fun (i : ι) => ↥(ℳ i)) : (decompose ℳ).symm (x + y) = (decompose ℳ).symm x + (decompose ℳ).symm y

@[simp]

theorem DirectSum.decompose_sum {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {ι' : Type u_5} (s : Finset ι') (f : ι' → M) : (decompose ℳ) (∑ i ∈ s, f i) = ∑ i ∈ s, (decompose ℳ) (f i)

@[simp]

theorem DirectSum.decompose_symm_sum {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {ι' : Type u_5} (s : Finset ι') (f : ι' → DirectSum ι fun (i : ι) => ↥(ℳ i)) : (decompose ℳ).symm (∑ i ∈ s, f i) = ∑ i ∈ s, (decompose ℳ).symm (f i)

theorem DirectSum.sum_support_decompose {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] [(i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)] (r : M) : ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) = r

theorem DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [Decomposition ℳ] {P : Type u_5} [SetLike P M] [AddSubmonoidClass P M] (p : P) (hp : SetLike.IsHomogeneous ℳ p) {x : M} : x ∈ p ↔ ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p

instance DirectSum.addCommGroupSetLike {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [AddCommGroup M] [SetLike σ M] [AddSubgroupClass σ M] (ℳ : ι → σ) : AddCommGroup (DirectSum ι fun (i : ι) => ↥(ℳ i))

The - in the statements below doesn't resolve without this line.

This seems to 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

• DirectSum.addCommGroupSetLike ℳ = inferInstance

@[simp]

theorem DirectSum.decompose_neg {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommGroup M] [SetLike σ M] [AddSubgroupClass σ M] (ℳ : ι → σ) [Decomposition ℳ] (x : M) : (decompose ℳ) (-x) = -(decompose ℳ) x

@[simp]

theorem DirectSum.decompose_symm_neg {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommGroup M] [SetLike σ M] [AddSubgroupClass σ M] (ℳ : ι → σ) [Decomposition ℳ] (x : DirectSum ι fun (i : ι) => ↥(ℳ i)) : (decompose ℳ).symm (-x) = -(decompose ℳ).symm x

@[simp]

theorem DirectSum.decompose_sub {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommGroup M] [SetLike σ M] [AddSubgroupClass σ M] (ℳ : ι → σ) [Decomposition ℳ] (x y : M) : (decompose ℳ) (x - y) = (decompose ℳ) x - (decompose ℳ) y

@[simp]

theorem DirectSum.decompose_symm_sub {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommGroup M] [SetLike σ M] [AddSubgroupClass σ M] (ℳ : ι → σ) [Decomposition ℳ] (x y : DirectSum ι fun (i : ι) => ↥(ℳ i)) : (decompose ℳ).symm (x - y) = (decompose ℳ).symm x - (decompose ℳ).symm y

@[reducible, inline]

abbrev DirectSum.Decomposition.ofLinearMap {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) (decompose : M →ₗ[R] DirectSum ι fun (i : ι) => ↥(ℳ i)) (h_left_inv : coeLinearMap ℳ ∘ₗ decompose = LinearMap.id) (h_right_inv : decompose ∘ₗ coeLinearMap ℳ = LinearMap.id) : Decomposition ℳ

A convenience method to construct a decomposition from an LinearMap, such that the proofs of left and right inverse can be constructed via ext.

Equations

• DirectSum.Decomposition.ofLinearMap ℳ decompose h_left_inv h_right_inv = { decompose' := ⇑decompose, left_inv := ⋯, right_inv := ⋯ }

def DirectSum.decomposeLinearEquiv {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [Decomposition ℳ] : M ≃ₗ[R] DirectSum ι fun (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

• One or more equations did not get rendered due to their size.

@[simp]

theorem DirectSum.decomposeLinearEquiv_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [Decomposition ℳ] (m : M) : (decomposeLinearEquiv ℳ) m = (decompose ℳ) m

@[simp]

theorem DirectSum.decomposeLinearEquiv_symm_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [Decomposition ℳ] (m : DirectSum ι fun (i : ι) => ↥(ℳ i)) : (decomposeLinearEquiv ℳ).symm m = (decompose ℳ).symm m

@[simp]

theorem DirectSum.decompose_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [Decomposition ℳ] (r : R) (x : M) : (decompose ℳ) (r • x) = r • (decompose ℳ) x

@[simp]

theorem DirectSum.decomposeLinearEquiv_symm_comp_lof {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [Decomposition ℳ] (i : ι) : ↑(decomposeLinearEquiv ℳ).symm ∘ₗ lof R ι (fun (x : ι) => ↥(ℳ x)) i = (ℳ i).subtype

theorem DirectSum.decompose_lhom_ext {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [Decomposition ℳ] {N : Type u_5} [AddCommMonoid N] [Module R N] ⦃f g : M →ₗ[R] N⦄ (h : ∀ (i : ι), f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype) : f = g

Two linear maps from a module with a decomposition agree if they agree on every piece.

Note this cannot be @[ext] as ℳ cannot be inferred.