Documentation

Mathlib.Logic.Equiv.Sum

Equivalence between sum types #

In this file we continue the work on equivalences begun in Mathlib/Logic/Equiv/Defs.lean, defining

More definitions of this kind can be found in other files. E.g., Mathlib/Algebra/Equiv/TransferInstance.lean does it for many algebraic type classes like Group, Module, etc.

Tags #

equivalence, congruence, bijective map

def Equiv.psumEquivSum (α : Type u_9) (β : Type u_10) :
α ⊕' β α β

PSum is equivalent to Sum.

Equations
Instances For
    def Equiv.sumCongr {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (ea : α₁ α₂) (eb : β₁ β₂) :
    α₁ β₁ α₂ β₂

    If α ≃ α' and β ≃ β', then α ⊕ β ≃ α' ⊕ β'. This is Sum.map as an equivalence.

    Equations
    Instances For
      @[simp]
      theorem Equiv.sumCongr_apply {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (ea : α₁ α₂) (eb : β₁ β₂) (a✝ : α₁ β₁) :
      (ea.sumCongr eb) a✝ = Sum.map (⇑ea) (⇑eb) a✝
      @[simp]
      theorem Equiv.sumCongr_trans {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} {γ₁ : Type u_13} {γ₂ : Type u_14} (e : α₁ β₁) (f : α₂ β₂) (g : β₁ γ₁) (h : β₂ γ₂) :
      (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)
      @[simp]
      theorem Equiv.sumCongr_symm {α : Type u_9} {β : Type u_10} {γ : Type u_11} {δ : Type u_12} (e : α β) (f : γ δ) :
      @[simp]
      theorem Equiv.sumCongr_refl {α : Type u_9} {β : Type u_10} :
      def Equiv.psumCongr {α : Sort u_1} {β : Sort u_4} {γ : Sort u_7} {δ : Sort u_8} (e₁ : α β) (e₂ : γ δ) :
      α ⊕' γ β ⊕' δ

      If α ≃ α' and β ≃ β', then α ⊕' β ≃ α' ⊕' β'.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Equiv.psumSum {α₁ : Sort u_2} {β₁ : Sort u_5} {α₂ : Type u_9} {β₂ : Type u_10} (ea : α₁ α₂) (eb : β₁ β₂) :
        α₁ ⊕' β₁ α₂ β₂

        Combine two Equivs using PSum in the domain and Sum in the codomain.

        Equations
        Instances For
          def Equiv.sumPSum {α₂ : Sort u_3} {β₂ : Sort u_6} {α₁ : Type u_9} {β₁ : Type u_10} (ea : α₁ α₂) (eb : β₁ β₂) :
          α₁ β₁ α₂ ⊕' β₂

          Combine two Equivs using Sum in the domain and PSum in the codomain.

          Equations
          Instances For
            def Equiv.subtypeSum {α : Type u_9} {β : Type u_10} {p : α βProp} :
            { c : α β // p c } { a : α // p (Sum.inl a) } { b : β // p (Sum.inr b) }

            A subtype of a sum is equivalent to a sum of subtypes.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[reducible, inline]
              abbrev Equiv.Perm.sumCongr {α : Type u_9} {β : Type u_10} (ea : Perm α) (eb : Perm β) :
              Perm (α β)

              Combine a permutation of α and of β into a permutation of α ⊕ β.

              Equations
              Instances For
                @[simp]
                theorem Equiv.Perm.sumCongr_apply {α : Type u_9} {β : Type u_10} (ea : Perm α) (eb : Perm β) (x : α β) :
                (ea.sumCongr eb) x = Sum.map (⇑ea) (⇑eb) x
                theorem Equiv.Perm.sumCongr_trans {α : Type u_9} {β : Type u_10} (e : Perm α) (f : Perm β) (g : Perm α) (h : Perm β) :
                theorem Equiv.Perm.sumCongr_symm {α : Type u_9} {β : Type u_10} (e : Perm α) (f : Perm β) :
                theorem Equiv.Perm.sumCongr_refl {α : Type u_9} {β : Type u_10} :

                Bool is equivalent the sum of two PUnits.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Equiv.sumComm (α : Type u_9) (β : Type u_10) :
                  α β β α

                  Sum of types is commutative up to an equivalence. This is Sum.swap as an equivalence.

                  Equations
                  Instances For
                    @[simp]
                    theorem Equiv.sumComm_apply (α : Type u_9) (β : Type u_10) :
                    (sumComm α β) = Sum.swap
                    @[simp]
                    theorem Equiv.sumComm_symm (α : Type u_9) (β : Type u_10) :
                    (sumComm α β).symm = sumComm β α
                    def Equiv.sumAssoc (α : Type u_9) (β : Type u_10) (γ : Type u_11) :
                    (α β) γ α β γ

                    Sum of types is associative up to an equivalence.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem Equiv.sumAssoc_apply_inl_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) :
                      (sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a
                      @[simp]
                      theorem Equiv.sumAssoc_apply_inl_inr {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β) :
                      (sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)
                      @[simp]
                      theorem Equiv.sumAssoc_apply_inr {α : Type u_9} {β : Type u_10} {γ : Type u_11} (c : γ) :
                      (sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)
                      @[simp]
                      theorem Equiv.sumAssoc_symm_apply_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) :
                      (sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
                      @[simp]
                      theorem Equiv.sumAssoc_symm_apply_inr_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β) :
                      @[simp]
                      theorem Equiv.sumAssoc_symm_apply_inr_inr {α : Type u_9} {β : Type u_10} {γ : Type u_11} (c : γ) :
                      (sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
                      def Equiv.sumSumSumComm (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) :
                      (α β) γ δ (α γ) β δ

                      Four-way commutativity of sum. The name matches add_add_add_comm.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem Equiv.sumSumSumComm_apply (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) (a✝ : (α β) γ δ) :
                        (sumSumSumComm α β γ δ) a✝ = ((sumAssoc (α γ) β δ) Sum.map (⇑(sumAssoc α γ β).symm) id Sum.map (Sum.map id (sumComm β γ)) id Sum.map (⇑(sumAssoc α β γ)) id (sumAssoc (α β) γ δ).symm) a✝
                        @[simp]
                        theorem Equiv.sumSumSumComm_symm (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) :
                        (sumSumSumComm α β γ δ).symm = sumSumSumComm α γ β δ
                        def Equiv.sumEmpty (α : Type u_9) (β : Type u_10) [IsEmpty β] :
                        α β α

                        Sum with IsEmpty is equivalent to the original type.

                        Equations
                        Instances For
                          @[simp]
                          theorem Equiv.sumEmpty_symm_apply (α : Type u_9) (β : Type u_10) [IsEmpty β] (val : α) :
                          (sumEmpty α β).symm val = Sum.inl val
                          @[simp]
                          theorem Equiv.sumEmpty_apply_inl {α : Type u_9} {β : Type u_10} [IsEmpty β] (a : α) :
                          (sumEmpty α β) (Sum.inl a) = a
                          def Equiv.emptySum (α : Type u_9) (β : Type u_10) [IsEmpty α] :
                          α β β

                          The sum of IsEmpty with any type is equivalent to that type.

                          Equations
                          Instances For
                            @[simp]
                            theorem Equiv.emptySum_symm_apply (α : Type u_9) (β : Type u_10) [IsEmpty α] (a✝ : β) :
                            (emptySum α β).symm a✝ = Sum.inr a✝
                            @[simp]
                            theorem Equiv.emptySum_apply_inr {α : Type u_9} {β : Type u_10} [IsEmpty α] (b : β) :
                            (emptySum α β) (Sum.inr b) = b
                            def Equiv.sumEquivSigmaBool (α β : Type u_9) :
                            α β (b : Bool) × bif b then β else α

                            α ⊕ β is equivalent to a Sigma-type over Bool. Note that this definition assumes α and β to be types from the same universe, so it cannot be used directly to transfer theorems about sigma types to theorems about sum types. In many cases one can use ULift to work around this difficulty.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def Equiv.sigmaFiberEquiv {α : Type u_9} {β : Type u_10} (f : αβ) :
                              (y : β) × { x : α // f x = y } α

                              sigmaFiberEquiv f for f : α → β is the natural equivalence between the type of all fibres of f and the total space α.

                              Equations
                              • Equiv.sigmaFiberEquiv f = { toFun := fun (x : (y : β) × { x : α // f x = y }) => x.snd, invFun := fun (x : α) => f x, x, , left_inv := , right_inv := }
                              Instances For
                                @[simp]
                                theorem Equiv.sigmaFiberEquiv_apply {α : Type u_9} {β : Type u_10} (f : αβ) (x : (y : β) × { x : α // f x = y }) :
                                (sigmaFiberEquiv f) x = x.snd
                                @[simp]
                                theorem Equiv.sigmaFiberEquiv_symm_apply_fst {α : Type u_9} {β : Type u_10} (f : αβ) (x : α) :
                                @[simp]
                                theorem Equiv.sigmaFiberEquiv_symm_apply_snd_coe {α : Type u_9} {β : Type u_10} (f : αβ) (x : α) :
                                ((sigmaFiberEquiv f).symm x).snd = x
                                def Equiv.sigmaEquivOptionOfInhabited (α : Type u) [Inhabited α] [DecidableEq α] :
                                (β : Type u) × (α Option β)

                                Inhabited types are equivalent to Option β for some β by identifying default with none.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def Equiv.sumCompl {α : Type u_9} (p : αProp) [DecidablePred p] :
                                  { a : α // p a } { a : α // ¬p a } α

                                  For any predicate p on α, the sum of the two subtypes {a // p a} and its complement {a // ¬ p a} is naturally equivalent to α.

                                  See subtypeOrEquiv for sum types over subtypes {x // p x} and {x // q x} that are not necessarily IsCompl p q.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Equiv.sumCompl_apply_inl {α : Type u_9} (p : αProp) [DecidablePred p] (x : { a : α // p a }) :
                                    (sumCompl p) (Sum.inl x) = x
                                    @[simp]
                                    theorem Equiv.sumCompl_apply_inr {α : Type u_9} (p : αProp) [DecidablePred p] (x : { a : α // ¬p a }) :
                                    (sumCompl p) (Sum.inr x) = x
                                    @[simp]
                                    theorem Equiv.sumCompl_apply_symm_of_pos {α : Type u_9} (p : αProp) [DecidablePred p] (a : α) (h : p a) :
                                    (sumCompl p).symm a = Sum.inl a, h
                                    @[simp]
                                    theorem Equiv.sumCompl_apply_symm_of_neg {α : Type u_9} (p : αProp) [DecidablePred p] (a : α) (h : ¬p a) :
                                    (sumCompl p).symm a = Sum.inr a, h
                                    def Equiv.prodSumDistrib (α : Type u_9) (β : Type u_10) (γ : Type u_11) :
                                    α × (β γ) α × β α × γ

                                    Type product is left distributive with respect to type sum up to an equivalence.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Equiv.prodSumDistrib_apply_left {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) (b : β) :
                                      @[simp]
                                      theorem Equiv.prodSumDistrib_apply_right {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) (c : γ) :
                                      @[simp]
                                      theorem Equiv.prodSumDistrib_symm_apply_left {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α × β) :
                                      @[simp]
                                      theorem Equiv.prodSumDistrib_symm_apply_right {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α × γ) :
                                      def Equiv.sigmaSumDistrib {ι : Type u_11} (α : ιType u_9) (β : ιType u_10) :
                                      (i : ι) × (α i β i) (i : ι) × α i (i : ι) × β i

                                      An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums. Compare with Equiv.sumSigmaDistrib which is indexed by sums.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem Equiv.sigmaSumDistrib_symm_apply {ι : Type u_11} (α : ιType u_9) (β : ιType u_10) (a✝ : (i : ι) × α i (i : ι) × β i) :
                                        (sigmaSumDistrib α β).symm a✝ = Sum.elim (Sigma.map id fun (x : ι) => Sum.inl) (Sigma.map id fun (x : ι) => Sum.inr) a✝
                                        @[simp]
                                        theorem Equiv.sigmaSumDistrib_apply {ι : Type u_11} (α : ιType u_9) (β : ιType u_10) (p : (i : ι) × (α i β i)) :
                                        def Equiv.sumSigmaDistrib {α : Type u_10} {β : Type u_11} (t : α βType u_9) :
                                        (i : α β) × t i (i : α) × t (Sum.inl i) (i : β) × t (Sum.inr i)

                                        A type indexed by disjoint sums of types is equivalent to the sum of the sums. Compare with Equiv.sigmaSumDistrib which has the sums as the output type.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[simp]
                                          theorem Equiv.sumSigmaDistrib_symm_apply {α : Type u_10} {β : Type u_11} (t : α βType u_9) (a✝ : (i : α) × t (Sum.inl i) (i : β) × t (Sum.inr i)) :
                                          (sumSigmaDistrib t).symm a✝ = Sum.elim (fun (a : (i : α) × t (Sum.inl i)) => Sum.inl a.fst, a.snd) (fun (b : (i : β) × t (Sum.inr i)) => Sum.inr b.fst, b.snd) a✝
                                          @[simp]
                                          theorem Equiv.sumSigmaDistrib_apply {α : Type u_10} {β : Type u_11} (t : α βType u_9) (x✝ : (i : α β) × t i) :
                                          (sumSigmaDistrib t) x✝ = match x✝ with | Sum.inl x, y => Sum.inl x, y | Sum.inr x, y => Sum.inr x, y