Documentation

Mathlib.Algebra.DirectSum.Decomposition

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

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 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.

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
    • One or more equations did not get rendered due to their size.
    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
      • One or more equations did not get rendered due to their size.
      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 ] :
        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
        • One or more equations did not get rendered due to their size.
        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 : MProp} (h_zero : p 0) (h_homogeneous : ∀ {i : ι} (m : ( i)), p m) (h_add : ∀ (m m' : M), p mp 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 ] :
          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
          • One or more equations did not get rendered due to their size.
          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) :
            @[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)) :
            @[simp]
            theorem DirectSum.decompose_zero {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ισ) [DirectSum.Decomposition ] :
            @[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) :
            @[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
            @[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) :
            @[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) :
            @[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
            • One or more equations did not get rendered due to their size.
            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 ] :
              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.
              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) :
                @[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)) :
                @[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) :
                @[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.