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 α] [Inhabited (β default)] : Inhabited (Sigma β)

Equations

• Sigma.instInhabitedSigma = { default := { fst := default, snd := default } }

instance Sigma.instDecidableEqSigma {α : Type u_1} {β : α → Type u_4} [h₁ : DecidableEq α] [h₂ : (a : α) → DecidableEq (β a)] : DecidableEq (Sigma β)

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₂} : { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ } ↔ a₁ = a₂ ∧ HEq b₁ b₂

@[simp]

theorem Sigma.eta {α : Type u_1} {β : α → Type u_4} (x : (a : α) × β a) : { fst := x.fst, snd := x.snd } = x

theorem Sigma.ext_iff {α : Type u_1} {β : α → Type u_4} {x₀ : Sigma β} {x₁ : Sigma β} : x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ HEq x₀.snd x₁.snd

theorem Function.eq_of_sigmaMk_comp {α : Type u_1} {β : α → Type u_4} {γ : Type u_7} [Nonempty γ] {a : α} {b : α} {f : γ → β a} {g : γ → β b} (h : Sigma.mk a ∘ f = Sigma.mk b ∘ 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 {α : Type u_1} {β : Type u_7} {p : α → β → Prop} {x₀ : (a : α) × Subtype (p a)} {x₁ : (a : α) × Subtype (p a)} : x₀.fst = x₁.fst → x₀.snd.val = x₁.snd.val → x₀ = x₁

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

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

@[simp]

theorem Sigma.forall {α : Type u_1} {β : α → Type u_4} {p : (a : α) × β a → Prop} : (∀ (x : (a : α) × β a), p x) ↔ ∀ (a : α) (b : β a), p { fst := a, snd := b }

@[simp]

theorem Sigma.exists {α : Type u_1} {β : α → Type u_4} {p : (a : α) × β a → Prop} : (∃ (x : (a : α) × β a), p x) ↔ ∃ (a : α), ∃ (b : β a), p { fst := a, snd := b }

theorem Sigma.exists' {α : Type u_1} {β : α → Type u_4} {p : (a : α) → β a → Prop} : (∃ (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 : α) → β a → Prop} : (∀ (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 : α} : Function.Injective (Sigma.mk i)

theorem Sigma.fst_surjective {α : Type u_1} {β : α → Type u_4} [h : ∀ (a : α), Nonempty (β a)] : Function.Surjective Sigma.fst

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)] : Function.Injective Sigma.fst

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 = { fst := f₁ x.fst, snd := f₂ x.fst x.snd }

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₂ { fst := x, snd := y } = { fst := f₁ x, snd := 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₁ : Function.Injective f₁) (h₂ : ∀ (a : α₁), Function.Injective (f₂ a)) : Function.Injective (Sigma.map f₁ f₂)

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 : α₁) : Function.Injective (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 f₁) : 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₁ : Function.Surjective f₁) (h₂ : ∀ (a : α₁), Function.Surjective (f₂ a)) : Function.Surjective (Sigma.map f₁ f₂)

def Sigma.curry {α : Type u_1} {β : α → Type u_4} {γ : (a : α) → β a → Type u_7} (f : (x : Sigma β) → γ 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

• Sigma.curry f x y = f { fst := x, snd := y }

def Sigma.uncurry {α : Type u_1} {β : α → Type u_4} {γ : (a : α) → β a → Type u_7} (f : (x : α) → (y : β x) → γ x y) (x : Sigma β) : γ 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

• Sigma.uncurry f x = f x.fst x.snd

@[simp]

theorem Sigma.uncurry_curry {α : Type u_1} {β : α → Type u_4} {γ : (a : α) → β a → Type u_7} (f : (x : Sigma β) → γ x.fst x.snd) : Sigma.uncurry (Sigma.curry f) = f

@[simp]

theorem Sigma.curry_uncurry {α : Type u_1} {β : α → Type u_4} {γ : (a : α) → β a → Type u_7} (f : (x : α) → (y : β x) → γ x y) : Sigma.curry (Sigma.uncurry f) = f

def Prod.toSigma {α : Type u_7} {β : Type u_8} (p : α × β) : (_ : α) × β

Convert a product type to a Σ-type.

Equations

• Prod.toSigma p = { fst := p.fst, snd := p.snd }

@[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 : α × β) : (Prod.toSigma x).fst = x.fst

@[simp]

theorem Prod.snd_toSigma {α : Type u_7} {β : Type u_8} (x : α × β) : (Prod.toSigma x).snd = x.snd

@[simp]

theorem Prod.toSigma_mk {α : Type u_7} {β : Type u_8} (x : α) (y : β) : Prod.toSigma (x, y) = { fst := x, snd := y }

def PSigma.elim {α : Sort u_1} {β : α → Sort u_2} {γ : Sort u_3} (f : (a : α) → β a → γ) (a : PSigma β) : γ

Nondependent eliminator for PSigma.

Equations

• PSigma.elim f a = PSigma.casesOn a f

@[simp]

theorem PSigma.elim_val {α : Sort u_1} {β : α → Sort u_2} {γ : Sort u_3} (f : (a : α) → β a → γ) (a : α) (b : β a) : PSigma.elim f { fst := a, snd := b } = f a b

instance PSigma.instInhabitedPSigma {α : Sort u_1} {β : α → Sort u_2} [Inhabited α] [Inhabited (β default)] : Inhabited (PSigma β)

Equations

• PSigma.instInhabitedPSigma = { default := { fst := default, snd := default } }

instance PSigma.decidableEq {α : Sort u_1} {β : α → Sort u_2} [h₁ : DecidableEq α] [h₂ : (a : α) → DecidableEq (β a)] : DecidableEq (PSigma β)

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₂} : { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ } ↔ a₁ = a₂ ∧ HEq b₁ b₂

theorem PSigma.ext_iff {α : Sort u_1} {β : α → Sort u_2} {x₀ : PSigma β} {x₁ : PSigma β} : x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ HEq x₀.snd x₁.snd

@[simp]

theorem PSigma.forall {α : Sort u_1} {β : α → Sort u_2} {p : (a : α) ×' β a → Prop} : (∀ (x : (a : α) ×' β a), p x) ↔ ∀ (a : α) (b : β a), p { fst := a, snd := b }

@[simp]

theorem PSigma.exists {α : Sort u_1} {β : α → Sort u_2} {p : (a : α) ×' β a → Prop} : (∃ (x : (a : α) ×' β a), p x) ↔ ∃ (a : α), ∃ (b : β a), p { fst := a, snd := b }

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₁.fst → x₀.snd.val = x₁.snd.val → x₀ = x₁

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

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

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₂ x = match x with | { fst := a, snd := b } => { fst := f₁ a, snd := f₂ a b }