Regrouping finitely supported products

Fintype.prod_sum_type splits a product over α ⊕ β into the two partial products, but it needs both index types to be finite. This file records the finprod analogue, which only needs the two restricted families to have finite multiplicative support. Regrouping by the fibers of an arbitrary map is also available, without finiteness assumptions on the fibers.

Main results

• TauCeti.hasFiniteMulSupport_sum_type: a family on α ⊕ β has finite multiplicative support as soon as its two restrictions do.
• TauCeti.finprod_sum_type: ∏ᶠ v : α ⊕ β, f v = (∏ᶠ a, f (.inl a)) * ∏ᶠ b, f (.inr b).
• TauCeti.finprod_fiberwise: regroup a finitely supported product by the fibers of a map.

theorem TauCeti.mulSupport_sum_type {α : Type u_1} {β : Type u_2} {M : Type u_3} [One M] (f : α ⊕ β → M) : Function.mulSupport f = Sum.inl '' Function.mulSupport (f ∘ Sum.inl) ∪ Sum.inr '' Function.mulSupport (f ∘ Sum.inr)

theorem TauCeti.support_sum_type {α : Type u_1} {β : Type u_2} {M : Type u_3} [Zero M] (f : α ⊕ β → M) : Function.support f = Sum.inl '' Function.support (f ∘ Sum.inl) ∪ Sum.inr '' Function.support (f ∘ Sum.inr)

theorem TauCeti.hasFiniteMulSupport_sum_type {α : Type u_1} {β : Type u_2} {M : Type u_3} {f : α ⊕ β → M} [One M] (hl : Function.HasFiniteMulSupport (f ∘ Sum.inl)) (hr : Function.HasFiniteMulSupport (f ∘ Sum.inr)) : Function.HasFiniteMulSupport f

Finite multiplicative support on both summands implies finite multiplicative support on their disjoint union.

theorem TauCeti.hasFiniteSupport_sum_type {α : Type u_1} {β : Type u_2} {M : Type u_3} {f : α ⊕ β → M} [Zero M] (hl : Function.HasFiniteSupport (f ∘ Sum.inl)) (hr : Function.HasFiniteSupport (f ∘ Sum.inr)) : Function.HasFiniteSupport f

theorem TauCeti.finprod_sum_type {α : Type u_1} {β : Type u_2} {M : Type u_3} [CommMonoid M] (f : α ⊕ β → M) (hl : Function.HasFiniteMulSupport (f ∘ Sum.inl)) (hr : Function.HasFiniteMulSupport (f ∘ Sum.inr)) : ∏ᶠ (v : α ⊕ β), f v = (∏ᶠ (a : α), f (Sum.inl a)) * ∏ᶠ (b : β), f (Sum.inr b)

A product over a disjoint union of index types splits as the product of the two partial products, provided both partial families have finite multiplicative support.

theorem TauCeti.finsum_sum_type {α : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] (f : α ⊕ β → M) (hl : Function.HasFiniteSupport (f ∘ Sum.inl)) (hr : Function.HasFiniteSupport (f ∘ Sum.inr)) : ∑ᶠ (v : α ⊕ β), f v = ∑ᶠ (a : α), f (Sum.inl a) + ∑ᶠ (b : β), f (Sum.inr b)

theorem TauCeti.finprod_fiberwise {α : Type u_4} {β : Type u_5} {M : Type u_6} [CommMonoid M] (g : α → β) (f : α → M) (hf : (Function.mulSupport f).Finite) : ∏ᶠ (b : β) (a : { a : α // g a = b }), f ↑a = ∏ᶠ (a : α), f a

Regroup a finitely supported product by the fibers of an arbitrary map. Neither the index sets nor the fibers need be finite.

theorem TauCeti.finsum_fiberwise {α : Type u_4} {β : Type u_5} {M : Type u_6} [AddCommMonoid M] (g : α → β) (f : α → M) (hf : (Function.support f).Finite) : ∑ᶠ (b : β) (a : { a : α // g a = b }), f ↑a = ∑ᶠ (a : α), f a

Regroup a finitely supported sum by the fibers of an arbitrary map. Neither the index sets nor the fibers need be finite.