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

• Quotient.finChoice: Given a function f : Π i, Quotient (S i) on a fintype ι, returns the class of functions Π i, α i sending each i to an element of the class f i.
• Quotient.finChoiceEquiv: A finite family of quotients is equivalent to a quotient of finite families.
• Quotient.finLiftOn: Given a fintype ι. A function on Π i, α i which respects setoid S i for each i can be lifted to a function on Π i, Quotient (S i).
• Quotient.finRecOn: Recursion principle for quotients indexed by a finite type. It is the dependent version of Quotient.finLiftOn.

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

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.

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 ∈ l → Quotient (S i)) → Prop} (f : ∀ (a : (i : ι) → i ∈ l → α i), C fun (x1 : ι) (x2 : x1 ∈ l) => ⟦a x1 x2⟧) (q : (i : ι) → i ∈ l → Quotient (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)) : Quotient piSetoid

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.

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)) : (finChoice f).eval = f

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).

@[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.

@[simp]

theorem Quotient.finChoiceEquiv_symm_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)} (q : Quotient inferInstance) (i : ι) : finChoiceEquiv.symm q i = q.eval i

@[simp]

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

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.

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.

@[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.

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).

@[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.

@[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)) : finChoiceEquiv q = finChoice q

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.

@[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