# Sigma types #

This file proves basic results about sigma types.

A sigma type is a dependent pair type. Like α × β but where the type of the second component depends on the first component. More precisely, given β : ι → Type*, Sigma β is made of stuff which is of type β i for some i : ι, so the sigma type is a disjoint union of types. For example, the sum type X ⊕ Y can be emulated using a sigma type, by taking ι with exactly two elements (see Equiv.sumEquivSigmaBool).

Σ x, A x is notation for Sigma A (note that this is \Sigma, not the sum operator ∑). Σ x y z ..., A x y z ... is notation for Σ x, Σ y, Σ z, ..., A x y z .... Here we have α : Type*, β : α → Type*, γ : Π a : α, β a → Type*, ..., A : Π (a : α) (b : β a) (c : γ a b) ..., Type* with x : α y : β x, z : γ x y, ...

## Notes #

The definition of Sigma takes values in Type*. This effectively forbids Prop- valued sigma types. To that effect, we have PSigma, which takes value in Sort* and carries a more complicated universe signature as a consequence.

instance Sigma.instInhabitedSigma {α : Type u_1} {β : αType u_4} [] [Inhabited (β default)] :
Equations
• Sigma.instInhabitedSigma = { default := default, default }
instance Sigma.instDecidableEqSigma {α : Type u_1} {β : αType u_4} [h₁ : ] [h₂ : (a : α) → DecidableEq (β a)] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Sigma.mk.inj_iff {α : Type u_1} {β : αType u_4} {a₁ : α} {a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
a₁, b₁ = a₂, b₂ a₁ = a₂ HEq b₁ b₂
@[simp]
theorem Sigma.eta {α : Type u_1} {β : αType u_4} (x : (a : α) × β a) :
x.fst, x.snd = x
theorem Sigma.eq {α : Type u_7} {β : αType u_8} {p₁ : (a : α) × β a} {p₂ : (a : α) × β a} (h₁ : p₁.fst = p₂.fst) :
Eq.recOn h₁ p₁.snd = p₂.sndp₁ = p₂
theorem Function.eq_of_sigmaMk_comp {α : Type u_1} {β : αType u_4} {γ : Type u_7} [] {a : α} {b : α} {f : γβ a} {g : γβ b} (h : f = g) :
a = b HEq f g

A version of Iff.mp Sigma.ext_iff for functions from a nonempty type to a sigma type.

theorem Sigma.subtype_ext_iff {α : Type u_1} {β : Type u_7} {p : αβProp} {x₀ : (a : α) × Subtype (p a)} {x₁ : (a : α) × Subtype (p a)} :
x₀ = x₁ x₀.fst = x₁.fst x₀.snd.val = x₁.snd.val
theorem Sigma.subtype_ext {α : Type u_1} {β : Type u_7} {p : αβProp} {x₀ : (a : α) × Subtype (p a)} {x₁ : (a : α) × Subtype (p a)} :
x₀.fst = x₁.fstx₀.snd.val = x₁.snd.valx₀ = x₁

A specialized ext lemma for equality of sigma types over an indexed subtype.

theorem Sigma.forall {α : Type u_1} {β : αType u_4} {p : (a : α) × β aProp} :
(∀ (x : (a : α) × β a), p x) ∀ (a : α) (b : β a), p a, b
@[simp]
theorem Sigma.exists {α : Type u_1} {β : αType u_4} {p : (a : α) × β aProp} :
(∃ (x : (a : α) × β a), p x) ∃ (a : α), ∃ (b : β a), p a, b
theorem Sigma.exists' {α : Type u_1} {β : αType u_4} {p : (a : α) → β aProp} :
(∃ (a : α), ∃ (b : β a), p a b) ∃ (x : (a : α) × β a), p x.fst x.snd
theorem Sigma.forall' {α : Type u_1} {β : αType u_4} {p : (a : α) → β aProp} :
(∀ (a : α) (b : β a), p a b) ∀ (x : (a : α) × β a), p x.fst x.snd
theorem sigma_mk_injective {α : Type u_1} {β : αType u_4} {i : α} :
theorem Sigma.fst_surjective {α : Type u_1} {β : αType u_4} [h : ∀ (a : α), Nonempty (β a)] :
theorem Sigma.fst_surjective_iff {α : Type u_1} {β : αType u_4} :
Function.Surjective Sigma.fst ∀ (a : α), Nonempty (β a)
theorem Sigma.fst_injective {α : Type u_1} {β : αType u_4} [h : ∀ (a : α), Subsingleton (β a)] :
theorem Sigma.fst_injective_iff {α : Type u_1} {β : αType u_4} :
Function.Injective Sigma.fst ∀ (a : α), Subsingleton (β a)
def Sigma.map {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁Type u_5} {β₂ : α₂Type u_6} (f₁ : α₁α₂) (f₂ : (a : α₁) → β₁ aβ₂ (f₁ a)) (x : Sigma β₁) :
Sigma β₂

Map the left and right components of a sigma

Equations
• Sigma.map f₁ f₂ x = f₁ x.fst, f₂ x.fst x.snd
Instances For
theorem Sigma.map_mk {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁Type u_5} {β₂ : α₂Type u_6} (f₁ : α₁α₂) (f₂ : (a : α₁) → β₁ aβ₂ (f₁ a)) (x : α₁) (y : β₁ x) :
Sigma.map f₁ f₂ x, y = f₁ x, f₂ x y
theorem Function.Injective.sigma_map {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁Type u_5} {β₂ : α₂Type u_6} {f₁ : α₁α₂} {f₂ : (a : α₁) → β₁ aβ₂ (f₁ a)} (h₁ : ) (h₂ : ∀ (a : α₁), Function.Injective (f₂ a)) :
theorem Function.Injective.of_sigma_map {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁Type u_5} {β₂ : α₂Type u_6} {f₁ : α₁α₂} {f₂ : (a : α₁) → β₁ aβ₂ (f₁ a)} (h : Function.Injective (Sigma.map f₁ f₂)) (a : α₁) :
theorem Function.Injective.sigma_map_iff {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁Type u_5} {β₂ : α₂Type u_6} {f₁ : α₁α₂} {f₂ : (a : α₁) → β₁ aβ₂ (f₁ a)} (h₁ : ) :
Function.Injective (Sigma.map f₁ f₂) ∀ (a : α₁), Function.Injective (f₂ a)
theorem Function.Surjective.sigma_map {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁Type u_5} {β₂ : α₂Type u_6} {f₁ : α₁α₂} {f₂ : (a : α₁) → β₁ aβ₂ (f₁ a)} (h₁ : ) (h₂ : ∀ (a : α₁), Function.Surjective (f₂ a)) :
def Sigma.curry {α : Type u_1} {β : αType u_4} {γ : (a : α) → β aType u_7} (f : (x : ) → γ x.fst x.snd) (x : α) (y : β x) :
γ x y

Interpret a function on Σ x : α, β x as a dependent function with two arguments.

This also exists as an Equiv as Equiv.piCurry γ.

Equations
Instances For
def Sigma.uncurry {α : Type u_1} {β : αType u_4} {γ : (a : α) → β aType u_7} (f : (x : α) → (y : β x) → γ x y) (x : ) :
γ x.fst x.snd

Interpret a dependent function with two arguments as a function on Σ x : α, β x.

This also exists as an Equiv as (Equiv.piCurry γ).symm.

Equations
• = f x.fst x.snd
Instances For
@[simp]
theorem Sigma.uncurry_curry {α : Type u_1} {β : αType u_4} {γ : (a : α) → β aType u_7} (f : (x : ) → γ x.fst x.snd) :
@[simp]
theorem Sigma.curry_uncurry {α : Type u_1} {β : αType u_4} {γ : (a : α) → β aType u_7} (f : (x : α) → (y : β x) → γ x y) :
theorem Sigma.curry_update {α : Type u_1} {β : αType u_4} {γ : (a : α) → β aType u_7} [] [(a : α) → DecidableEq (β a)] (i : (a : α) × β a) (f : (i : (a : α) × β a) → γ i.fst i.snd) (x : γ i.fst i.snd) :
def Prod.toSigma {α : Type u_7} {β : Type u_8} (p : α × β) :
(_ : α) × β

Convert a product type to a Σ-type.

Equations
• p.toSigma = p.fst, p.snd
Instances For
@[simp]
theorem Prod.fst_comp_toSigma {α : Type u_7} {β : Type u_8} :
Sigma.fst Prod.toSigma = Prod.fst
@[simp]
theorem Prod.fst_toSigma {α : Type u_7} {β : Type u_8} (x : α × β) :
x.toSigma.fst = x.fst
@[simp]
theorem Prod.snd_toSigma {α : Type u_7} {β : Type u_8} (x : α × β) :
x.toSigma.snd = x.snd
@[simp]
theorem Prod.toSigma_mk {α : Type u_7} {β : Type u_8} (x : α) (y : β) :
(x, y).toSigma = x, y
def PSigma.elim {α : Sort u_1} {β : αSort u_2} {γ : Sort u_3} (f : (a : α) → β aγ) (a : ) :
γ

Nondependent eliminator for PSigma.

Equations
Instances For
@[simp]
theorem PSigma.elim_val {α : Sort u_1} {β : αSort u_2} {γ : Sort u_3} (f : (a : α) → β aγ) (a : α) (b : β a) :
PSigma.elim f a, b = f a b
@[deprecated ex_of_PSigma]
theorem PSigma.ex_of_psig {α : Type u} {p : αProp} :
(x : α) ×' p x∃ (x : α), p x

Alias of ex_of_PSigma.

instance PSigma.instInhabitedOfDefault_mathlib {α : Sort u_1} {β : αSort u_2} [] [Inhabited (β default)] :
Equations
• PSigma.instInhabitedOfDefault_mathlib = { default := default, default }
instance PSigma.decidableEq {α : Sort u_1} {β : αSort u_2} [h₁ : ] [h₂ : (a : α) → DecidableEq (β a)] :
Equations
• One or more equations did not get rendered due to their size.
theorem PSigma.mk.inj_iff {α : Sort u_1} {β : αSort u_2} {a₁ : α} {a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
a₁, b₁ = a₂, b₂ a₁ = a₂ HEq b₁ b₂
@[deprecated PSigma.ext_iff]
theorem PSigma.eq {α : Sort u_3} {β : αSort u_4} {p₁ : (a : α) ×' β a} {p₂ : (a : α) ×' β a} (h₁ : p₁.fst = p₂.fst) :
Eq.recOn h₁ p₁.snd = p₂.sndp₁ = p₂
theorem PSigma.forall {α : Sort u_1} {β : αSort u_2} {p : (a : α) ×' β aProp} :
(∀ (x : (a : α) ×' β a), p x) ∀ (a : α) (b : β a), p a, b
@[simp]
theorem PSigma.exists {α : Sort u_1} {β : αSort u_2} {p : (a : α) ×' β aProp} :
(∃ (x : (a : α) ×' β a), p x) ∃ (a : α), ∃ (b : β a), p a, b
theorem PSigma.subtype_ext_iff {α : Sort u_1} {β : Sort u_3} {p : αβProp} {x₀ : (a : α) ×' Subtype (p a)} {x₁ : (a : α) ×' Subtype (p a)} :
x₀ = x₁ x₀.fst = x₁.fst x₀.snd.val = x₁.snd.val
theorem PSigma.subtype_ext {α : Sort u_1} {β : Sort u_3} {p : αβProp} {x₀ : (a : α) ×' Subtype (p a)} {x₁ : (a : α) ×' Subtype (p a)} :
x₀.fst = x₁.fstx₀.snd.val = x₁.snd.valx₀ = x₁

A specialized ext lemma for equality of PSigma types over an indexed subtype.

def PSigma.map {α₁ : Sort u_3} {α₂ : Sort u_4} {β₁ : α₁Sort u_5} {β₂ : α₂Sort u_6} (f₁ : α₁α₂) (f₂ : (a : α₁) → β₁ aβ₂ (f₁ a)) :
PSigma β₁PSigma β₂

Map the left and right components of a sigma

Equations
• PSigma.map f₁ f₂ a, b = f₁ a, f₂ a b
Instances For