# Topological sums and functorial constructions #

Lemmas on the interaction of tprod, tsum, HasProd, HasSum etc with products, Sigma and Pi types, MulOpposite, etc.

## Product, Sigma and Pi types #

theorem hasSum_pi_single {α : Type u_1} {β : Type u_2} [] [] [] (b : β) (a : α) :
HasSum () a
theorem hasProd_pi_single {α : Type u_1} {β : Type u_2} [] [] [] (b : β) (a : α) :
HasProd () a
@[simp]
theorem tsum_pi_single {α : Type u_1} {β : Type u_2} [] [] [] (b : β) (a : α) :
∑' (b' : β), Pi.single b a b' = a
@[simp]
theorem tprod_pi_single {α : Type u_1} {β : Type u_2} [] [] [] (b : β) (a : α) :
∏' (b' : β), Pi.mulSingle b a b' = a
theorem tsum_setProd_singleton_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (b : β) (t : Set γ) (f : β × γα) :
∑' (x : ({b} ×ˢ t)), f x = ∑' (c : t), f (b, c)
theorem tprod_setProd_singleton_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (b : β) (t : Set γ) (f : β × γα) :
∏' (x : ({b} ×ˢ t)), f x = ∏' (c : t), f (b, c)
theorem tsum_setProd_singleton_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (s : Set β) (c : γ) (f : β × γα) :
∑' (x : (s ×ˢ {c})), f x = ∑' (b : s), f (b, c)
theorem tprod_setProd_singleton_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (s : Set β) (c : γ) (f : β × γα) :
∏' (x : (s ×ˢ {c})), f x = ∏' (b : s), f (b, c)
theorem Summable.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : β × γα} (hf : ) :
Summable fun (p : γ × β) => f p.swap
theorem Multipliable.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : β × γα} (hf : ) :
Multipliable fun (p : γ × β) => f p.swap
theorem HasSum.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : βα} {g : βγ} {a : α} {b : γ} (hf : HasSum f a) (hg : HasSum g b) :
HasSum (fun (x : β) => (f x, g x)) (a, b)
theorem HasProd.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : βα} {g : βγ} {a : α} {b : γ} (hf : HasProd f a) (hg : HasProd g b) :
HasProd (fun (x : β) => (f x, g x)) (a, b)
theorem HasSum.sigma {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} {g : βα} {a : α} (ha : HasSum f a) (hf : ∀ (b : β), HasSum (fun (c : γ b) => f b, c) (g b)) :
HasSum g a
theorem HasProd.sigma {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} {g : βα} {a : α} (ha : HasProd f a) (hf : ∀ (b : β), HasProd (fun (c : γ b) => f b, c) (g b)) :
theorem HasSum.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : β × γα} {g : βα} {a : α} (ha : HasSum f a) (hf : ∀ (b : β), HasSum (fun (c : γ) => f (b, c)) (g b)) :
HasSum g a

If a series f on β × γ has sum a and for each b the restriction of f to {b} × γ has sum g b, then the series g has sum a.

theorem HasProd.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : β × γα} {g : βα} {a : α} (ha : HasProd f a) (hf : ∀ (b : β), HasProd (fun (c : γ) => f (b, c)) (g b)) :

If a function f on β × γ has product a and for each b the restriction of f to {b} × γ has product g b, then the function g has product a.

theorem Summable.sigma' {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} (ha : ) (hf : ∀ (b : β), Summable fun (c : γ b) => f b, c) :
Summable fun (b : β) => ∑' (c : γ b), f b, c
theorem Multipliable.sigma' {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} (ha : ) (hf : ∀ (b : β), Multipliable fun (c : γ b) => f b, c) :
Multipliable fun (b : β) => ∏' (c : γ b), f b, c
theorem HasSum.sigma_of_hasSum {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} {g : βα} {a : α} (ha : HasSum g a) (hf : ∀ (b : β), HasSum (fun (c : γ b) => f b, c) (g b)) (hf' : ) :
HasSum f a
theorem HasProd.sigma_of_hasProd {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} {g : βα} {a : α} (ha : HasProd g a) (hf : ∀ (b : β), HasProd (fun (c : γ b) => f b, c) (g b)) (hf' : ) :
theorem tsum_sigma' {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} (h₁ : ∀ (b : β), Summable fun (c : γ b) => f b, c) (h₂ : ) :
∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f b, c
theorem tprod_sigma' {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} (h₁ : ∀ (b : β), Multipliable fun (c : γ b) => f b, c) (h₂ : ) :
∏' (p : (b : β) × γ b), f p = ∏' (b : β) (c : γ b), f b, c
theorem tsum_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : β × γα} (h : ) (h₁ : ∀ (b : β), Summable fun (c : γ) => f (b, c)) :
∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
theorem tprod_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : β × γα} (h : ) (h₁ : ∀ (b : β), Multipliable fun (c : γ) => f (b, c)) :
∏' (p : β × γ), f p = ∏' (b : β) (c : γ), f (b, c)
theorem tsum_comm' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : βγα} (h : ) (h₁ : ∀ (b : β), Summable (f b)) (h₂ : ∀ (c : γ), Summable fun (b : β) => f b c) :
∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
theorem tprod_comm' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : βγα} (h : ) (h₁ : ∀ (b : β), Multipliable (f b)) (h₂ : ∀ (c : γ), Multipliable fun (b : β) => f b c) :
∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c
theorem Summable.sigma_factor {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} (ha : ) (b : β) :
Summable fun (c : γ b) => f b, c
theorem Multipliable.sigma_factor {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} (ha : ) (b : β) :
Multipliable fun (c : γ b) => f b, c
theorem Summable.sigma {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} (ha : ) :
Summable fun (b : β) => ∑' (c : γ b), f b, c
theorem Multipliable.sigma {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} (ha : ) :
Multipliable fun (b : β) => ∏' (c : γ b), f b, c
theorem Summable.prod_factor {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : β × γα} (h : ) (b : β) :
Summable fun (c : γ) => f (b, c)
theorem Multipliable.prod_factor {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : β × γα} (h : ) (b : β) :
Multipliable fun (c : γ) => f (b, c)
theorem HasSum.tsum_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {f : βα} {a : α} (hf : HasSum f a) (g : βγ) :
HasSum (fun (c : γ) => ∑' (b : (g ⁻¹' {c})), f b) a
theorem HasProd.tprod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {f : βα} {a : α} (hf : HasProd f a) (g : βγ) :
HasProd (fun (c : γ) => ∏' (b : (g ⁻¹' {c})), f b) a
theorem tsum_sigma {α : Type u_1} {β : Type u_2} [] [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} (ha : ) :
∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f b, c
theorem tprod_sigma {α : Type u_1} {β : Type u_2} [] [] [] [] [] {γ : βType u_5} {f : (b : β) × γ bα} (ha : ) :
∏' (p : (b : β) × γ b), f p = ∏' (b : β) (c : γ b), f b, c
theorem tsum_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {f : β × γα} (h : ) :
∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
theorem tprod_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {f : β × γα} (h : ) :
∏' (p : β × γ), f p = ∏' (b : β) (c : γ), f (b, c)
theorem tsum_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {f : βγα} (h : ) :
∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
theorem tprod_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {f : βγα} (h : ) :
∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c
theorem Pi.hasSum {α : Type u_1} {ι : Type u_5} {π : αType u_6} [(x : α) → AddCommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] {f : ι(x : α) → π x} {g : (x : α) → π x} :
HasSum f g ∀ (x : α), HasSum (fun (i : ι) => f i x) (g x)
theorem Pi.hasProd {α : Type u_1} {ι : Type u_5} {π : αType u_6} [(x : α) → CommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] {f : ι(x : α) → π x} {g : (x : α) → π x} :
HasProd f g ∀ (x : α), HasProd (fun (i : ι) => f i x) (g x)
theorem Pi.summable {α : Type u_1} {ι : Type u_5} {π : αType u_6} [(x : α) → AddCommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] {f : ι(x : α) → π x} :
∀ (x : α), Summable fun (i : ι) => f i x
theorem Pi.multipliable {α : Type u_1} {ι : Type u_5} {π : αType u_6} [(x : α) → CommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] {f : ι(x : α) → π x} :
∀ (x : α), Multipliable fun (i : ι) => f i x
theorem tsum_apply {α : Type u_1} {ι : Type u_5} {π : αType u_6} [(x : α) → AddCommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] [∀ (x : α), T2Space (π x)] {f : ι(x : α) → π x} {x : α} (hf : ) :
tsum (fun (i : ι) => f i) x = ∑' (i : ι), f i x
theorem tprod_apply {α : Type u_1} {ι : Type u_5} {π : αType u_6} [(x : α) → CommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] [∀ (x : α), T2Space (π x)] {f : ι(x : α) → π x} {x : α} (hf : ) :
tprod (fun (i : ι) => f i) x = ∏' (i : ι), f i x

## Multiplicative opposite #

theorem HasSum.op {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} (hf : HasSum f a) :
HasSum (fun (a : β) => MulOpposite.op (f a)) ()
theorem Summable.op {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) :
Summable (MulOpposite.op f)
theorem HasSum.unop {α : Type u_1} {β : Type u_2} [] [] {f : βαᵐᵒᵖ} {a : αᵐᵒᵖ} (hf : HasSum f a) :
HasSum (fun (a : β) => MulOpposite.unop (f a)) ()
theorem Summable.unop {α : Type u_1} {β : Type u_2} [] [] {f : βαᵐᵒᵖ} (hf : ) :
Summable (MulOpposite.unop f)
@[simp]
theorem hasSum_op {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} :
HasSum (fun (a : β) => MulOpposite.op (f a)) () HasSum f a
@[simp]
theorem hasSum_unop {α : Type u_1} {β : Type u_2} [] [] {f : βαᵐᵒᵖ} {a : αᵐᵒᵖ} :
HasSum (fun (a : β) => MulOpposite.unop (f a)) () HasSum f a
@[simp]
theorem summable_op {α : Type u_1} {β : Type u_2} [] [] {f : βα} :
(Summable fun (a : β) => MulOpposite.op (f a))
@[simp]
theorem summable_unop {α : Type u_1} {β : Type u_2} [] [] {f : βαᵐᵒᵖ} :
(Summable fun (a : β) => MulOpposite.unop (f a))
theorem tsum_op {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] :
∑' (x : β), MulOpposite.op (f x) = MulOpposite.op (∑' (x : β), f x)
theorem tsum_unop {α : Type u_1} {β : Type u_2} [] [] [] {f : βαᵐᵒᵖ} :
∑' (x : β), MulOpposite.unop (f x) = MulOpposite.unop (∑' (x : β), f x)

## Interaction with the star #

theorem HasSum.star {α : Type u_1} {β : Type u_2} [] [] [] [] {f : βα} {a : α} (h : HasSum f a) :
HasSum (fun (b : β) => star (f b)) (star a)
theorem Summable.star {α : Type u_1} {β : Type u_2} [] [] [] [] {f : βα} (hf : ) :
Summable fun (b : β) => star (f b)
theorem Summable.ofStar {α : Type u_1} {β : Type u_2} [] [] [] [] {f : βα} (hf : Summable fun (b : β) => star (f b)) :
@[simp]
theorem summable_star_iff {α : Type u_1} {β : Type u_2} [] [] [] [] {f : βα} :
(Summable fun (b : β) => star (f b))
@[simp]
theorem summable_star_iff' {α : Type u_1} {β : Type u_2} [] [] [] [] {f : βα} :
theorem tsum_star {α : Type u_1} {β : Type u_2} [] [] [] [] {f : βα} [] :
star (∑' (b : β), f b) = ∑' (b : β), star (f b)