Documentation

Mathlib.Algebra.DirectSum.Basic

Direct sum #

This file defines the direct sum of abelian groups, indexed by a discrete type.

Notation #

⨁ i, β i is the n-ary direct sum DirectSum. This notation is in the DirectSum locale, accessible after open DirectSum.

References #

def DirectSum (ι : Type v) (β : ιType w) [(i : ι) → AddCommMonoid (β i)] :
Type (max w v)

DirectSum β is the direct sum of a family of additive commutative monoids β i.

Note: open DirectSum will enable the notation ⨁ i, β i for DirectSum β.

Instances For
    instance instInhabitedDirectSum (ι : Type v) (β : ιType w) [(i : ι) → AddCommMonoid (β i)] :
    instance instAddCommMonoidDirectSum (ι : Type v) (β : ιType w) [(i : ι) → AddCommMonoid (β i)] :
    instance instFunLikeDirectSum (ι : Type v) (β : ιType w) [(i : ι) → AddCommMonoid (β i)] :
    FunLike (DirectSum ι β) ι fun i => β i
    instance instCoeFunDirectSumForAll (ι : Type v) (β : ιType w) [(i : ι) → AddCommMonoid (β i)] :
    CoeFun (DirectSum ι β) fun x => (i : ι) → β i

    ⨁ i, f i is notation for DirectSum _ f and equals the direct sum of fun i ↦ f i. Taking the direct sum over multiple arguments is possible, e.g. ⨁ (i) (j), f i j.

    Instances For
      instance DirectSum.instAddCommGroupDirectSumToAddCommMonoid {ι : Type v} (β : ιType w) [(i : ι) → AddCommGroup (β i)] :
      @[simp]
      theorem DirectSum.sub_apply {ι : Type v} {β : ιType w} [(i : ι) → AddCommGroup (β i)] (g₁ : ⨁ (i : ι), β i) (g₂ : ⨁ (i : ι), β i) (i : ι) :
      ↑(g₁ - g₂) i = g₁ i - g₂ i
      @[simp]
      theorem DirectSum.zero_apply {ι : Type v} (β : ιType w) [(i : ι) → AddCommMonoid (β i)] (i : ι) :
      0 i = 0
      @[simp]
      theorem DirectSum.add_apply {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] (g₁ : ⨁ (i : ι), β i) (g₂ : ⨁ (i : ι), β i) (i : ι) :
      ↑(g₁ + g₂) i = g₁ i + g₂ i
      def DirectSum.mk {ι : Type v} [dec_ι : DecidableEq ι] (β : ιType w) [(i : ι) → AddCommMonoid (β i)] (s : Finset ι) :
      ((i : s) → β i) →+ ⨁ (i : ι), β i

      mk β s x is the element of ⨁ i, β i that is zero outside s and has coefficient x i for i in s.

      Instances For
        def DirectSum.of {ι : Type v} [dec_ι : DecidableEq ι] (β : ιType w) [(i : ι) → AddCommMonoid (β i)] (i : ι) :
        β i →+ ⨁ (i : ι), β i

        of i is the natural inclusion map from β i to ⨁ i, β i.

        Instances For
          @[simp]
          theorem DirectSum.of_eq_same {ι : Type v} [dec_ι : DecidableEq ι] (β : ιType w) [(i : ι) → AddCommMonoid (β i)] (i : ι) (x : β i) :
          ↑(↑(DirectSum.of β i) x) i = x
          theorem DirectSum.of_eq_of_ne {ι : Type v} [dec_ι : DecidableEq ι] (β : ιType w) [(i : ι) → AddCommMonoid (β i)] (i : ι) (j : ι) (x : β i) (h : i j) :
          ↑(↑(DirectSum.of β i) x) j = 0
          @[simp]
          theorem DirectSum.support_zero {ι : Type v} [dec_ι : DecidableEq ι] (β : ιType w) [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] :
          @[simp]
          theorem DirectSum.support_of {ι : Type v} [dec_ι : DecidableEq ι] (β : ιType w) [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (i : ι) (x : β i) (h : x 0) :
          DFinsupp.support (↑(DirectSum.of β i) x) = {i}
          theorem DirectSum.support_of_subset {ι : Type v} [dec_ι : DecidableEq ι] (β : ιType w) [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {i : ι} {b : β i} :
          theorem DirectSum.sum_support_of {ι : Type v} [dec_ι : DecidableEq ι] (β : ιType w) [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (x : ⨁ (i : ι), β i) :
          (Finset.sum (DFinsupp.support x) fun i => ↑(DirectSum.of β i) (x i)) = x
          theorem DirectSum.mk_injective {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] (s : Finset ι) :
          theorem DirectSum.of_injective {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] (i : ι) :
          theorem DirectSum.induction_on {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {C : (⨁ (i : ι), β i) → Prop} (x : ⨁ (i : ι), β i) (H_zero : C 0) (H_basic : (i : ι) → (x : β i) → C (↑(DirectSum.of β i) x)) (H_plus : (x y : ⨁ (i : ι), β i) → C xC yC (x + y)) :
          C x
          theorem DirectSum.addHom_ext {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {γ : Type u_1} [AddMonoid γ] ⦃f : (⨁ (i : ι), β i) →+ γ ⦃g : (⨁ (i : ι), β i) →+ γ (H : ∀ (i : ι) (y : β i), f (↑(DirectSum.of β i) y) = g (↑(DirectSum.of β i) y)) :
          f = g

          If two additive homomorphisms from ⨁ i, β i are equal on each of β i y, then they are equal.

          theorem DirectSum.addHom_ext' {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {γ : Type u_1} [AddMonoid γ] ⦃f : (⨁ (i : ι), β i) →+ γ ⦃g : (⨁ (i : ι), β i) →+ γ (H : ∀ (i : ι), AddMonoidHom.comp f (DirectSum.of (fun i => β i) i) = AddMonoidHom.comp g (DirectSum.of (fun i => β i) i)) :
          f = g

          If two additive homomorphisms from ⨁ i, β i are equal on each of β i y, then they are equal.

          See note [partially-applied ext lemmas].

          def DirectSum.toAddMonoid {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) :
          (⨁ (i : ι), β i) →+ γ

          toAddMonoid φ is the natural homomorphism from ⨁ i, β i to γ induced by a family φ of homomorphisms β i → γ.

          Instances For
            @[simp]
            theorem DirectSum.toAddMonoid_of {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i) :
            ↑(DirectSum.toAddMonoid φ) (↑(DirectSum.of β i) x) = ↑(φ i) x
            theorem DirectSum.toAddMonoid.unique {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [AddCommMonoid γ] (ψ : (⨁ (i : ι), β i) →+ γ) (f : ⨁ (i : ι), β i) :
            ψ f = ↑(DirectSum.toAddMonoid fun i => AddMonoidHom.comp ψ (DirectSum.of β i)) f
            def DirectSum.fromAddMonoid {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [AddCommMonoid γ] :
            (⨁ (i : ι), γ →+ β i) →+ γ →+ ⨁ (i : ι), β i

            fromAddMonoid φ is the natural homomorphism from γ to ⨁ i, β i induced by a family φ of homomorphisms γ → β i.

            Note that this is not an isomorphism. Not every homomorphism γ →+ ⨁ i, β i arises in this way.

            Instances For
              @[simp]
              theorem DirectSum.fromAddMonoid_of {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [AddCommMonoid γ] (i : ι) (f : γ →+ β i) :
              DirectSum.fromAddMonoid (↑(DirectSum.of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (DirectSum.of β i) f
              theorem DirectSum.fromAddMonoid_of_apply {ι : Type v} [dec_ι : DecidableEq ι] {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [AddCommMonoid γ] (i : ι) (f : γ →+ β i) (x : γ) :
              ↑(DirectSum.fromAddMonoid (↑(DirectSum.of (fun i => γ →+ β i) i) f)) x = ↑(DirectSum.of β i) (f x)
              def DirectSum.setToSet {ι : Type v} [dec_ι : DecidableEq ι] (β : ιType w) [(i : ι) → AddCommMonoid (β i)] (S : Set ι) (T : Set ι) (H : S T) :
              (⨁ (i : S), β i) →+ ⨁ (i : T), β i

              setToSet β S T h is the natural homomorphism ⨁ (i : S), β i → ⨁ (i : T), β i, where h : S ⊆ T.

              Instances For
                instance DirectSum.unique {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [∀ (i : ι), Subsingleton (β i)] :
                Unique (⨁ (i : ι), β i)
                instance DirectSum.uniqueOfIsEmpty {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [IsEmpty ι] :
                Unique (⨁ (i : ι), β i)

                A direct sum over an empty type is trivial.

                def DirectSum.id (M : Type v) (ι : optParam (Type u_1) PUnit.{u_1 + 1} ) [AddCommMonoid M] [Unique ι] :
                (⨁ (x : ι), M) ≃+ M

                The natural equivalence between ⨁ _ : ι, M and M when Unique ι.

                Instances For
                  def DirectSum.equivCongrLeft {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {κ : Type u_1} (h : ι κ) :
                  (⨁ (i : ι), β i) ≃+ ⨁ (k : κ), β (h.symm k)

                  Reindexing terms of a direct sum.

                  Instances For
                    @[simp]
                    theorem DirectSum.equivCongrLeft_apply {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {κ : Type u_1} (h : ι κ) (f : ⨁ (i : ι), β i) (k : κ) :
                    ↑(↑(DirectSum.equivCongrLeft h) f) k = f (h.symm k)
                    @[simp]
                    theorem DirectSum.addEquivProdDirectSum_apply {ι : Type v} [dec_ι : DecidableEq ι] {α : Option ιType w} [(i : Option ι) → AddCommMonoid (α i)] :
                    ∀ (a : Π₀ (i : Option ι), (fun i => α i) i), DirectSum.addEquivProdDirectSum a = Equiv.toFun DFinsupp.equivProdDFinsupp a
                    @[simp]
                    theorem DirectSum.addEquivProdDirectSum_symm_apply {ι : Type v} [dec_ι : DecidableEq ι] {α : Option ιType w} [(i : Option ι) → AddCommMonoid (α i)] :
                    ∀ (a : (fun i => α i) none × Π₀ (i : ι), (fun i => α i) (some i)), ↑(AddEquiv.symm DirectSum.addEquivProdDirectSum) a = Equiv.invFun DFinsupp.equivProdDFinsupp a
                    noncomputable def DirectSum.addEquivProdDirectSum {ι : Type v} [dec_ι : DecidableEq ι] {α : Option ιType w} [(i : Option ι) → AddCommMonoid (α i)] :
                    (⨁ (i : Option ι), α i) ≃+ α none × ⨁ (i : ι), α (some i)

                    Isomorphism obtained by separating the term of index none of a direct sum over Option ι.

                    Instances For
                      def DirectSum.sigmaCurry {ι : Type v} [dec_ι : DecidableEq ι] {α : ιType u} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] :
                      (⨁ (i : (_i : ι) × α _i), δ i.fst i.snd) →+ ⨁ (i : ι) (j : α i), δ i j

                      The natural map between ⨁ (i : Σ i, α i), δ i.1 i.2 and ⨁ i (j : α i), δ i j.

                      Instances For
                        @[simp]
                        theorem DirectSum.sigmaCurry_apply {ι : Type v} [dec_ι : DecidableEq ι] {α : ιType u} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] (f : ⨁ (i : (_i : ι) × α _i), δ i.fst i.snd) (i : ι) (j : α i) :
                        ↑(↑(DirectSum.sigmaCurry f) i) j = f { fst := i, snd := j }
                        def DirectSum.sigmaUncurry {ι : Type v} {α : ιType u} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → DecidableEq (δ i j)] :
                        (⨁ (i : ι) (j : α i), δ i j) →+ ⨁ (i : (_i : ι) × α _i), δ i.fst i.snd

                        The natural map between ⨁ i (j : α i), δ i j and Π₀ (i : Σ i, α i), δ i.1 i.2, inverse of curry.

                        Instances For
                          @[simp]
                          theorem DirectSum.sigmaUncurry_apply {ι : Type v} {α : ιType u} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → DecidableEq (δ i j)] (f : ⨁ (i : ι) (j : α i), δ i j) (i : ι) (j : α i) :
                          ↑(DirectSum.sigmaUncurry f) { fst := i, snd := j } = ↑(f i) j
                          def DirectSum.sigmaCurryEquiv {ι : Type v} [dec_ι : DecidableEq ι] {α : ιType u} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → DecidableEq (δ i j)] :
                          (⨁ (i : (_i : ι) × α _i), δ i.fst i.snd) ≃+ ⨁ (i : ι) (j : α i), δ i j

                          The natural map between ⨁ (i : Σ i, α i), δ i.1 i.2 and ⨁ i (j : α i), δ i j.

                          Instances For
                            def DirectSum.coeAddMonoidHom {ι : Type v} {M : Type u_1} {S : Type u_2} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ιS) :
                            (⨁ (i : ι), { x // x A i }) →+ M

                            The canonical embedding from ⨁ i, A i to M where A is a collection of AddSubmonoid M indexed by ι.

                            When S = Submodule _ M, this is available as a LinearMap, DirectSum.coe_linearMap.

                            Instances For
                              @[simp]
                              theorem DirectSum.coeAddMonoidHom_of {ι : Type v} {M : Type u_1} {S : Type u_2} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ιS) (i : ι) (x : { x // x A i }) :
                              ↑(DirectSum.coeAddMonoidHom A) (↑(DirectSum.of (fun i => { x // x A i }) i) x) = x
                              theorem DirectSum.coe_of_apply {ι : Type v} {M : Type u_1} {S : Type u_2} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] {A : ιS} (i : ι) (j : ι) (x : { x // x A i }) :
                              ↑(↑(↑(DirectSum.of (fun i => { x // x A i }) i) x) j) = ↑(if i = j then x else 0)
                              def DirectSum.IsInternal {ι : Type v} {M : Type u_1} {S : Type u_2} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ιS) :

                              The DirectSum formed by a collection of additive submonoids (or subgroups, or submodules) of M is said to be internal if the canonical map (⨁ i, A i) →+ M is bijective.

                              For the alternate statement in terms of independence and spanning, see DirectSum.subgroup_isInternal_iff_independent_and_supr_eq_top and DirectSum.isInternalSubmodule_iff_independent_and_supr_eq_top.

                              Instances For