Decompositions of additive monoids, groups, and modules into direct sums #
Main definitions #
DirectSum.Decomposition ℳ: A typeclass to provide a constructive decomposition from an additive monoidMinto a family of additive submonoidsℳDirectSum.decompose ℳ: The canonical equivalence provided by the above typeclass
Main statements #
DirectSum.Decomposition.isInternal: The link toDirectSum.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 ℳ)) DirectSum.Decomposition.decompose'
- right_inv : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) DirectSum.Decomposition.decompose'
Instances
instance
DirectSum.instSubsingletonDecomposition
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[DecidableEq ι]
[AddCommMonoid M]
[SetLike σ M]
[AddSubmonoidClass σ M]
(ℳ : ι → σ)
:
DirectSum.Decomposition instances, while carrying data, are always equal.
Equations
- ⋯ = ⋯
@[inline, reducible]
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 : AddMonoidHom.comp (DirectSum.coeAddMonoidHom ℳ) decompose = AddMonoidHom.id M)
(h_right_inv : AddMonoidHom.comp decompose (DirectSum.coeAddMonoidHom ℳ) = AddMonoidHom.id (DirectSum ι fun (i : ι) => ↥(ℳ i)))
:
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 := ⋯ }
Instances For
noncomputable def
DirectSum.IsInternal.chooseDecomposition
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[DecidableEq ι]
[AddCommMonoid M]
[SetLike σ M]
[AddSubmonoidClass σ M]
(ℳ : ι → σ)
(h : DirectSum.IsInternal ℳ)
:
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 := ⋯ }
Instances For
theorem
DirectSum.Decomposition.isInternal
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[DecidableEq ι]
[AddCommMonoid M]
[SetLike σ M]
[AddSubmonoidClass σ M]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
:
def
DirectSum.decompose
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[DecidableEq ι]
[AddCommMonoid M]
[SetLike σ M]
[AddSubmonoidClass σ M]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
:
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 := ⋯ }
Instances For
theorem
DirectSum.Decomposition.inductionOn
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[DecidableEq ι]
[AddCommMonoid M]
[SetLike σ M]
[AddSubmonoidClass σ M]
(ℳ : ι → σ)
[DirectSum.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
DirectSum.Decomposition.decompose'_eq
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[DecidableEq ι]
[AddCommMonoid M]
[SetLike σ M]
[AddSubmonoidClass σ M]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
:
DirectSum.Decomposition.decompose' = ⇑(DirectSum.decompose ℳ)
@[simp]
theorem
DirectSum.decompose_symm_of
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[DecidableEq ι]
[AddCommMonoid M]
[SetLike σ M]
[AddSubmonoidClass σ M]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
{i : ι}
(x : ↥(ℳ i))
:
(DirectSum.decompose ℳ).symm ((DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
{i : ι}
(x : ↥(ℳ i))
:
(DirectSum.decompose ℳ) ↑x = (DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
{x : M}
{i : ι}
(hx : x ∈ ℳ i)
:
(DirectSum.decompose ℳ) x = (DirectSum.of (fun (i : ι) => ↥(ℳ i)) i) { val := x, property := hx }
theorem
DirectSum.decompose_of_mem_same
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[DecidableEq ι]
[AddCommMonoid M]
[SetLike σ M]
[AddSubmonoidClass σ M]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
{x : M}
{i : ι}
(hx : x ∈ ℳ i)
:
↑(((DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
{x : M}
{i : ι}
{j : ι}
(hx : x ∈ ℳ i)
(hij : i ≠ j)
:
↑(((DirectSum.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]
(ℳ : ι → σ)
[DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
:
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 ℳ = AddEquiv.symm (let __src := (DirectSum.decompose ℳ).symm; { toEquiv := __src, map_add' := ⋯ })
Instances For
@[simp]
theorem
DirectSum.decomposeAddEquiv_apply
{ι : Type u_1}
{M : Type u_3}
{σ : Type u_4}
[DecidableEq ι]
[AddCommMonoid M]
[SetLike σ M]
[AddSubmonoidClass σ M]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
(a : M)
:
(DirectSum.decomposeAddEquiv ℳ) a = (DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
(a : DirectSum ι fun (i : ι) => ↥(ℳ i))
:
(AddEquiv.symm (DirectSum.decomposeAddEquiv ℳ)) a = (DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
:
(DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
:
(DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
(x : M)
(y : M)
:
(DirectSum.decompose ℳ) (x + y) = (DirectSum.decompose ℳ) x + (DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
(x : DirectSum ι fun (i : ι) => ↥(ℳ i))
(y : DirectSum ι fun (i : ι) => ↥(ℳ i))
:
(DirectSum.decompose ℳ).symm (x + y) = (DirectSum.decompose ℳ).symm x + (DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
{ι' : Type u_5}
(s : Finset ι')
(f : ι' → M)
:
(DirectSum.decompose ℳ) (Finset.sum s fun (i : ι') => f i) = Finset.sum s fun (i : ι') => (DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
{ι' : Type u_5}
(s : Finset ι')
(f : ι' → DirectSum ι fun (i : ι) => ↥(ℳ i))
:
(DirectSum.decompose ℳ).symm (Finset.sum s fun (i : ι') => f i) = Finset.sum s fun (i : ι') => (DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
[(i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)]
(r : M)
:
(Finset.sum (DFinsupp.support ((DirectSum.decompose ℳ) r)) fun (i : ι) => ↑(((DirectSum.decompose ℳ) r) i)) = r
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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
(x : M)
:
(DirectSum.decompose ℳ) (-x) = -(DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
(x : DirectSum ι fun (i : ι) => ↥(ℳ i))
:
(DirectSum.decompose ℳ).symm (-x) = -(DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
(x : M)
(y : M)
:
(DirectSum.decompose ℳ) (x - y) = (DirectSum.decompose ℳ) x - (DirectSum.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]
(ℳ : ι → σ)
[DirectSum.Decomposition ℳ]
(x : DirectSum ι fun (i : ι) => ↥(ℳ i))
(y : DirectSum ι fun (i : ι) => ↥(ℳ i))
:
(DirectSum.decompose ℳ).symm (x - y) = (DirectSum.decompose ℳ).symm x - (DirectSum.decompose ℳ).symm y
@[inline, reducible]
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 : DirectSum.coeLinearMap ℳ ∘ₗ decompose = LinearMap.id)
(h_right_inv : decompose ∘ₗ DirectSum.coeLinearMap ℳ = LinearMap.id)
:
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 := ⋯ }
Instances For
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)
[DirectSum.Decomposition ℳ]
:
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.
Instances For
@[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)
[DirectSum.Decomposition ℳ]
(m : M)
:
(DirectSum.decomposeLinearEquiv ℳ) m = (DirectSum.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)
[DirectSum.Decomposition ℳ]
(m : DirectSum ι fun (i : ι) => ↥(ℳ i))
:
(LinearEquiv.symm (DirectSum.decomposeLinearEquiv ℳ)) m = (DirectSum.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)
[DirectSum.Decomposition ℳ]
(r : R)
(x : M)
:
(DirectSum.decompose ℳ) (r • x) = r • (DirectSum.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)
[DirectSum.Decomposition ℳ]
(i : ι)
:
↑(LinearEquiv.symm (DirectSum.decomposeLinearEquiv ℳ)) ∘ₗ DirectSum.lof R ι (fun (x : ι) => ↥(ℳ x)) i = Submodule.subtype (ℳ i)
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)
[DirectSum.Decomposition ℳ]
{N : Type u_5}
[AddCommMonoid N]
[Module R N]
⦃f : M →ₗ[R] N⦄
⦃g : M →ₗ[R] N⦄
(h : ∀ (i : ι), f ∘ₗ Submodule.subtype (ℳ i) = g ∘ₗ Submodule.subtype (ℳ i))
:
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.