Documentation

Mathlib.Data.Fintype.Quotient

Quotients of families indexed by a finite type #

This file proves some basic facts and defines lifting and recursion principle for quotients indexed by a finite type.

Main definitions #

def Quotient.listChoice {ι : Type u_1} [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {l : List ι} (q : (i : ι) → i lQuotient (S i)) :

Given a collection of setoids indexed by a type ι, a list l of indices, and a function that for each i ∈ l gives a term of the corresponding quotient type, then there is a corresponding term in the quotient of the product of the setoids indexed by l.

Equations
    Instances For
      theorem Quotient.listChoice_mk {ι : Type u_1} [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {l : List ι} (a : (i : ι) → i lα i) :
      (listChoice fun (x1 : ι) (x2 : x1 l) => a x1 x2) = a
      theorem Quotient.list_ind {ι : Type u_1} [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {l : List ι} {C : ((i : ι) → i lQuotient (S i))Prop} (f : ∀ (a : (i : ι) → i lα i), C fun (x1 : ι) (x2 : x1 l) => a x1 x2) (q : (i : ι) → i lQuotient (S i)) :
      C q

      Choice-free induction principle for quotients indexed by a List.

      theorem Quotient.ind_fintype_pi {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {C : ((i : ι) → Quotient (S i))Prop} (f : ∀ (a : (i : ι) → α i), C fun (x : ι) => a x) (q : (i : ι) → Quotient (S i)) :
      C q

      Choice-free induction principle for quotients indexed by a finite type. See Quotient.induction_on_pi for the general version assuming Classical.choice.

      theorem Quotient.induction_on_fintype_pi {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {C : ((i : ι) → Quotient (S i))Prop} (q : (i : ι) → Quotient (S i)) (f : ∀ (a : (i : ι) → α i), C fun (x : ι) => a x) :
      C q

      Choice-free induction principle for quotients indexed by a finite type. See Quotient.induction_on_pi for the general version assuming Classical.choice.

      def Quotient.finChoice {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} (q : (i : ι) → Quotient (S i)) :

      Given a collection of setoids indexed by a fintype ι and a function that for each i : ι gives a term of the corresponding quotient type, then there is corresponding term in the quotient of the product of the setoids. See Quotient.choice for the noncomputable general version.

      Equations
        Instances For
          theorem Quotient.finChoice_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} (a : (i : ι) → α i) :
          (finChoice fun (x : ι) => a x) = a
          theorem Quotient.eval_finChoice {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} (f : (i : ι) → Quotient (S i)) :
          def Quotient.finLiftOn {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {β : Sort u_3} (q : (i : ι) → Quotient (S i)) (f : ((i : ι) → α i)β) (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i b i)f a = f b) :
          β

          Lift a function on ∀ i, α i to a function on ∀ i, Quotient (S i).

          Equations
            Instances For
              @[simp]
              theorem Quotient.finLiftOn_empty {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {β : Sort u_3} [e : IsEmpty ι] (q : (i : ι) → Quotient (S i)) :
              finLiftOn q = fun (f : ((i : ι) → α i)β) (x : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i b i)f a = f b) => f fun (a : ι) => e.elim a
              @[simp]
              theorem Quotient.finLiftOn_mk {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {β : Sort u_3} (a : (i : ι) → α i) :
              (finLiftOn fun (x : ι) => a x) = fun (f : ((i : ι) → α i)β) (x : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i b i)f a = f b) => f a
              def Quotient.finChoiceEquiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} :
              ((i : ι) → Quotient (S i)) Quotient piSetoid

              Quotient.finChoice as an equivalence.

              Equations
                Instances For
                  @[simp]
                  theorem Quotient.finChoiceEquiv_symm_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} (q : Quotient inferInstance) (i : ι) :
                  @[simp]
                  theorem Quotient.finChoiceEquiv_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} (q : (i : ι) → Quotient (S i)) :
                  def Quotient.finHRecOn {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {C : ((i : ι) → Quotient (S i))Sort u_4} (q : (i : ι) → Quotient (S i)) (f : (a : (i : ι) → α i) → C fun (x : ι) => a x) (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i b i)f a f b) :
                  C q

                  Recursion principle for quotients indexed by a finite type.

                  Equations
                    Instances For
                      def Quotient.finRecOn {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {C : ((i : ι) → Quotient (S i))Sort u_4} (q : (i : ι) → Quotient (S i)) (f : (a : (i : ι) → α i) → C fun (x : ι) => a x) (h : ∀ (a b : (i : ι) → α i) (h : ∀ (i : ι), a i b i), f a = f b) :
                      C q

                      Recursion principle for quotients indexed by a finite type.

                      Equations
                        Instances For
                          @[simp]
                          theorem Quotient.finHRecOn_mk {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {C : ((i : ι) → Quotient (S i))Sort u_4} (a : (i : ι) → α i) :
                          (finHRecOn fun (x : ι) => a x) = fun (f : (a : (i : ι) → α i) → C fun (x : ι) => a x) (x : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i b i)f a f b) => f a
                          @[simp]
                          theorem Quotient.finRecOn_mk {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ιSort u_2} {S : (i : ι) → Setoid (α i)} {C : ((i : ι) → Quotient (S i))Sort u_4} (a : (i : ι) → α i) :
                          (finRecOn fun (x : ι) => a x) = fun (f : (a : (i : ι) → α i) → C fun (x : ι) => a x) (x : ∀ (a b : (i : ι) → α i) (h : ∀ (i : ι), a i b i), f a = f b) => f a
                          def Trunc.finChoice {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιSort u_2} (q : (i : ι) → Trunc (α i)) :
                          Trunc ((i : ι) → α i)

                          Given a function that for each i : ι gives a term of the corresponding truncation type, then there is corresponding term in the truncation of the product.

                          Equations
                            Instances For
                              theorem Trunc.finChoice_eq {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιSort u_2} (f : (i : ι) → α i) :
                              (finChoice fun (i : ι) => mk (f i)) = mk f
                              def Trunc.finLiftOn {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιSort u_2} {β : Sort u_3} (q : (i : ι) → Trunc (α i)) (f : ((i : ι) → α i)β) (h : ∀ (a b : (i : ι) → α i), f a = f b) :
                              β

                              Lift a function on ∀ i, α i to a function on ∀ i, Trunc (α i).

                              Equations
                                Instances For
                                  @[simp]
                                  theorem Trunc.finLiftOn_empty {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιSort u_2} {β : Sort u_3} [e : IsEmpty ι] (q : (i : ι) → Trunc (α i)) :
                                  finLiftOn q = fun (f : ((i : ι) → α i)β) (x : ∀ (a b : (i : ι) → α i), f a = f b) => f fun (a : ι) => e.elim a
                                  @[simp]
                                  theorem Trunc.finLiftOn_mk {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιSort u_2} {β : Sort u_3} (a : (i : ι) → α i) :
                                  (finLiftOn fun (x : ι) => a x) = fun (f : ((i : ι) → α i)β) (x : ∀ (a b : (i : ι) → α i), f a = f b) => f a
                                  def Trunc.finChoiceEquiv {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιSort u_2} :
                                  ((i : ι) → Trunc (α i)) Trunc ((i : ι) → α i)

                                  Trunc.finChoice as an equivalence.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem Trunc.finChoiceEquiv_symm_apply {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιSort u_2} (q : Trunc ((i : ι) → α i)) (i : ι) :
                                      finChoiceEquiv.symm q i = map (fun (x : (i : ι) → α i) => x i) q
                                      @[simp]
                                      theorem Trunc.finChoiceEquiv_apply {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιSort u_2} (q : (i : ι) → Trunc (α i)) :
                                      def Trunc.finRecOn {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιSort u_2} {C : ((i : ι) → Trunc (α i))Sort u_4} (q : (i : ι) → Trunc (α i)) (f : (a : (i : ι) → α i) → C fun (x : ι) => mk (a x)) (h : ∀ (a b : (i : ι) → α i), f a = f b) :
                                      C q

                                      Recursion principle for Truncs indexed by a finite type.

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem Trunc.finRecOn_mk {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιSort u_2} {C : ((i : ι) → Trunc (α i))Sort u_4} (a : (i : ι) → α i) :
                                          (finRecOn fun (x : ι) => a x) = fun (f : (a : (i : ι) → α i) → C fun (x : ι) => mk (a x)) (x : ∀ (a b : (i : ι) → α i), f a = f b) => f a