algebra.direct_sum - mathlib docs

source

def direct_sum (ι : Type v) (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] :

Type (max v w)

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

Note: open_locale direct_sum will enable the notation ⨁ i, β i for direct_sum β.

Equations

direct_sum ι β = Π₀ (i : ι), β i

source

@[protected, instance]

def direct_sum.has_coe_to_fun (ι : Type v) (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] :

has_coe_to_fun (direct_sum ι β)

source

@[protected, instance]

def direct_sum.add_comm_monoid (ι : Type v) (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] :

add_comm_monoid (direct_sum ι β)

source

@[protected, instance]

def direct_sum.inhabited (ι : Type v) (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] :

inhabited (direct_sum ι β)

source

@[protected, instance]

def direct_sum.add_comm_group {ι : Type v} (β : ι → Type w) [Π (i : ι), add_comm_group (β i)] :

add_comm_group (direct_sum ι β)

Equations

direct_sum.add_comm_group β = dfinsupp.add_comm_group

source

@[simp]

theorem direct_sum.sub_apply {ι : Type v} {β : ι → Type w} [Π (i : ι), add_comm_group (β i)] (g₁ g₂ : ⨁ (i : ι), β i) (i : ι) :

⇑(g₁ - g₂) i = ⇑g₁ i - ⇑g₂ i

source

@[simp]

theorem direct_sum.zero_apply {ι : Type v} (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] (i : ι) :

⇑0 i = 0

source

@[simp]

theorem direct_sum.add_apply {ι : Type v} {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] (g₁ g₂ : ⨁ (i : ι), β i) (i : ι) :

⇑(g₁ + g₂) i = ⇑g₁ i + ⇑g₂ i

source

def direct_sum.mk {ι : Type v} [dec_ι : decidable_eq ι] (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] (s : finset ι) :

(Π (i : ↥↑s), β i.val) →+ ⨁ (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

direct_sum.mk β s = {to_fun := dfinsupp.mk s, map_zero' := _, map_add' := _}

source

def direct_sum.of {ι : Type v} [dec_ι : decidable_eq ι] (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] (i : ι) :

β i →+ ⨁ (i : ι), β i

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

Equations

direct_sum.of β i = dfinsupp.single_add_hom β i

source

theorem direct_sum.mk_injective {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] (s : finset ι) :

function.injective ⇑(direct_sum.mk β s)

source

theorem direct_sum.of_injective {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] (i : ι) :

function.injective ⇑(direct_sum.of β i)

source

@[protected]

theorem direct_sum.induction_on {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {C : (⨁ (i : ι), β i) → Prop} (x : ⨁ (i : ι), β i) (H_zero : C 0) (H_basic : ∀ (i : ι) (x : β i), C (⇑(direct_sum.of β i) x)) (H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)) :

C x

source

theorem direct_sum.add_hom_ext {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u_1} [add_monoid γ] ⦃f g : (⨁ (i : ι), β i) →+ γ⦄ (H : ∀ (i : ι) (y : β i), ⇑f (⇑(direct_sum.of (λ (i : ι), β i) i) y) = ⇑g (⇑(direct_sum.of (λ (i : ι), β i) i) y)) :

f = g

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

source

@[ext]

theorem direct_sum.add_hom_ext' {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u_1} [add_monoid γ] ⦃f g : (⨁ (i : ι), β i) →+ γ⦄ (H : ∀ (i : ι), f.comp (direct_sum.of (λ (i : ι), β i) i) = g.comp (direct_sum.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].

source

def direct_sum.to_add_monoid {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} [add_comm_monoid γ] (φ : Π (i : ι), β i →+ γ) :

(⨁ (i : ι), β i) →+ γ

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

Equations

direct_sum.to_add_monoid φ = ⇑dfinsupp.lift_add_hom φ

source

@[simp]

theorem direct_sum.to_add_monoid_of {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} [add_comm_monoid γ] (φ : Π (i : ι), β i →+ γ) (i : ι) (x : β i) :

⇑(direct_sum.to_add_monoid φ) (⇑(direct_sum.of β i) x) = ⇑(φ i) x

source

theorem direct_sum.to_add_monoid.unique {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} [add_comm_monoid γ] (ψ : (⨁ (i : ι), β i) →+ γ) (f : ⨁ (i : ι), β i) :

⇑ψ f = ⇑(direct_sum.to_add_monoid (λ (i : ι), ψ.comp (direct_sum.of β i))) f

source

def direct_sum.from_add_monoid {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} [add_comm_monoid γ] :

(⨁ (i : ι), γ →+ β i) →+ γ →+ ⨁ (i : ι), β i

from_add_monoid φ 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

direct_sum.from_add_monoid = direct_sum.to_add_monoid (λ (i : ι), ⇑add_monoid_hom.comp_hom (direct_sum.of β i))

source

@[simp]

theorem direct_sum.from_add_monoid_of {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} [add_comm_monoid γ] (i : ι) (f : γ →+ β i) :

⇑direct_sum.from_add_monoid (⇑(direct_sum.of (λ (i : ι), γ →+ β i) i) f) = (direct_sum.of (λ (i : ι), β i) i).comp f

source

theorem direct_sum.from_add_monoid_of_apply {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} [add_comm_monoid γ] (i : ι) (f : γ →+ β i) (x : γ) :

⇑(⇑direct_sum.from_add_monoid (⇑(direct_sum.of (λ (i : ι), γ →+ β i) i) f)) x = ⇑(direct_sum.of (λ (i : ι), β i) i) (⇑f x)

source

def direct_sum.set_to_set {ι : Type v} [dec_ι : decidable_eq ι] (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] (S T : set ι) (H : S ⊆ T) :

(⨁ (i : ↥S), β ↑i) →+ ⨁ (i : ↥T), β ↑i

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

Equations

direct_sum.set_to_set β S T H = direct_sum.to_add_monoid (λ (i : ↥S), direct_sum.of (λ (i : subtype T), β ↑i) ⟨↑i, _⟩)

source

@[protected]

def direct_sum.id (M : Type v) (ι : Type u_1 := punit) [add_comm_monoid M] [unique ι] :

(⨁ (_x : ι), M) ≃+ M

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

Equations

direct_sum.id M ι = {to_fun := ⇑(direct_sum.to_add_monoid (λ (_x : ι), add_monoid_hom.id M)), inv_fun := ⇑(direct_sum.of (λ (_x : ι), M) (default ι)), left_inv := _, right_inv := _, map_add' := _}

source

def direct_sum.add_submonoid_is_internal {ι : Type v} {M : Type u_1} [decidable_eq ι] [add_comm_monoid M] (A : ι → add_submonoid M) :

Prop

The direct_sum formed by a collection of add_submonoids of M is said to be internal if the canonical map (⨁ i, A i) →+ M is bijective.

See direct_sum.add_subgroup_is_internal for the same statement about add_subgroups.

Equations

direct_sum.add_submonoid_is_internal A = function.bijective ⇑(direct_sum.to_add_monoid (λ (i : ι), (A i).subtype))

source

def direct_sum.add_subgroup_is_internal {ι : Type v} {M : Type u_1} [decidable_eq ι] [add_comm_group M] (A : ι → add_subgroup M) :

Prop

The direct_sum formed by a collection of add_subgroups of M is said to be internal if the canonical map (⨁ i, A i) →+ M is bijective.

See direct_sum.submodule_is_internal for the same statement about submoduless.

Equations

direct_sum.add_subgroup_is_internal A = function.bijective ⇑(direct_sum.to_add_monoid (λ (i : ι), (A i).subtype))

source

theorem direct_sum.add_subgroup_is_internal.to_add_submonoid {ι : Type v} {M : Type u_1} [decidable_eq ι] [add_comm_group M] (A : ι → add_subgroup M) :

direct_sum.add_subgroup_is_internal A ↔ direct_sum.add_submonoid_is_internal (λ (i : ι), (A i).to_add_submonoid)

mathlib documentation

Direct sum #

Notation #

References #