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 := default, 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₂} :
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₂.sndp₁ = 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₁.fstx₀.snd.val = x₁.snd.valx₀ = 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 : α) × β aProp} :
(∀ (x : (a : α) × β a), p x) ∀ (a : α) (b : β a), p a, b
@[simp]
theorem Sigma.exists {α : Type u_1} {β : αType u_4} {p : (a : α) × β aProp} :
(∃ (x : (a : α) × β a), p x) ∃ (a : α), ∃ (b : β a), p a, b
theorem Sigma.exists' {α : Type u_1} {β : αType u_4} {p : (a : α) → β aProp} :
(∃ (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 : α) → β aProp} :
(∀ (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 : α} :
theorem Sigma.fst_surjective {α : Type u_1} {β : αType u_4} [h : ∀ (a : α), Nonempty (β a)] :
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)] :
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
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₂ 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)) :
    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) :
        theorem Sigma.curry_update {α : Type u_1} {β : αType u_4} {γ : (a : α) → β aType u_7} [DecidableEq α] [(a : α) → DecidableEq (β a)] (i : (a : α) × β a) (f : (i : (a : α) × β a) → γ i.fst i.snd) (x : γ i.fst i.snd) :
        def Prod.toSigma {α : Type u_7} {β : Type u_8} (p : α × β) :
        (_ : α) × β

        Convert a product type to a Σ-type.

        Equations
        • p.toSigma = p.fst, p.snd
        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 : α × β) :
          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
          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 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)] :
            Equations
            • PSigma.instInhabitedOfDefault_mathlib = { default := default, 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₂} :
            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₂.sndp₁ = p₂
            @[simp]
            theorem PSigma.forall {α : Sort u_1} {β : αSort u_2} {p : (a : α) ×' β aProp} :
            (∀ (x : (a : α) ×' β a), p x) ∀ (a : α) (b : β a), p a, b
            @[simp]
            theorem PSigma.exists' {α : Sort u_1} {β : αSort u_2} {p : (a : α) ×' β aProp} :
            (∃ (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₁.fstx₀.snd.val = x₁.snd.valx₀ = 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₂ x = match x with | a, b => f₁ a, f₂ a b
            Instances For