Quotients of families indexed by a finite type

This file provides Quotient.finChoice, a mechanism to go from a finite family of quotients to a quotient of finite families.

Main definitions

• Quotient.finChoice

def Quotient.finChoiceAux {ι : Type u_1} [DecidableEq ι] {α : ι → Type u_2} [S : (i : ι) → Setoid (α i)] (l : List ι) : ((i : ι) → i ∈ l → Quotient (S i)) → Quotient inferInstance

An auxiliary function for Quotient.finChoice. Given a collection of setoids indexed by a type ι, a (finite) 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

• One or more equations did not get rendered due to their size.
• Quotient.finChoiceAux [] x_2 = ⟦fun (x : ι) (h : x ∈ []) => nomatch ⋯⟧

theorem Quotient.finChoiceAux_eq {ι : Type u_1} [DecidableEq ι] {α : ι → Type u_2} [S : (i : ι) → Setoid (α i)] (l : List ι) (f : (i : ι) → i ∈ l → α i) : (Quotient.finChoiceAux l fun (i : ι) (h : i ∈ l) => ⟦f i h⟧) = ⟦f⟧

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

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.

Equations

• One or more equations did not get rendered due to their size.

theorem Quotient.finChoice_eq {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ι → Type u_2} [(i : ι) → Setoid (α i)] (f : (i : ι) → α i) : (Quotient.finChoice fun (i : ι) => ⟦f i⟧) = ⟦f⟧

def Trunc.finChoice {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ι → Type u_2} (f : (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

• Trunc.finChoice f = Quotient.map' id ⋯ (Quotient.finChoice f)

theorem Trunc.finChoice_eq {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ι → Type u_2} (f : (i : ι) → α i) : (Trunc.finChoice fun (i : ι) => Trunc.mk (f i)) = Trunc.mk f