data.sigma.basic

# Sigma types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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. This can be seen as a generalization of the sum type α ⊕ β:

• α ⊕ β is made of stuff which is either of type α or β.
• Given α : ι → Type*, sigma α is made of stuff which is of type α i for some i : ι. One effectively recovers a type isomorphic to α ⊕ β by taking a ι with exactly two elements. See equiv.sum_equiv_sigma_bool.

Σ x, A x is notation for sigma A (note the difference with the big 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 in consequence.

@[protected, instance]
def sigma.inhabited {α : Type u_1} {β : α Type u_4} [inhabited α]  :
Equations
@[protected, instance]
def sigma.decidable_eq {α : Type u_1} {β : α Type u_4} [h₁ : decidable_eq α] [h₂ : Π (a : α), decidable_eq (β a)] :
Equations
• sigma.decidable_eq a₁, b₁⟩ a₂, b₂⟩ = sigma.decidable_eq._match_1 a₁ b₁ a₂ b₂ (h₁ a₁ a₂)
• sigma.decidable_eq._match_1 a b₁ a b₂ = sigma.decidable_eq._match_2 a b₁ b₂ (h₂ a b₁ b₂)
• sigma.decidable_eq._match_1 a₁ _x a₂ _x_1 =
• sigma.decidable_eq._match_2 a b b =
• sigma.decidable_eq._match_2 a b₁ b₂ =
@[simp, nolint]
theorem sigma.mk.inj_iff {α : Type u_1} {β : α Type u_4} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
a₁, b₁⟩ = a₂, b₂⟩ a₁ = a₂ b₁ == b₂
@[simp]
theorem sigma.eta {α : Type u_1} {β : α Type u_4} (x : Σ (a : α), β a) :
x.fst, x.snd = x
@[ext]
theorem sigma.ext {α : Type u_1} {β : α Type u_4} {x₀ x₁ : sigma β} (h₀ : x₀.fst = x₁.fst) (h₁ : x₀.snd == x₁.snd) :
x₀ = x₁
theorem sigma.ext_iff {α : Type u_1} {β : α Type u_4} {x₀ x₁ : sigma β} :
x₀ = x₁ x₀.fst = x₁.fst x₀.snd == x₁.snd
@[ext]
theorem sigma.subtype_ext {α : Type u_1} {β : Type u_2} {p : α β Prop} {x₀ x₁ : Σ (a : α), subtype (p a)} :
x₀.fst = x₁.fst (x₀.snd) = (x₁.snd) 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_2} {p : α β Prop} {x₀ x₁ : Σ (a : α), subtype (p a)} :
x₀ = x₁ x₀.fst = x₁.fst (x₀.snd) = (x₁.snd)
@[simp]
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⟩
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
theorem sigma_mk_injective {α : Type u_1} {β : α Type u_4} {i : α} :
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)) :
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 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)) :
def sigma.curry {α : Type u_1} {β : α Type u_4} {γ : Π (a : α), β a Type u_2} (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.Pi_curry γ.

Equations
• x y = f x, y⟩
def sigma.uncurry {α : Type u_1} {β : α Type u_4} {γ : Π (a : α), β a Type u_2} (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.Pi_curry γ).symm.

Equations
@[simp]
theorem sigma.uncurry_curry {α : Type u_1} {β : α Type u_4} {γ : Π (a : α), β a Type u_2} (f : Π (x : sigma β), γ x.fst x.snd) :
@[simp]
theorem sigma.curry_uncurry {α : Type u_1} {β : α Type u_4} {γ : Π (a : α), β a Type u_2} (f : Π (x : α) (y : β x), γ x y) :
def prod.to_sigma {α : Type u_1} {β : Type u_2} (p : α × β) :
Σ (_x : α), β

Convert a product type to a Σ-type.

Equations
@[simp]
theorem prod.fst_comp_to_sigma {α : Type u_1} {β : Type u_2} :
@[simp]
theorem prod.fst_to_sigma {α : Type u_1} {β : Type u_2} (x : α × β) :
@[simp]
theorem prod.snd_to_sigma {α : Type u_1} {β : Type u_2} (x : α × β) :
@[simp]
theorem prod.to_sigma_mk {α : Type u_1} {β : Type u_2} (x : α) (y : β) :
(x, y).to_sigma = x, y⟩
@[protected, instance]
meta def sigma.reflect {α : Type u} (β : α Type v) [reflected (Type u) α] [reflected Type v) β] [hα : has_reflect α] [hβ : Π (i : α), has_reflect (β i)] :
has_reflect (Σ (a : α), β a)
def psigma.elim {α : Sort u_1} {β : α Sort u_2} {γ : Sort u_3} (f : Π (a : α), β a γ) (a : psigma β) :
γ

Nondependent eliminator for psigma.

Equations
• a = a.cases_on f
@[simp]
theorem psigma.elim_val {α : Sort u_1} {β : α Sort u_2} {γ : Sort u_3} (f : Π (a : α), β a γ) (a : α) (b : β a) :
a, b⟩ = f a b
@[protected, instance]
def psigma.inhabited {α : Sort u_1} {β : α Sort u_2} [inhabited α]  :
Equations
@[protected, instance]
def psigma.decidable_eq {α : Sort u_1} {β : α Sort u_2} [h₁ : decidable_eq α] [h₂ : Π (a : α), decidable_eq (β a)] :
Equations
• psigma.decidable_eq a₁, b₁⟩ a₂, b₂⟩ = psigma.decidable_eq._match_1 a₁ b₁ a₂ b₂ (h₁ a₁ a₂)
• psigma.decidable_eq._match_1 a b₁ a b₂ = psigma.decidable_eq._match_2 a b₁ b₂ (h₂ a b₁ b₂)
• psigma.decidable_eq._match_1 a₁ _x a₂ _x_1 =
• psigma.decidable_eq._match_2 a b b =
• psigma.decidable_eq._match_2 a b₁ b₂ =
theorem psigma.mk.inj_iff {α : Sort u_1} {β : α Sort u_2} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
a₁, b₁⟩ = a₂, b₂⟩ a₁ = a₂ b₁ == b₂
@[ext]
theorem psigma.ext {α : Sort u_1} {β : α Sort u_2} {x₀ x₁ : psigma β} (h₀ : x₀.fst = x₁.fst) (h₁ : x₀.snd == x₁.snd) :
x₀ = x₁
theorem psigma.ext_iff {α : Sort u_1} {β : α Sort u_2} {x₀ x₁ : psigma β} :
x₀ = x₁ x₀.fst = x₁.fst 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 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⟩
@[ext]
theorem psigma.subtype_ext {α : Sort u_1} {β : Sort u_2} {p : α β Prop} {x₀ x₁ : Σ' (a : α), subtype (p a)} :
x₀.fst = x₁.fst (x₀.snd) = (x₁.snd) 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_2} {p : α β Prop} {x₀ x₁ : Σ' (a : α), subtype (p a)} :
x₀ = x₁ x₀.fst = x₁.fst (x₀.snd) = (x₁.snd)
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
• f₂ a, b⟩ = f₁ a, f₂ a b