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 direct_sum.
This notation is in the direct_sum locale, accessible after open_locale direct_sum.
References
- https://en.wikipedia.org/wiki/Direct_sum
def
direct_sum
(ι : Type v)
[decidable_eq ι]
(β : ι → Type w)
[Π (i : ι), add_comm_group (β i)] :
Type (max v w)
Equations
- direct_sum ι β = Π₀ (i : ι), β i
@[instance]
def
direct_sum.add_comm_group
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)] :
add_comm_group (⨁ (i : ι), β i)
@[instance]
def
direct_sum.inhabited
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)] :
inhabited (⨁ (i : ι), β i)
Equations
- direct_sum.inhabited = {default := 0}
def
direct_sum.mk
{ι : Type v}
[decidable_eq ι]
(β : ι → Type w)
[Π (i : ι), add_comm_group (β i)]
(s : finset ι)
(a : Π (i : ↥↑s), β i.val) :
⨁ (i : ι), β i
Equations
def
direct_sum.of
{ι : Type v}
[decidable_eq ι]
(β : ι → Type w)
[Π (i : ι), add_comm_group (β i)]
(i : ι)
(a : β i) :
⨁ (i : ι), β i
Equations
@[instance]
def
direct_sum.mk.is_add_group_hom
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(s : finset ι) :
@[simp]
theorem
direct_sum.mk_zero
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(s : finset ι) :
direct_sum.mk β s 0 = 0
@[simp]
theorem
direct_sum.mk_add
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(s : finset ι)
(x y : Π (i : ↥↑s), β i.val) :
direct_sum.mk β s (x + y) = direct_sum.mk β s x + direct_sum.mk β s y
@[simp]
theorem
direct_sum.mk_neg
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(s : finset ι)
(x : Π (i : ↥↑s), β i.val) :
direct_sum.mk β s (-x) = -direct_sum.mk β s x
@[simp]
theorem
direct_sum.mk_sub
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(s : finset ι)
(x y : Π (i : ↥↑s), β i.val) :
direct_sum.mk β s (x - y) = direct_sum.mk β s x - direct_sum.mk β s y
@[instance]
def
direct_sum.of.is_add_group_hom
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(i : ι) :
@[simp]
theorem
direct_sum.of_zero
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(i : ι) :
direct_sum.of β i 0 = 0
@[simp]
theorem
direct_sum.of_add
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(i : ι)
(x y : β i) :
direct_sum.of β i (x + y) = direct_sum.of β i x + direct_sum.of β i y
@[simp]
theorem
direct_sum.of_neg
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(i : ι)
(x : β i) :
direct_sum.of β i (-x) = -direct_sum.of β i x
@[simp]
theorem
direct_sum.of_sub
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(i : ι)
(x y : β i) :
direct_sum.of β i (x - y) = direct_sum.of β i x - direct_sum.of β i y
theorem
direct_sum.mk_injective
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(s : finset ι) :
theorem
direct_sum.of_injective
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(i : ι) :
theorem
direct_sum.induction_on
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β 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
def
direct_sum.to_group
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
{γ : Type u₁}
[add_comm_group γ]
(φ : Π (i : ι), β i → γ)
[∀ (i : ι), is_add_group_hom (φ i)]
(f : ⨁ (i : ι), β i) :
γ
Equations
- direct_sum.to_group φ f = quotient.lift_on f (λ (x : dfinsupp.pre ι (λ (i : ι), (λ (i : ι), β i) i)), ∑ (i : ι) in x.pre_support.to_finset, φ i (x.to_fun i)) _
@[instance]
def
direct_sum.to_group.is_add_group_hom
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
{γ : Type u₁}
[add_comm_group γ]
{φ : Π (i : ι), β i → γ}
[∀ (i : ι), is_add_group_hom (φ i)] :
@[simp]
theorem
direct_sum.to_group_zero
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
{γ : Type u₁}
[add_comm_group γ]
(φ : Π (i : ι), β i → γ)
[∀ (i : ι), is_add_group_hom (φ i)] :
direct_sum.to_group φ 0 = 0
@[simp]
theorem
direct_sum.to_group_add
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
{γ : Type u₁}
[add_comm_group γ]
(φ : Π (i : ι), β i → γ)
[∀ (i : ι), is_add_group_hom (φ i)]
(x y : ⨁ (i : ι), β i) :
direct_sum.to_group φ (x + y) = direct_sum.to_group φ x + direct_sum.to_group φ y
@[simp]
theorem
direct_sum.to_group_neg
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
{γ : Type u₁}
[add_comm_group γ]
(φ : Π (i : ι), β i → γ)
[∀ (i : ι), is_add_group_hom (φ i)]
(x : ⨁ (i : ι), β i) :
direct_sum.to_group φ (-x) = -direct_sum.to_group φ x
@[simp]
theorem
direct_sum.to_group_sub
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
{γ : Type u₁}
[add_comm_group γ]
(φ : Π (i : ι), β i → γ)
[∀ (i : ι), is_add_group_hom (φ i)]
(x y : ⨁ (i : ι), β i) :
direct_sum.to_group φ (x - y) = direct_sum.to_group φ x - direct_sum.to_group φ y
@[simp]
theorem
direct_sum.to_group_of
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
{γ : Type u₁}
[add_comm_group γ]
(φ : Π (i : ι), β i → γ)
[∀ (i : ι), is_add_group_hom (φ i)]
(i : ι)
(x : β i) :
direct_sum.to_group φ (direct_sum.of β i x) = φ i x
theorem
direct_sum.to_group.unique
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
{γ : Type u₁}
[add_comm_group γ]
(ψ : (⨁ (i : ι), β i) → γ)
[is_add_group_hom ψ]
(f : ⨁ (i : ι), β i) :
ψ f = direct_sum.to_group (λ (i : ι), ψ ∘ direct_sum.of β i) f
def
direct_sum.set_to_set
{ι : Type v}
[decidable_eq ι]
(β : ι → Type w)
[Π (i : ι), add_comm_group (β i)]
(S T : set ι)
(H : S ⊆ T)
(a : ⨁ (i : ↥S), β ↑i) :
Equations
- direct_sum.set_to_set β S T H = direct_sum.to_group (λ (i : ↥S), direct_sum.of (β ∘ subtype.val) ⟨i.val, _⟩)
@[instance]
def
direct_sum.is_add_group_hom
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(S T : set ι)
(H : S ⊆ T) :
is_add_group_hom (direct_sum.set_to_set β S T H)
Equations
- direct_sum.id M = {to_fun := direct_sum.to_group (λ (_x : punit), id) _, inv_fun := direct_sum.of (λ (_x : punit), M) punit.star, left_inv := _, right_inv := _}
@[instance]
def
direct_sum.has_coe_to_fun
{ι : Type v}
[decidable_eq ι]
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)] :
has_coe_to_fun (⨁ (i : ι), β i)