mathlib documentation

data.sigma.basic

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

Σ 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 (default α))] :
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₂ (is_true _) = sigma.decidable_eq._match_2 a b₁ b₂ (h₂ a b₁ b₂)
  • sigma.decidable_eq._match_1 a₁ _x a₂ _x_1 (is_false n) = is_false _
  • sigma.decidable_eq._match_2 a b b (is_true _) = is_true _
  • sigma.decidable_eq._match_2 a b₁ b₂ (is_false n) = 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
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.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 : α), β aType 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
def sigma.uncurry {α : Type u_1} {β : α → Type u_4} {γ : Π (a : α), β aType 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 : α), β aType u_2} (f : Π (x : sigma β), γ x.fst x.snd) :
@[simp]
theorem sigma.curry_uncurry {α : Type u_1} {β : α → Type u_4} {γ : Π (a : α), β aType u_2} (f : Π (x : α) (y : β x), γ x y) :
@[simp]
def prod.to_sigma {α : Type u_1} {β : Type u_2} :
α × β(Σ (_x : α), β)

Convert a product type to a Σ-type.

Equations
@[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 : α × β) :
def psigma.elim {α : Sort u_1} {β : α → Sort u_2} {γ : Sort u_3} (f : Π (a : α), β a → γ) (a : psigma β) :
γ

Nondependent eliminator for psigma.

Equations
@[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 (default α))] :
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₂ (is_true _) = psigma.decidable_eq._match_2 a b₁ b₂ (h₂ a b₁ b₂)
  • psigma.decidable_eq._match_1 a₁ _x a₂ _x_1 (is_false n) = is_false _
  • psigma.decidable_eq._match_2 a b b (is_true _) = is_true _
  • psigma.decidable_eq._match_2 a b₁ b₂ (is_false n) = 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
@[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