Images and erasures of finite sets on sum types

These identities compute the image of a disjoint sum, the two projections of an image under Sum.map, and the projections after erasing an element of the left summand. They are used to calculate joins of simplicial complexes factor by factor.

Main results

• Finset.image_sumMap_disjSum: mapping the summands commutes with disjoint union.
• Finset.toLeft_image_sumMap and Finset.toRight_image_sumMap: projections of an image under Sum.map.
• Finset.toLeft_erase_inl and Finset.toRight_erase_inl: projections after erasing a left-tagged element.

@[simp]

theorem Finset.image_sumMap_disjSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [DecidableEq γ] [DecidableEq δ] (s : Finset α) (t : Finset β) (f : α → γ) (g : β → δ) : image (Sum.map f g) (s.disjSum t) = (image f s).disjSum (image g t)

Mapping the two summands commutes with disjoint union.

@[simp]

theorem Finset.toLeft_image_sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [DecidableEq γ] [DecidableEq δ] (s : Finset (α ⊕ β)) (f : α → γ) (g : β → δ) : (image (Sum.map f g) s).toLeft = image f s.toLeft

The left projection of the image under a map of summands.

@[simp]

theorem Finset.toRight_image_sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [DecidableEq γ] [DecidableEq δ] (s : Finset (α ⊕ β)) (f : α → γ) (g : β → δ) : (image (Sum.map f g) s).toRight = image g s.toRight

The right projection of the image under a map of summands.

@[simp]

theorem Finset.toLeft_erase_inl {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (s : Finset (α ⊕ β)) (a : α) : (s.erase (Sum.inl a)).toLeft = s.toLeft.erase a

Erasing a left-tagged element erases it from the left projection.

@[simp]

theorem Finset.toRight_erase_inl {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (s : Finset (α ⊕ β)) (a : α) : (s.erase (Sum.inl a)).toRight = s.toRight

Erasing a left-tagged element leaves the right projection unchanged.