mathlib3 documentation

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

inhabited (sigma β)

Equations

sigma.inhabited = {default := ⟨inhabited.default _inst_1, inhabited.default _inst_2⟩}

@[protected, instance]

def sigma.decidable_eq {α : Type u_1} {β : α → Type u_4} [h₁ : decidable_eq α] [h₂ : Π (a : α), decidable_eq (β a)] :

decidable_eq (sigma β)

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₂ (decidable.is_true _) = sigma.decidable_eq._match_2 a b₁ b₂ (h₂ a b₁ b₂)
sigma.decidable_eq._match_1 a₁ _x a₂ _x_1 (decidable.is_false n) = decidable.is_false _
sigma.decidable_eq._match_2 a b b (decidable.is_true _) = decidable.is_true _
sigma.decidable_eq._match_2 a b₁ b₂ (decidable.is_false n) = decidable.is_false _

@[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

sigma.map f₁ f₂ x = ⟨f₁ x.fst, f₂ x.fst x.snd⟩

theorem sigma_mk_injective {α : Type u_1} {β : α → Type u_4} {i : α} :

function.injective (sigma.mk 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)) :

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_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

sigma.curry f 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

sigma.uncurry f x = f x.fst x.snd

@[simp]

theorem sigma.uncurry_curry {α : Type u_1} {β : α → Type u_4} {γ : Π (a : α), β a → Type u_2} (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_2} (f : Π (x : α) (y : β x), γ x y) :

sigma.curry (sigma.uncurry f) = f

def prod.to_sigma {α : Type u_1} {β : Type u_2} (p : α × β) :

Σ (_x : α), β

Convert a product type to a Σ-type.

Equations

p.to_sigma = ⟨p.fst, p.snd⟩

@[simp]

theorem prod.fst_comp_to_sigma {α : Type u_1} {β : Type u_2} :

sigma.fst ∘ prod.to_sigma = prod.fst

@[simp]

theorem prod.fst_to_sigma {α : Type u_1} {β : Type u_2} (x : α × β) :

x.to_sigma.fst = x.fst

@[simp]

theorem prod.snd_to_sigma {α : Type u_1} {β : Type u_2} (x : α × β) :

x.to_sigma.snd = x.snd

@[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 [reflected_univ] [reflected_univ] {α : 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

psigma.elim f 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) :

psigma.elim f ⟨a, b⟩ = f a b

@[protected, instance]

def psigma.inhabited {α : Sort u_1} {β : α → Sort u_2} [inhabited α] [inhabited (β inhabited.default)] :

inhabited (psigma β)

Equations

psigma.inhabited = {default := ⟨inhabited.default _inst_1, inhabited.default _inst_2⟩}

@[protected, instance]

def psigma.decidable_eq {α : Sort u_1} {β : α → Sort u_2} [h₁ : decidable_eq α] [h₂ : Π (a : α), decidable_eq (β a)] :

decidable_eq (psigma β)

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₂ (decidable.is_true _) = psigma.decidable_eq._match_2 a b₁ b₂ (h₂ a b₁ b₂)
psigma.decidable_eq._match_1 a₁ _x a₂ _x_1 (decidable.is_false n) = decidable.is_false _
psigma.decidable_eq._match_2 a b b (decidable.is_true _) = decidable.is_true _
psigma.decidable_eq._match_2 a b₁ b₂ (decidable.is_false n) = decidable.is_false _

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

psigma.map f₁ f₂ ⟨a, b⟩ = ⟨f₁ a, f₂ a b⟩