Documentation

Mathlib.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. 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)] :
Equations
  • Sigma.instInhabitedSigma = { default := { fst := default, snd := default } }
instance Sigma.instDecidableEqSigma {α : Type u_1} {β : αType u_4} [h₁ : DecidableEq α] [h₂ : (a : α) → DecidableEq (β a)] :
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 {α : Type u_1} {β : αType u_4} {x₀ : Sigma β} {x₁ : Sigma β} (h₀ : x₀.fst = x₁.fst) (h₁ : HEq x₀.snd x₁.snd) :
x₀ = 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₁.fstx₀.snd.val = x₁.snd.valx₀ = 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 : α) × β aProp} :
((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 : α) × β aProp} :
(x, p x) a b, p { fst := a, snd := b }
theorem Sigma.exists' {α : Type u_1} {β : αType u_4} {p : (a : α) → β aProp} :
(a b, p a b) x, p x.fst x.snd
theorem Sigma.forall' {α : Type u_1} {β : αType u_4} {p : (a : α) → β aProp} :
((a : α) → (b : β a) → p a b) (x : (a : α) × β a) → p x.fst x.snd
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 }
Instances For
    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 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 : α) → β aType 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
    Instances For
      def Sigma.uncurry {α : Type u_1} {β : αType u_4} {γ : (a : α) → β aType 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
      Instances For
        @[simp]
        theorem Sigma.uncurry_curry {α : Type u_1} {β : αType u_4} {γ : (a : α) → β aType u_7} (f : (x : Sigma β) → γ x.fst x.snd) :
        @[simp]
        theorem Sigma.curry_uncurry {α : Type u_1} {β : αType u_4} {γ : (a : α) → β aType u_7} (f : (x : α) → (y : β x) → γ x y) :
        def Prod.toSigma {α : Type u_7} {β : Type u_8} (p : α × β) :
        (_ : α) × β

        Convert a product type to a Σ-type.

        Equations
        Instances For
          @[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
          Instances For
            @[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)] :
            Equations
            • PSigma.instInhabitedPSigma = { default := { fst := default, snd := default } }
            instance PSigma.decidableEq {α : Sort u_1} {β : αSort u_2} [h₁ : DecidableEq α] [h₂ : (a : α) → DecidableEq (β a)] :
            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 {α : Sort u_1} {β : αSort u_2} {x₀ : PSigma β} {x₁ : PSigma β} (h₀ : x₀.fst = x₁.fst) (h₁ : HEq x₀.snd x₁.snd) :
            x₀ = x₁
            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 : α) ×' β aProp} :
            ((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 : α) ×' β aProp} :
            (x, p x) a b, 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₁.fstx₀.snd.val = x₁.snd.valx₀ = 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 }
            Instances For