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

• https://en.wikipedia.org/wiki/Direct_sum

ink

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

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

• DirectSum ι β = Dfinsupp fun i => β i

ink

instance instInhabitedDirectSum (ι : Type v) (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] : Inhabited (DirectSum ι β)

Equations

• instInhabitedDirectSum ι β = inferInstanceAs (Inhabited (Dfinsupp fun i => β i))

ink

instance instAddCommMonoidDirectSum (ι : Type v) (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] : AddCommMonoid (DirectSum ι β)

Equations

• instAddCommMonoidDirectSum ι β = inferInstanceAs (AddCommMonoid (Dfinsupp fun i => β i))

ink

instance instCoeFunDirectSumForAll (ι : Type v) (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] : CoeFun (DirectSum ι β) fun x => (i : ι) → β i

Equations

• instCoeFunDirectSumForAll ι β = inferInstanceAs (CoeFun (Dfinsupp fun i => β i) fun x => (i : ι) → β i)

ink

def «⨁_,_» : Lean.ParserDescr

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

ink

instance DirectSum.instAddCommGroupDirectSumToAddCommMonoid {ι : Type v} (β : ι → Type w) [inst : (i : ι) → AddCommGroup (β i)] : AddCommGroup (DirectSum ι β)

Equations

• DirectSum.instAddCommGroupDirectSumToAddCommMonoid β = inferInstanceAs (AddCommGroup (Dfinsupp fun i => β i))

ink

@[simp]

theorem DirectSum.sub_apply {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommGroup (β i)] (g₁ : DirectSum ι fun i => β i) (g₂ : DirectSum ι fun i => β i) (i : ι) : ↑(g₁ - g₂) i = ↑g₁ i - ↑g₂ i

ink

@[simp]

theorem DirectSum.zero_apply {ι : Type v} (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (i : ι) : ↑0 i = 0

ink

@[simp]

theorem DirectSum.add_apply {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] (g₁ : DirectSum ι fun i => β i) (g₂ : DirectSum ι fun i => β i) (i : ι) : ↑(g₁ + g₂) i = ↑g₁ i + ↑g₂ i

ink

def DirectSum.mk {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (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

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

ink

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

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

Equations

• DirectSum.of β i = Dfinsupp.singleAddHom β i

ink

@[simp]

theorem DirectSum.of_eq_same {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (i : ι) (x : β i) : ↑(↑(DirectSum.of β i) x) i = x

ink

theorem DirectSum.of_eq_of_ne {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (i : ι) (j : ι) (x : β i) (h : i ≠ j) : ↑(↑(DirectSum.of β i) x) j = 0

ink

@[simp]

theorem DirectSum.support_zero {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)] : Dfinsupp.support 0 = ∅

ink

@[simp]

theorem DirectSum.support_of {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (i : ι) (x : β i) (h : x ≠ 0) : Dfinsupp.support (↑(DirectSum.of β i) x) = {i}

ink

theorem DirectSum.support_of_subset {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i} : Dfinsupp.support (↑(DirectSum.of β i) b) ⊆ {i}

ink

theorem DirectSum.sum_support_of {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (x : DirectSum ι fun i => β i) : (Finset.sum (Dfinsupp.support x) fun i => ↑(DirectSum.of β i) (↑x i)) = x

ink

theorem DirectSum.mk_injective {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] (s : Finset ι) : Function.Injective ↑(DirectSum.mk β s)

ink

theorem DirectSum.of_injective {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] (i : ι) : Function.Injective ↑(DirectSum.of β i)

ink

theorem DirectSum.induction_on {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {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 x → C y → C (x + y)) : C x

ink

theorem DirectSum.addHom_ext {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u_1} [inst : 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.

ink

theorem DirectSum.addHom_ext' {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u_1} [inst : AddMonoid γ] ⦃f : (DirectSum ι fun i => β i) →+ γ⦄ ⦃g : (DirectSum ι fun 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].

ink

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

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

Equations

• DirectSum.toAddMonoid φ = ↑Dfinsupp.liftAddHom φ

ink

@[simp]

theorem DirectSum.toAddMonoid_of {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [inst : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i) : ↑(DirectSum.toAddMonoid φ) (↑(DirectSum.of β i) x) = ↑(φ i) x

ink

theorem DirectSum.toAddMonoid.unique {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [inst : AddCommMonoid γ] (ψ : (DirectSum ι fun i => β i) →+ γ) (f : DirectSum ι fun i => β i) : ↑ψ f = ↑(DirectSum.toAddMonoid fun i => AddMonoidHom.comp ψ (DirectSum.of β i)) f

ink

def DirectSum.fromAddMonoid {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [inst : 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

• DirectSum.fromAddMonoid = DirectSum.toAddMonoid fun i => ↑AddMonoidHom.compHom (DirectSum.of β i)

ink

@[simp]

theorem DirectSum.fromAddMonoid_of {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [inst : AddCommMonoid γ] (i : ι) (f : γ →+ β i) : ↑DirectSum.fromAddMonoid (↑(DirectSum.of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (DirectSum.of β i) f

ink

theorem DirectSum.fromAddMonoid_of_apply {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁} [inst : AddCommMonoid γ] (i : ι) (f : γ →+ β i) (x : γ) : ↑(↑DirectSum.fromAddMonoid (↑(DirectSum.of (fun i => γ →+ β i) i) f)) x = ↑(DirectSum.of β i) (↑f x)

ink

def DirectSum.setToSet {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (S : Set ι) (T : Set ι) (H : S ⊆ T) : (DirectSum ↑S fun i => β ↑i) →+ DirectSum ↑T fun i => β ↑i

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

Equations

• DirectSum.setToSet β S T H = DirectSum.toAddMonoid fun i => DirectSum.of (fun i => β ↑i) { val := ↑i, property := (_ : ↑i ∈ T) }

ink

instance DirectSum.unique {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst : ∀ (i : ι), Subsingleton (β i)] : Unique (DirectSum ι fun i => β i)

Equations

• DirectSum.unique = Dfinsupp.unique

ink

instance DirectSum.uniqueOfIsEmpty {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst : IsEmpty ι] : Unique (DirectSum ι fun i => β i)

A direct sum over an empty type is trivial.

Equations

• DirectSum.uniqueOfIsEmpty = Dfinsupp.uniqueOfIsEmpty

ink

def DirectSum.id (M : Type v) (ι : optParam (Type u_1) PUnit) [inst : AddCommMonoid M] [inst : Unique ι] : (DirectSum ι fun _x => M) ≃+ M

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

Equations

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

ink

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

Reindexing terms of a direct sum.

Equations

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

ink

@[simp]

theorem DirectSum.equivCongrLeft_apply {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {κ : Type u_1} (h : ι ≃ κ) (f : DirectSum ι fun i => β i) (k : κ) : ↑(↑(DirectSum.equivCongrLeft h) f) k = ↑f (↑(Equiv.symm h) k)

ink

@[simp]

theorem DirectSum.addEquivProdDirectSum_apply {ι : Type v} [dec_ι : DecidableEq ι] {α : Option ι → Type w} [inst : (i : Option ι) → AddCommMonoid (α i)] : ∀ (a : Dfinsupp fun i => (fun i => α i) i), ↑DirectSum.addEquivProdDirectSum a = Equiv.toFun Dfinsupp.equivProdDfinsupp a

ink

@[simp]

theorem DirectSum.addEquivProdDirectSum_symm_apply {ι : Type v} [dec_ι : DecidableEq ι] {α : Option ι → Type w} [inst : (i : Option ι) → AddCommMonoid (α i)] : ∀ (a : (fun i => α i) none × Dfinsupp fun i => (fun i => α i) (some i)), ↑(AddEquiv.symm DirectSum.addEquivProdDirectSum) a = Equiv.invFun Dfinsupp.equivProdDfinsupp a

ink

noncomputable def DirectSum.addEquivProdDirectSum {ι : Type v} [dec_ι : DecidableEq ι] {α : Option ι → Type w} [inst : (i : Option ι) → AddCommMonoid (α i)] : (DirectSum (Option ι) fun i => α i) ≃+ α none × DirectSum ι fun i => α (some i)

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

Equations

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

ink

noncomputable def DirectSum.sigmaCurry {ι : Type v} {α : ι → Type u} {δ : (i : ι) → α i → Type w} [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] : (DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) →+ DirectSum ι fun i => DirectSum (α i) fun j => δ i j

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

Equations

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

ink

@[simp]

theorem DirectSum.sigmaCurry_apply {ι : Type v} {α : ι → Type u} {δ : (i : ι) → α i → Type w} [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] (f : DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) (i : ι) (j : α i) : ↑(↑(↑DirectSum.sigmaCurry f) i) j = ↑f { fst := i, snd := j }

ink

noncomputable def DirectSum.sigmaUncurry {ι : Type v} {α : ι → Type u} {δ : (i : ι) → α i → Type w} [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → DecidableEq (δ i j)] : (DirectSum ι fun i => DirectSum (α i) fun j => δ i j) →+ DirectSum ((_i : ι) × α _i) fun 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

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

ink

@[simp]

theorem DirectSum.sigmaUncurry_apply {ι : Type v} {α : ι → Type u} {δ : (i : ι) → α i → Type w} [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → DecidableEq (δ i j)] (f : DirectSum ι fun i => DirectSum (α i) fun j => δ i j) (i : ι) (j : α i) : ↑(↑DirectSum.sigmaUncurry f) { fst := i, snd := j } = ↑(↑f i) j

ink

noncomputable def DirectSum.sigmaCurryEquiv {ι : Type v} {α : ι → Type u} {δ : (i : ι) → α i → Type w} [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → DecidableEq (δ i j)] : (DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) ≃+ DirectSum ι fun i => DirectSum (α i) fun j => δ i j

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

Equations

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

ink

def DirectSum.coeAddMonoidHom {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst : AddCommMonoid M] [inst : SetLike S M] [inst : AddSubmonoidClass S M] (A : ι → S) : (DirectSum ι fun 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.

Equations

• DirectSum.coeAddMonoidHom A = DirectSum.toAddMonoid fun i => AddSubmonoidClass.Subtype (A i)

ink

@[simp]

theorem DirectSum.coeAddMonoidHom_of {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst : AddCommMonoid M] [inst : SetLike S M] [inst : 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

ink

theorem DirectSum.coe_of_apply {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst : AddCommMonoid M] [inst : SetLike S M] [inst : 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)

ink

def DirectSum.IsInternal {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst : AddCommMonoid M] [inst : SetLike S M] [inst : AddSubmonoidClass S M] (A : ι → S) : Prop

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.

Equations

• DirectSum.IsInternal A = Function.Bijective ↑(DirectSum.coeAddMonoidHom A)

ink

theorem DirectSum.IsInternal.addSubmonoid_supᵢ_eq_top {ι : Type v} {M : Type u_1} [inst : DecidableEq ι] [inst : AddCommMonoid M] (A : ι → AddSubmonoid M) (h : DirectSum.IsInternal A) : supᵢ A = ⊤