Equivalence between sum types

In this file we continue the work on equivalences begun in Mathlib/Logic/Equiv/Defs.lean, defining

• canonical isomorphisms between various types: e.g.,

  • Equiv.sumEquivSigmaBool is the canonical equivalence between the sum of two types α ⊕ β and the sigma-type Σ b, bif b then β else α;

  • Equiv.prodSumDistrib : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ) shows that type product and type sum satisfy the distributive law up to a canonical equivalence;

More definitions of this kind can be found in other files. E.g., Mathlib/Algebra/Group/TransferInstance.lean does it for Group, Mathlib/Algebra/Module/TransferInstance.lean does it for Module, and similar files exist for other algebraic type classes.

Tags

equivalence, congruence, bijective map

def Equiv.psumEquivSum (α : Type u_9) (β : Type u_10) : α ⊕' β ≃ α ⊕ β

PSum is equivalent to Sum.

def Equiv.sumCongr {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂

If α ≃ α' and β ≃ β', then α ⊕ β ≃ α' ⊕ β'. This is Sum.map as an equivalence.

@[simp]

theorem Equiv.sumCongr_apply {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (a✝ : α₁ ⊕ β₁) : (ea.sumCongr eb) a✝ = Sum.map (⇑ea) (⇑eb) a✝

@[simp]

theorem Equiv.sumCongr_trans {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} {γ₁ : Type u_13} {γ₂ : Type u_14} (e : α₁ ≃ β₁) (f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂) : (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)

@[simp]

theorem Equiv.sumCongr_symm {α : Type u_9} {β : Type u_10} {γ : Type u_11} {δ : Type u_12} (e : α ≃ β) (f : γ ≃ δ) : (e.sumCongr f).symm = e.symm.sumCongr f.symm

@[simp]

theorem Equiv.sumCongr_refl {α : Type u_9} {β : Type u_10} : (Equiv.refl α).sumCongr (Equiv.refl β) = Equiv.refl (α ⊕ β)

def Equiv.psumCongr {α : Sort u_1} {β : Sort u_4} {γ : Sort u_7} {δ : Sort u_8} (e₁ : α ≃ β) (e₂ : γ ≃ δ) : α ⊕' γ ≃ β ⊕' δ

If α ≃ α' and β ≃ β', then α ⊕' β ≃ α' ⊕' β'.

def Equiv.psumSum {α₁ : Sort u_2} {β₁ : Sort u_5} {α₂ : Type u_9} {β₂ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕' β₁ ≃ α₂ ⊕ β₂

Combine two Equivs using PSum in the domain and Sum in the codomain.

def Equiv.sumPSum {α₂ : Sort u_3} {β₂ : Sort u_6} {α₁ : Type u_9} {β₁ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕ β₁ ≃ α₂ ⊕' β₂

Combine two Equivs using Sum in the domain and PSum in the codomain.

def Equiv.subtypeSum {α : Type u_9} {β : Type u_10} {p : α ⊕ β → Prop} : { c : α ⊕ β // p c } ≃ { a : α // p (Sum.inl a) } ⊕ { b : β // p (Sum.inr b) }

A subtype of a sum is equivalent to a sum of subtypes.

@[reducible, inline]

abbrev Equiv.Perm.sumCongr {α : Type u_9} {β : Type u_10} (ea : Perm α) (eb : Perm β) : Perm (α ⊕ β)

Combine a permutation of α and of β into a permutation of α ⊕ β.

@[simp]

theorem Equiv.Perm.sumCongr_apply {α : Type u_9} {β : Type u_10} (ea : Perm α) (eb : Perm β) (x : α ⊕ β) : (ea.sumCongr eb) x = Sum.map (⇑ea) (⇑eb) x

theorem Equiv.Perm.sumCongr_trans {α : Type u_9} {β : Type u_10} (e : Perm α) (f : Perm β) (g : Perm α) (h : Perm β) : Equiv.trans (e.sumCongr f) (g.sumCongr h) = sumCongr (Equiv.trans e g) (Equiv.trans f h)

theorem Equiv.Perm.sumCongr_symm {α : Type u_9} {β : Type u_10} (e : Perm α) (f : Perm β) : Equiv.symm (e.sumCongr f) = sumCongr (Equiv.symm e) (Equiv.symm f)

theorem Equiv.Perm.sumCongr_refl {α : Type u_9} {β : Type u_10} : sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)

def Equiv.boolEquivPUnitSumPUnit : Bool ≃ PUnit ⊕ PUnit

Bool is equivalent the sum of two PUnits.

def Equiv.sumComm (α : Type u_9) (β : Type u_10) : α ⊕ β ≃ β ⊕ α

Sum of types is commutative up to an equivalence. This is Sum.swap as an equivalence.

@[simp]

theorem Equiv.sumComm_apply (α : Type u_9) (β : Type u_10) : ⇑(sumComm α β) = Sum.swap

@[simp]

theorem Equiv.sumComm_symm (α : Type u_9) (β : Type u_10) : (sumComm α β).symm = sumComm β α

def Equiv.sumAssoc (α : Type u_9) (β : Type u_10) (γ : Type u_11) : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ

Sum of types is associative up to an equivalence.

@[simp]

theorem Equiv.sumAssoc_apply_inl_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) : (sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a

@[simp]

theorem Equiv.sumAssoc_apply_inl_inr {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β) : (sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)

@[simp]

theorem Equiv.sumAssoc_apply_inr {α : Type u_9} {β : Type u_10} {γ : Type u_11} (c : γ) : (sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)

@[simp]

theorem Equiv.sumAssoc_symm_apply_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) : (sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)

@[simp]

theorem Equiv.sumAssoc_symm_apply_inr_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β) : (sumAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)

@[simp]

theorem Equiv.sumAssoc_symm_apply_inr_inr {α : Type u_9} {β : Type u_10} {γ : Type u_11} (c : γ) : (sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c

def Equiv.sumSumSumComm (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) : (α ⊕ β) ⊕ γ ⊕ δ ≃ (α ⊕ γ) ⊕ β ⊕ δ

Four-way commutativity of sum. The name matches add_add_add_comm.

@[simp]

theorem Equiv.sumSumSumComm_apply (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) (a✝ : (α ⊕ β) ⊕ γ ⊕ δ) : (sumSumSumComm α β γ δ) a✝ = (⇑(sumAssoc (α ⊕ γ) β δ) ∘ Sum.map (⇑(sumAssoc α γ β).symm) id ∘ Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm) a✝

@[simp]

theorem Equiv.sumSumSumComm_symm (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) : (sumSumSumComm α β γ δ).symm = sumSumSumComm α γ β δ

def Equiv.sumEmpty (α : Type u_9) (β : Type u_10) [IsEmpty β] : α ⊕ β ≃ α

Sum with IsEmpty is equivalent to the original type.

@[simp]

theorem Equiv.sumEmpty_symm_apply (α : Type u_9) (β : Type u_10) [IsEmpty β] (val : α) : (sumEmpty α β).symm val = Sum.inl val

@[simp]

theorem Equiv.sumEmpty_apply_inl {α : Type u_9} {β : Type u_10} [IsEmpty β] (a : α) : (sumEmpty α β) (Sum.inl a) = a

def Equiv.emptySum (α : Type u_9) (β : Type u_10) [IsEmpty α] : α ⊕ β ≃ β

The sum of IsEmpty with any type is equivalent to that type.

@[simp]

theorem Equiv.emptySum_symm_apply (α : Type u_9) (β : Type u_10) [IsEmpty α] (a✝ : β) : (emptySum α β).symm a✝ = Sum.inr a✝

@[simp]

theorem Equiv.emptySum_apply_inr {α : Type u_9} {β : Type u_10} [IsEmpty α] (b : β) : (emptySum α β) (Sum.inr b) = b

def Equiv.sumEquivSigmaBool (α β : Type u_9) : α ⊕ β ≃ (b : Bool) × bif b then β else α

α ⊕ β is equivalent to a Sigma-type over Bool. Note that this definition assumes α and β to be types from the same universe, so it cannot be used directly to transfer theorems about sigma types to theorems about sum types. In many cases one can use ULift to work around this difficulty.

def Equiv.sigmaFiberEquiv {α : Type u_9} {β : Type u_10} (f : α → β) : (y : β) × { x : α // f x = y } ≃ α

sigmaFiberEquiv f for f : α → β is the natural equivalence between the type of all fibres of f and the total space α.

@[simp]

theorem Equiv.sigmaFiberEquiv_symm_apply_fst {α : Type u_9} {β : Type u_10} (f : α → β) (x : α) : ((sigmaFiberEquiv f).symm x).fst = f x

@[simp]

theorem Equiv.sigmaFiberEquiv_apply {α : Type u_9} {β : Type u_10} (f : α → β) (x : (y : β) × { x : α // f x = y }) : (sigmaFiberEquiv f) x = ↑x.snd

@[simp]

theorem Equiv.sigmaFiberEquiv_symm_apply_snd_coe {α : Type u_9} {β : Type u_10} (f : α → β) (x : α) : ↑((sigmaFiberEquiv f).symm x).snd = x

def Equiv.sigmaEquivOptionOfInhabited (α : Type u) [Inhabited α] [DecidableEq α] : (β : Type u) × (α ≃ Option β)

Inhabited types are equivalent to Option β for some β by identifying default with none.

def Equiv.sumCompl {α : Type u_9} (p : α → Prop) [DecidablePred p] : { a : α // p a } ⊕ { a : α // ¬p a } ≃ α

For any predicate p on α, the sum of the two subtypes {a // p a} and its complement {a // ¬ p a} is naturally equivalent to α.

See subtypeOrEquiv for sum types over subtypes {x // p x} and {x // q x} that are not necessarily IsCompl p q. See also Equiv.Set.sumCompl for a version on sets.

@[simp]

theorem Equiv.sumCompl_apply_inl {α : Type u_9} {p : α → Prop} [DecidablePred p] (x : { a : α // p a }) : (sumCompl p) (Sum.inl x) = ↑x

@[simp]

theorem Equiv.sumCompl_apply_inr {α : Type u_9} {p : α → Prop} [DecidablePred p] (x : { a : α // ¬p a }) : (sumCompl p) (Sum.inr x) = ↑x

@[simp]

theorem Equiv.sumCompl_symm_apply_of_pos {α : Type u_9} {p : α → Prop} [DecidablePred p] {a : α} (h : p a) : (sumCompl p).symm a = Sum.inl ⟨a, h⟩

@[simp]

theorem Equiv.sumCompl_symm_apply_of_neg {α : Type u_9} {p : α → Prop} [DecidablePred p] {a : α} (h : ¬p a) : (sumCompl p).symm a = Sum.inr ⟨a, h⟩

@[deprecated Equiv.sumCompl_symm_apply_of_pos (since := "2025-10-28")]

theorem Equiv.sumCompl_apply_symm_of_pos {α : Type u_9} {p : α → Prop} [DecidablePred p] {a : α} (h : p a) : (sumCompl p).symm a = Sum.inl ⟨a, h⟩

Alias of Equiv.sumCompl_symm_apply_of_pos.

@[deprecated Equiv.sumCompl_symm_apply_of_neg (since := "2025-10-28")]

theorem Equiv.sumCompl_apply_symm_of_neg {α : Type u_9} {p : α → Prop} [DecidablePred p] {a : α} (h : ¬p a) : (sumCompl p).symm a = Sum.inr ⟨a, h⟩

Alias of Equiv.sumCompl_symm_apply_of_neg.

@[simp]

theorem Equiv.sumCompl_symm_apply_pos {α : Type u_9} {p : α → Prop} [DecidablePred p] (x : { x : α // p x }) : (sumCompl p).symm ↑x = Sum.inl x

@[simp]

theorem Equiv.sumCompl_symm_apply_neg {α : Type u_9} {p : α → Prop} [DecidablePred p] (x : { x : α // ¬p x }) : (sumCompl p).symm ↑x = Sum.inr x

def Equiv.prodSumDistrib (α : Type u_9) (β : Type u_10) (γ : Type u_11) : α × (β ⊕ γ) ≃ α × β ⊕ α × γ

Type product is left distributive with respect to type sum up to an equivalence.

@[simp]

theorem Equiv.prodSumDistrib_apply_left {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) (b : β) : (prodSumDistrib α β γ) (a, Sum.inl b) = Sum.inl (a, b)

@[simp]

theorem Equiv.prodSumDistrib_apply_right {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) (c : γ) : (prodSumDistrib α β γ) (a, Sum.inr c) = Sum.inr (a, c)

@[simp]

theorem Equiv.prodSumDistrib_symm_apply_left {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α × β) : (prodSumDistrib α β γ).symm (Sum.inl a) = (a.fst, Sum.inl a.snd)

@[simp]

theorem Equiv.prodSumDistrib_symm_apply_right {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α × γ) : (prodSumDistrib α β γ).symm (Sum.inr a) = (a.fst, Sum.inr a.snd)

def Equiv.sigmaSumDistrib {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) : (i : ι) × (α i ⊕ β i) ≃ (i : ι) × α i ⊕ (i : ι) × β i

An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums. Compare with Equiv.sumSigmaDistrib which is indexed by sums.

@[simp]

theorem Equiv.sigmaSumDistrib_apply {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) (p : (i : ι) × (α i ⊕ β i)) : (sigmaSumDistrib α β) p = Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd

@[simp]

theorem Equiv.sigmaSumDistrib_symm_apply {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) (a✝ : (i : ι) × α i ⊕ (i : ι) × β i) : (sigmaSumDistrib α β).symm a✝ = Sum.elim (Sigma.map id fun (x : ι) => Sum.inl) (Sigma.map id fun (x : ι) => Sum.inr) a✝

def Equiv.sumSigmaDistrib {α : Type u_10} {β : Type u_11} (t : α ⊕ β → Type u_9) : (i : α ⊕ β) × t i ≃ (i : α) × t (Sum.inl i) ⊕ (i : β) × t (Sum.inr i)

A type indexed by disjoint sums of types is equivalent to the sum of the sums. Compare with Equiv.sigmaSumDistrib which has the sums as the output type.

@[simp]

theorem Equiv.sumSigmaDistrib_apply {α : Type u_10} {β : Type u_11} (t : α ⊕ β → Type u_9) (x✝ : (i : α ⊕ β) × t i) : (sumSigmaDistrib t) x✝ = match x✝ with | ⟨Sum.inl x, y⟩ => Sum.inl ⟨x, y⟩ | ⟨Sum.inr x, y⟩ => Sum.inr ⟨x, y⟩

@[simp]

theorem Equiv.sumSigmaDistrib_symm_apply {α : Type u_10} {β : Type u_11} (t : α ⊕ β → Type u_9) (a✝ : (i : α) × t (Sum.inl i) ⊕ (i : β) × t (Sum.inr i)) : (sumSigmaDistrib t).symm a✝ = Sum.elim (fun (a : (i : α) × t (Sum.inl i)) => ⟨Sum.inl a.fst, a.snd⟩) (fun (b : (i : β) × t (Sum.inr i)) => ⟨Sum.inr b.fst, b.snd⟩) a✝