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 := ⟨default, 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₂} : ⟨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₂.snd → p₁ = p₂

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_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₁.fst → x₀.snd.val = x₁.snd.val → x₀ = 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 : α) × β a → Prop} : (∀ (x : (a : α) × β a), p x) ↔ ∀ (a : α) (b : β a), p ⟨a, b⟩

@[simp]

theorem Sigma.exists {α : Type u_1} {β : α → Type u_4} {p : (a : α) × β a → Prop} : (∃ (x : (a : α) × β a), p x) ↔ ∃ (a : α), ∃ (b : β a), p ⟨a, 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 = ⟨f₁ x.fst, 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₂ ⟨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₁ : 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 ⟨x, 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

theorem Sigma.curry_update {α : Type u_1} {β : α → Type u_4} {γ : (a : α) → β a → Type u_7} [DecidableEq α] [(a : α) → DecidableEq (β a)] (i : (a : α) × β a) (f : (i : (a : α) × β a) → γ i.fst i.snd) (x : γ i.fst i.snd) : Sigma.curry (Function.update f i x) = Function.update (Sigma.curry f) i.fst (Function.update (Sigma.curry f i.fst) i.snd x)

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

Convert a product type to a Σ-type.

Equations

• p.toSigma = ⟨p.fst, 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 : α × β) : 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 : 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 ⟨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 α] [Inhabited (β default)] : Inhabited (PSigma β)

Equations

• PSigma.instInhabitedOfDefault_mathlib = { default := ⟨default, 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₂} : ⟨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₂.snd → p₁ = p₂

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

@[simp]

theorem PSigma.exists {α : Sort u_1} {β : α → Sort u_2} {p : (a : α) ×' β a → Prop} : (∃ (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₁.fst → x₀.snd.val = x₁.snd.val → x₀ = 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⟩