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

Equations
Instances For
    instance instInhabitedDirectSum (ι : Type v) (β : ιType w) [(i : ι) → AddCommMonoid (β i)] :
    Equations
    instance instAddCommMonoidDirectSum (ι : Type v) (β : ιType w) [(i : ι) → AddCommMonoid (β i)] :
    Equations
    instance instDFunLikeDirectSum (ι : Type v) (β : ιType w) [(i : ι) → AddCommMonoid (β i)] :
    DFunLike (DirectSum ι β) ι fun (i : ι) => β i
    Equations
    instance instCoeFunDirectSumForall (ι : Type v) (β : ιType w) [(i : ι) → AddCommMonoid (β i)] :
    CoeFun (DirectSum ι β) fun (x : DirectSum ι β) => (i : ι) → β i
    Equations

    Pretty printer defined by notation3 command.

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

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        instance instDecidableEqDirectSum (ι : Type v) (β : ιType w) [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → DecidableEq (β i)] :
        Equations
        instance DirectSum.instAddCommGroup {ι : Type v} (β : ιType w) [(i : ι) → AddCommGroup (β i)] :
        Equations
        @[simp]
        theorem DirectSum.sub_apply {ι : Type v} {β : ιType w} [(i : ι) → AddCommGroup (β i)] (g₁ : DirectSum ι fun (i : ι) => β i) (g₂ : DirectSum ι fun (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₁ : DirectSum ι fun (i : ι) => β i) (g₂ : DirectSum ι fun (i : ι) => β i) (i : ι) :
        (g₁ + g₂) i = g₁ i + g₂ i
        def DirectSum.mk {ι : Type v} (β : ιType w) [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (s : Finset ι) :
        ((i : s) → β i) →+ DirectSum ι fun (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.

        Equations
        Instances For
          def DirectSum.of {ι : Type v} (β : ιType w) [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (i : ι) :
          β i →+ DirectSum ι fun (i : ι) => β i

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

          Equations
          Instances For
            @[simp]
            theorem DirectSum.of_eq_same {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (i : ι) (x : β i) :
            ((DirectSum.of β i) x) i = x
            theorem DirectSum.of_eq_of_ne {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (i : ι) (j : ι) (x : β i) (h : i j) :
            ((DirectSum.of β i) x) j = 0
            theorem DirectSum.of_apply {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {i : ι} (j : ι) (x : β i) :
            ((DirectSum.of β i) x) j = if h : i = j then Eq.recOn h x else 0
            theorem DirectSum.mk_apply_of_mem {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {s : Finset ι} {f : (i : s) → β i} {n : ι} (hn : n s) :
            ((DirectSum.mk β s) f) n = f n, hn
            theorem DirectSum.mk_apply_of_not_mem {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {s : Finset ι} {f : (i : s) → β i} {n : ι} (hn : ns) :
            ((DirectSum.mk β s) f) n = 0
            @[simp]
            theorem DirectSum.support_zero {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] [(i : ι) → (x : β i) → Decidable (x 0)] :
            @[simp]
            theorem DirectSum.support_of {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] [(i : ι) → (x : β i) → Decidable (x 0)] (i : ι) (x : β i) (h : x 0) :
            theorem DirectSum.support_of_subset {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] [(i : ι) → (x : β i) → Decidable (x 0)] {i : ι} {b : β i} :
            theorem DirectSum.sum_support_of {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] [(i : ι) → (x : β i) → Decidable (x 0)] (x : DirectSum ι fun (i : ι) => β i) :
            iDFinsupp.support x, (DirectSum.of β i) (x i) = x
            theorem DirectSum.sum_univ_of {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] [Fintype ι] (x : DirectSum ι fun (i : ι) => β i) :
            i : ι, (DirectSum.of β i) (x i) = x
            theorem DirectSum.mk_injective {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (s : Finset ι) :
            theorem DirectSum.of_injective {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (i : ι) :
            theorem DirectSum.induction_on {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {C : (DirectSum ι fun (i : ι) => β i)Prop} (x : DirectSum ι fun (i : ι) => β i) (H_zero : C 0) (H_basic : ∀ (i : ι) (x : β i), C ((DirectSum.of β i) x)) (H_plus : ∀ (x y : DirectSum ι fun (i : ι) => β i), C xC yC (x + y)) :
            C x
            theorem DirectSum.addHom_ext {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u_1} [AddMonoid γ] ⦃f : (DirectSum ι fun (i : ι) => β i) →+ γ ⦃g : (DirectSum ι fun (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'_iff {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u_1} [AddMonoid γ] {f : (DirectSum ι fun (i : ι) => β i) →+ γ} {g : (DirectSum ι fun (i : ι) => β i) →+ γ} :
            f = g ∀ (i : ι), f.comp (DirectSum.of β i) = g.comp (DirectSum.of β i)
            theorem DirectSum.addHom_ext' {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u_1} [AddMonoid γ] ⦃f : (DirectSum ι fun (i : ι) => β i) →+ γ ⦃g : (DirectSum ι fun (i : ι) => β i) →+ γ (H : ∀ (i : ι), f.comp (DirectSum.of β i) = g.comp (DirectSum.of β 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} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) :
            (DirectSum ι fun (i : ι) => β i) →+ γ

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

            Equations
            Instances For
              @[simp]
              theorem DirectSum.toAddMonoid_of {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i) :
              (DirectSum.toAddMonoid φ) ((DirectSum.of β i) x) = (φ i) x
              theorem DirectSum.toAddMonoid.unique {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] (ψ : (DirectSum ι fun (i : ι) => β i) →+ γ) (f : DirectSum ι fun (i : ι) => β i) :
              ψ f = (DirectSum.toAddMonoid fun (i : ι) => ψ.comp (DirectSum.of β i)) f
              theorem DirectSum.toAddMonoid_injective {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] :
              Function.Injective DirectSum.toAddMonoid
              @[simp]
              theorem DirectSum.toAddMonoid_inj {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] {f : (i : ι) → β i →+ γ} {g : (i : ι) → β i →+ γ} :
              def DirectSum.fromAddMonoid {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] :
              (DirectSum ι fun (i : ι) => γ →+ β i) →+ γ →+ DirectSum ι fun (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.

              Equations
              Instances For
                @[simp]
                theorem DirectSum.fromAddMonoid_of {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] (i : ι) (f : γ →+ β i) :
                DirectSum.fromAddMonoid ((DirectSum.of (fun (i : ι) => γ →+ β i) i) f) = (DirectSum.of β i).comp f
                theorem DirectSum.fromAddMonoid_of_apply {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : 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} (β : ιType w) [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (S : Set ι) (T : Set ι) (H : S T) :
                (DirectSum S fun (i : S) => β i) →+ DirectSum T fun (i : T) => β i

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

                Equations
                Instances For
                  instance DirectSum.unique {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [∀ (i : ι), Subsingleton (β i)] :
                  Unique (DirectSum ι fun (i : ι) => β i)
                  Equations
                  • DirectSum.unique = DFinsupp.unique
                  instance DirectSum.uniqueOfIsEmpty {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] [IsEmpty ι] :
                  Unique (DirectSum ι fun (i : ι) => β i)

                  A direct sum over an empty type is trivial.

                  Equations
                  • DirectSum.uniqueOfIsEmpty = DFinsupp.uniqueOfIsEmpty
                  def DirectSum.id (M : Type v) (ι : optParam (Type u_1) PUnit.{u_1 + 1} ) [AddCommMonoid M] [Unique ι] :
                  (DirectSum ι fun (x : ι) => M) ≃+ M

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

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

                    Reindexing terms of a direct sum.

                    Equations
                    Instances For
                      @[simp]
                      theorem DirectSum.equivCongrLeft_apply {ι : Type v} {β : ιType w} [(i : ι) → AddCommMonoid (β i)] {κ : Type u_1} (h : ι κ) (f : DirectSum ι fun (i : ι) => β i) (k : κ) :
                      ((DirectSum.equivCongrLeft h) f) k = f (h.symm k)
                      @[simp]
                      theorem DirectSum.addEquivProdDirectSum_symm_apply_support' {ι : Type v} {α : Option ιType w} [(i : Option ι) → AddCommMonoid (α i)] (f : (fun (i : Option ι) => α i) none × Π₀ (i : ι), (fun (i : Option ι) => α i) (some i)) :
                      (DirectSum.addEquivProdDirectSum.symm f).support' = Trunc.map (fun (s : { s : Multiset ι // ∀ (i : ι), i s f.2 i = 0 }) => none ::ₘ Multiset.map some s, ) f.2.support'
                      @[simp]
                      theorem DirectSum.addEquivProdDirectSum_apply {ι : Type v} {α : Option ιType w} [(i : Option ι) → AddCommMonoid (α i)] (f : Π₀ (i : Option ι), (fun (i : Option ι) => α i) i) :
                      DirectSum.addEquivProdDirectSum f = (f none, DFinsupp.comapDomain some f)
                      @[simp]
                      theorem DirectSum.addEquivProdDirectSum_symm_apply_toFun {ι : Type v} {α : Option ιType w} [(i : Option ι) → AddCommMonoid (α i)] (f : (fun (i : Option ι) => α i) none × Π₀ (i : ι), (fun (i : Option ι) => α i) (some i)) (i : Option ι) :
                      (DirectSum.addEquivProdDirectSum.symm f) i = match i with | none => f.1 | some val => f.2 val
                      noncomputable def DirectSum.addEquivProdDirectSum {ι : Type v} {α : Option ιType w} [(i : Option ι) → AddCommMonoid (α i)] :
                      (DirectSum (Option ι) fun (i : Option ι) => α i) ≃+ α none × DirectSum ι fun (i : ι) => α (some i)

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

                      Equations
                      • DirectSum.addEquivProdDirectSum = { toEquiv := DFinsupp.equivProdDFinsupp, map_add' := }
                      Instances For
                        def DirectSum.sigmaCurry {ι : Type v} [DecidableEq ι] {α : ιType u} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] :
                        (DirectSum ((_i : ι) × α _i) fun (i : (_i : ι) × α _i) => δ i.fst i.snd) →+ DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j

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

                        Equations
                        • DirectSum.sigmaCurry = { toFun := DFinsupp.sigmaCurry, map_zero' := , map_add' := }
                        Instances For
                          @[simp]
                          theorem DirectSum.sigmaCurry_apply {ι : Type v} [DecidableEq ι] {α : ιType u} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] (f : DirectSum ((_i : ι) × α _i) fun (i : (_i : ι) × α _i) => δ i.fst i.snd) (i : ι) (j : α i) :
                          ((DirectSum.sigmaCurry f) i) j = f i, j
                          def DirectSum.sigmaUncurry {ι : Type v} [DecidableEq ι] {α : ιType u} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] :
                          (DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j) →+ DirectSum ((_i : ι) × α _i) fun (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.

                          Equations
                          • DirectSum.sigmaUncurry = { toFun := DFinsupp.sigmaUncurry, map_zero' := , map_add' := }
                          Instances For
                            @[simp]
                            theorem DirectSum.sigmaUncurry_apply {ι : Type v} [DecidableEq ι] {α : ιType u} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] (f : DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j) (i : ι) (j : α i) :
                            (DirectSum.sigmaUncurry f) i, j = (f i) j
                            def DirectSum.sigmaCurryEquiv {ι : Type v} [DecidableEq ι] {α : ιType u} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] :
                            (DirectSum ((_i : ι) × α _i) fun (i : (_i : ι) × α _i) => δ i.fst i.snd) ≃+ DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j

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

                            Equations
                            • DirectSum.sigmaCurryEquiv = { toFun := (↑DirectSum.sigmaCurry).toFun, invFun := DFinsupp.sigmaCurryEquiv.invFun, left_inv := , right_inv := , map_add' := }
                            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) :
                              (DirectSum ι fun (i : ι) => (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.

                              Equations
                              Instances For
                                theorem DirectSum.coeAddMonoidHom_eq_dfinsupp_sum {ι : Type v} [DecidableEq ι] {M : Type u_1} {S : Type u_2} [DecidableEq M] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ιS) (x : DirectSum ι fun (i : ι) => (A i)) :
                                (DirectSum.coeAddMonoidHom A) x = DFinsupp.sum x fun (i : ι) (x : (A i)) => x
                                @[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 : (A i)) :
                                (DirectSum.coeAddMonoidHom A) ((DirectSum.of (fun (i : ι) => (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 : (A i)) :
                                (((DirectSum.of (fun (i : ι) => (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.isInternal_submodule_iff_independent_and_iSup_eq_top.

                                Equations
                                Instances For
                                  theorem DirectSum.support_subset {ι : Type v} {M : Type u_1} {S : Type u_2} [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] [DecidableEq ι] [DecidableEq M] (A : ιS) (x : DirectSum ι fun (i : ι) => (A i)) :
                                  (Function.support fun (i : ι) => (x i)) (DFinsupp.support x)
                                  theorem DirectSum.finite_support {ι : Type v} {M : Type u_1} {S : Type u_2} [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ιS) (x : DirectSum ι fun (i : ι) => (A i)) :
                                  (Function.support fun (i : ι) => (x i)).Finite