Mathlib.Data.Fintype.Quotient

Quotient.listChoice definition

{l : List ι} (q : ∀ i ∈ l, Quotient (S i)) : @Quotient (∀ i ∈ l, α i) piSetoid

Full source

/-- 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`. -/
def listChoice {l : List ι} (q : ∀ i ∈ l, Quotient (S i)) : @Quotient (∀ i ∈ l, α i) piSetoid :=
  match l with
  |     [] => ⟦nofun⟧
  | i :: _ => Quotient.liftOn₂ (List.Pi.head (i := i) q)
    (listChoice (List.Pi.tail q))
    (⟦List.Pi.cons _ _ · ·⟧)
    (fun _ _ _ _ ha hl ↦ Quotient.sound (List.Pi.forall_rel_cons_ext ha hl))

Quotient construction for dependent functions over a list

Informal description

Given a list `l` of indices of type `ι` and for each `i ∈ l` a quotient `Quotient (S i)` of a setoid `S i` on `α i`, the function `listChoice` constructs an element of the quotient of the product setoid `piSetoid` on the dependent function type `∀ i ∈ l, α i`. This is done by recursively lifting the head and tail of the list, ensuring compatibility with the setoid relations.

Quotient.listChoice_mk theorem

{l : List ι} (a : ∀ i ∈ l, α i) : listChoice (S := S) (⟦a · ·⟧) = ⟦a⟧

Full source

theorem listChoice_mk {l : List ι} (a : ∀ i ∈ l, α i) : listChoice (S := S) (⟦a · ·⟧) = ⟦a⟧ :=
  match l with
  |     [] => Quotient.sound nofun
  | i :: l => by
    unfold listChoice List.Pi.tail
    rw [listChoice_mk]
    exact congrArg (⟦·⟧) (List.Pi.cons_eta a)

Equivalence Class Preservation under $\text{listChoice}$ for List-Indexed Functions

Informal description

For any list $l$ of indices of type $\iota$ and any function $a \colon \forall i \in l, \alpha_i$, the equivalence class of $a$ under the product setoid $\text{piSetoid}$ is equal to the result of applying $\text{listChoice}$ to the family of equivalence classes $\llbracket a \rrbracket$ for each $i \in l$.

Quotient.list_ind theorem

 {l : List ι} {C : (∀ i ∈ l, Quotient (S i)) → Prop} (f : ∀ a : ∀ i ∈ l, α i, C (⟦a · ·⟧))
  (q : ∀ i ∈ l, Quotient (S i)) : C q

Full source

/-- Choice-free induction principle for quotients indexed by a `List`. -/
@[elab_as_elim]
lemma list_ind {l : List ι} {C : (∀ i ∈ l, Quotient (S i)) → Prop}
    (f : ∀ a : ∀ i ∈ l, α i, C (⟦a · ·⟧)) (q : ∀ i ∈ l, Quotient (S i)) : C q :=
  match l with
  |     [] => cast (congr_arg _ (funext₂ nofun)) (f nofun)
  | i :: l => by
    rw [← List.Pi.cons_eta q]
    induction' List.Pi.head q using Quotient.ind with a
    refine @list_ind _ (fun q ↦ C (List.Pi.cons _ _ ⟦a⟧ q)) ?_ (List.Pi.tail q)
    intro as
    rw [List.Pi.cons_map a as (fun i ↦ Quotient.mk (S i))]
    exact f _

Induction Principle for Quotients Indexed by a List

Informal description

Let $l$ be a list of indices of type $\iota$, and let $S_i$ be a setoid on $\alpha_i$ for each $i \in l$. Given a predicate $C$ on functions mapping each $i \in l$ to a quotient $\text{Quotient}(S_i)$, if $C$ holds for all functions $a \colon \Pi i \in l, \alpha_i$ when applied to their equivalence classes $\llbracket a \rrbracket$, then $C$ holds for any function $q \colon \Pi i \in l, \text{Quotient}(S_i)$.

Quotient.ind_fintype_pi theorem

{C : (∀ i, Quotient (S i)) → Prop} (f : ∀ a : ∀ i, α i, C (⟦a ·⟧)) (q : ∀ i, Quotient (S i)) : C q

Full source

/-- Choice-free induction principle for quotients indexed by a finite type.
  See `Quotient.induction_on_pi` for the general version assuming `Classical.choice`. -/
@[elab_as_elim]
lemma ind_fintype_pi {C : (∀ i, Quotient (S i)) → Prop}
    (f : ∀ a : ∀ i, α i, C (⟦a ·⟧)) (q : ∀ i, Quotient (S i)) : C q := by
  have {m : Multiset ι} (C : (∀ i ∈ m, Quotient (S i)) → Prop) :
      ∀ (_ : ∀ a : ∀ i ∈ m, α i, C (⟦a · ·⟧)) (q : ∀ i ∈ m, Quotient (S i)), C q := by
    induction m using Quotient.ind
    exact list_ind
  exact this (fun q ↦ C (q · (Finset.mem_univ _))) (fun _ ↦ f _) (fun i _ ↦ q i)

Induction Principle for Quotients Indexed by a Finite Type

Informal description

Let $\iota$ be a finite type and for each $i \in \iota$, let $S_i$ be a setoid on $\alpha_i$. Given a predicate $C$ on functions mapping each $i$ to a quotient $\text{Quotient}(S_i)$, if $C$ holds for all functions $a \colon \Pi i, \alpha_i$ when applied to their equivalence classes $\llbracket a \rrbracket$, then $C$ holds for any function $q \colon \Pi i, \text{Quotient}(S_i)$.

Quotient.induction_on_fintype_pi theorem

{C : (∀ i, Quotient (S i)) → Prop} (q : ∀ i, Quotient (S i)) (f : ∀ a : ∀ i, α i, C (⟦a ·⟧)) : C q

Full source

/-- Choice-free induction principle for quotients indexed by a finite type.
  See `Quotient.induction_on_pi` for the general version assuming `Classical.choice`. -/
@[elab_as_elim]
lemma induction_on_fintype_pi {C : (∀ i, Quotient (S i)) → Prop}
    (q : ∀ i, Quotient (S i)) (f : ∀ a : ∀ i, α i, C (⟦a ·⟧)) : C q :=
  ind_fintype_pi f q

Induction Principle for Quotients Indexed by a Finite Type

Informal description

Let $\iota$ be a finite type and for each $i \in \iota$, let $S_i$ be a setoid on $\alpha_i$. Given a predicate $C$ on functions mapping each $i$ to a quotient $\text{Quotient}(S_i)$, if for every function $a \colon \Pi i, \alpha_i$ the predicate $C$ holds for the function $\llbracket a \rrbracket \colon \Pi i, \text{Quotient}(S_i)$ (where $\llbracket a \rrbracket$ maps each $i$ to the equivalence class of $a(i)$), then $C$ holds for any function $q \colon \Pi i, \text{Quotient}(S_i)$.

Quotient.finChoice definition

(q : ∀ i, Quotient (S i)) : @Quotient (∀ i, α i) piSetoid

Full source

/-- 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. -/
def finChoice (q : ∀ i, Quotient (S i)) :
    @Quotient (∀ i, α i) piSetoid := by
  let e := Equiv.subtypeQuotientEquivQuotientSubtype (fun l : List ι ↦ ∀ i, i ∈ l)
    (fun s : Multiset ι ↦ ∀ i, i ∈ s) (fun i ↦ Iff.rfl) (fun _ _ ↦ Iff.rfl) ⟨_, Finset.mem_univ⟩
  refine e.liftOn
    (fun l ↦ (listChoice fun i _ ↦ q i).map (fun a i ↦ a i (l.2 i)) ?_) ?_
  · exact fun _ _ h i ↦ h i _
  intro _ _ _
  refine ind_fintype_pi (fun a ↦ ?_) q
  simp_rw [listChoice_mk, Quotient.map_mk]

Finite choice of representatives in product quotients

Informal description

Given a finite type $\iota$ and for each $i \in \iota$ a quotient $\text{Quotient}(S_i)$ of a setoid $S_i$ on $\alpha_i$, the function $\text{finChoice}$ constructs an element of the quotient of the product setoid $\text{piSetoid}$ on the dependent function type $\forall i, \alpha_i$. This is done by lifting a function that selects representatives from each quotient class to a function on the entire product type, respecting the equivalence relations.

Quotient.finChoice_eq theorem

(a : ∀ i, α i) : finChoice (S := S) (⟦a ·⟧) = ⟦a⟧

Full source

theorem finChoice_eq (a : ∀ i, α i) :
    finChoice (S := S) (⟦a ·⟧) = ⟦a⟧ := by
  dsimp [finChoice]
  obtain ⟨l, hl⟩ := (Finset.univ.val : Multiset ι).exists_rep
  simp_rw [← hl, Equiv.subtypeQuotientEquivQuotientSubtype, listChoice_mk]
  rfl

Equivalence Class Preservation under $\text{finChoice}$ for Finite Product Quotients

Informal description

For any function $a \colon \forall i, \alpha_i$ where each $\alpha_i$ has a setoid structure $S_i$, the equivalence class of $a$ under the product setoid $\text{piSetoid}$ is equal to the result of applying $\text{finChoice}$ to the family of equivalence classes $\llbracket a \rrbracket$ for each $i$.

Quotient.eval_finChoice theorem

(f : ∀ i, Quotient (S i)) : eval (finChoice f) = f

Full source

lemma eval_finChoice (f : ∀ i, Quotient (S i)) :
    eval (finChoice f) = f :=
  induction_on_fintype_pi f (fun a ↦ by rw [finChoice_eq]; rfl)

Evaluation of Finite Choice Representative in Product Quotients is Identity

Informal description

For any finite type $\iota$ and for each $i \in \iota$, let $S_i$ be a setoid on $\alpha_i$. Given a function $f \colon \forall i, \text{Quotient}(S_i)$, the evaluation of the quotient element $\text{finChoice}(f)$ at any index $i$ is equal to $f(i)$. In other words, the composition of $\text{finChoice}$ with evaluation at any index $i$ is the identity function on the family of quotients.

Quotient.finLiftOn definition

 (q : ∀ i, Quotient (S i)) (f : (∀ i, α i) → β) (h : ∀ (a b : ∀ i, α i), (∀ i, a i ≈ b i) → f a = f b) : β

Full source

/-- Lift a function on `∀ i, α i` to a function on `∀ i, Quotient (S i)`. -/
def finLiftOn (q : ∀ i, Quotient (S i)) (f : (∀ i, α i) → β)
    (h : ∀ (a b : ∀ i, α i), (∀ i, a i ≈ b i) → f a = f b) : β :=
  (finChoice q).liftOn f h

Lifting a function to a finite product of quotients

Informal description

Given a finite type $\iota$ and for each $i \in \iota$ a quotient $\text{Quotient}(S_i)$ of a setoid $S_i$ on $\alpha_i$, the function $\text{finLiftOn}$ lifts a function $f : (\forall i, \alpha_i) \to \beta$ that respects the equivalence relations $S_i$ (i.e., $f(a) = f(b)$ whenever $a_i \approx b_i$ for all $i$) to a function on the product quotient $\forall i, \text{Quotient}(S_i)$.

Quotient.finLiftOn_empty theorem

[e : IsEmpty ι] (q : ∀ i, Quotient (S i)) : finLiftOn (β := β) q = fun f _ ↦ f e.elim

Full source

@[simp]
lemma finLiftOn_empty [e : IsEmpty ι] (q : ∀ i, Quotient (S i)) :
    finLiftOn (β := β) q = fun f _ ↦ f e.elim := by
  ext f h
  dsimp [finLiftOn]
  induction finChoice q using Quotient.ind
  exact h _ _ e.elim

Behavior of `finLiftOn` on Empty Index Type

Informal description

For any empty type $\iota$ and any family of quotient types $q : \forall i, \text{Quotient}(S_i)$, the function $\text{finLiftOn}$ applied to $q$ is equal to the function that takes any $f : (\forall i, \alpha_i) \to \beta$ and returns $f$ applied to the elimination of the empty type $\iota$.

Quotient.finLiftOn_mk theorem

(a : ∀ i, α i) : finLiftOn (S := S) (β := β) (⟦a ·⟧) = fun f _ ↦ f a

Full source

@[simp]
lemma finLiftOn_mk (a : ∀ i, α i) :
    finLiftOn (S := S) (β := β) (⟦a ·⟧) = fun f _ ↦ f a := by
  ext f h
  dsimp [finLiftOn]
  rw [finChoice_eq]
  rfl

Lifting Evaluation on Equivalence Classes for Finite Product Quotients

Informal description

For any function $a \colon \forall i, \alpha_i$ where each $\alpha_i$ has a setoid structure $S_i$, the lifting operation $\text{finLiftOn}$ applied to the family of equivalence classes $\llbracket a \rrbracket$ is equal to the evaluation of any function $f \colon (\forall i, \alpha_i) \to \beta$ at $a$, provided that $f$ respects the equivalence relations $S_i$.

Quotient.finChoiceEquiv definition

: (∀ i, Quotient (S i)) ≃ @Quotient (∀ i, α i) piSetoid

Full source

/-- `Quotient.finChoice` as an equivalence. -/
@[simps]
def finChoiceEquiv :
    (∀ i, Quotient (S i)) ≃ @Quotient (∀ i, α i) piSetoid where
  toFun := finChoice
  invFun := eval
  left_inv q := by
    refine induction_on_fintype_pi q (fun a ↦ ?_)
    rw [finChoice_eq]
    rfl
  right_inv q := by
    induction q using Quotient.ind
    exact finChoice_eq _

Equivalence between product of quotients and quotient of products for finite types

Informal description

Given a finite type $\iota$ and for each $i \in \iota$ a quotient $\text{Quotient}(S_i)$ of $\alpha_i$ by an equivalence relation $S_i$, there is an equivalence between: 1. The product type $\prod_{i \in \iota} \text{Quotient}(S_i)$ (functions assigning to each $i$ a quotient class) 2. The quotient $\text{Quotient}(\text{piSetoid})$ of the dependent function type $\prod_{i \in \iota} \alpha_i$ by the product equivalence relation (where two functions are equivalent if they are equivalent at every index) The equivalence is given by: - The forward map selects representatives from each quotient class to form a function in $\prod_{i \in \iota} \alpha_i$ and then takes its equivalence class - The inverse map evaluates a quotient class of functions at each index $i$ to get a quotient class in $\text{Quotient}(S_i)$

Quotient.finHRecOn definition

 {C : (∀ i, Quotient (S i)) → Sort*} (q : ∀ i, Quotient (S i)) (f : ∀ a : ∀ i, α i, C (⟦a ·⟧))
  (h : ∀ (a b : ∀ i, α i), (∀ i, a i ≈ b i) → HEq (f a) (f b)) : C q

Full source

/-- Recursion principle for quotients indexed by a finite type. -/
@[elab_as_elim]
def finHRecOn {C : (∀ i, Quotient (S i)) → Sort*}
    (q : ∀ i, Quotient (S i))
    (f : ∀ a : ∀ i, α i, C (⟦a ·⟧))
    (h : ∀ (a b : ∀ i, α i), (∀ i, a i ≈ b i) → HEq (f a) (f b)) :
    C q :=
  eval_finChoice q ▸ (finChoice q).hrecOn f h

Dependent Recursion Principle for Quotients Indexed by Finite Types

Informal description

Given a finite type $\iota$ and for each $i \in \iota$ a quotient $\text{Quotient}(S_i)$ of $\alpha_i$ by an equivalence relation $S_i$, the function $\text{finHRecOn}$ provides a dependent recursion principle. For any type family $C$ indexed by $\forall i, \text{Quotient}(S_i)$, a function $f \colon \forall a \colon \forall i, \alpha_i, C(\llbracket a \rrbracket)$, and a proof $h$ that $f$ respects the equivalence relations (i.e., for any $a, b \colon \forall i, \alpha_i$ with $a_i \approx b_i$ for all $i$, the values $f(a)$ and $f(b)$ are heterogeneously equal), the function $\text{finHRecOn}$ constructs an element of $C(q)$ for any $q \colon \forall i, \text{Quotient}(S_i)$.

Quotient.finRecOn definition

 {C : (∀ i, Quotient (S i)) → Sort*} (q : ∀ i, Quotient (S i)) (f : ∀ a : ∀ i, α i, C (⟦a ·⟧))
  (h : ∀ (a b : ∀ i, α i) (h : ∀ i, a i ≈ b i), Eq.ndrec (f a) (funext fun i ↦ Quotient.sound (h i)) = f b) : C q

Full source

/-- Recursion principle for quotients indexed by a finite type. -/
@[elab_as_elim]
def finRecOn {C : (∀ i, Quotient (S i)) → Sort*}
    (q : ∀ i, Quotient (S i))
    (f : ∀ a : ∀ i, α i, C (⟦a ·⟧))
    (h : ∀ (a b : ∀ i, α i) (h : ∀ i, a i ≈ b i),
      Eq.ndrec (f a) (funext fun i ↦ Quotient.sound (h i)) = f b) :
    C q :=
  finHRecOn q f (rec_heq_iff_heq.mp <| heq_of_eq <| h · · ·)

Dependent recursion principle for quotients indexed by finite types

Informal description

Given a finite type $\iota$ and for each $i \in \iota$ a quotient $\text{Quotient}(S_i)$ of $\alpha_i$ by an equivalence relation $S_i$, the function $\text{finRecOn}$ provides a dependent recursion principle. For any type family $C$ indexed by $\forall i, \text{Quotient}(S_i)$, a function $f \colon \forall a \colon \forall i, \alpha_i, C(\llbracket a \rrbracket)$, and a proof $h$ that $f$ respects the equivalence relations (i.e., for any $a, b \colon \forall i, \alpha_i$ with $a_i \approx b_i$ for all $i$, the values $f(a)$ and $f(b)$ are equal when transported appropriately), the function $\text{finRecOn}$ constructs an element of $C(q)$ for any $q \colon \forall i, \text{Quotient}(S_i)$.

Quotient.finHRecOn_mk theorem

{C : (∀ i, Quotient (S i)) → Sort*} (a : ∀ i, α i) : finHRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a

Full source

@[simp]
lemma finHRecOn_mk {C : (∀ i, Quotient (S i)) → Sort*}
    (a : ∀ i, α i) :
    finHRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a := by
  ext f h
  refine eq_of_heq ((eqRec_heq _ _).trans ?_)
  rw [finChoice_eq]
  rfl

Computation Rule for Dependent Recursion on Finite Product Quotients

Informal description

For any type family $C$ indexed by $\forall i, \text{Quotient}(S_i)$ and any function $a \colon \forall i, \alpha_i$, the application of $\text{finHRecOn}$ to the equivalence class $\llbracket a \rrbracket$ is equal to the function that evaluates $f$ at $a$, where $f$ is a function from $\forall i, \alpha_i$ to $C(\llbracket a \rrbracket)$ that respects the equivalence relations $S_i$.

Quotient.finRecOn_mk theorem

{C : (∀ i, Quotient (S i)) → Sort*} (a : ∀ i, α i) : finRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a

Full source

@[simp]
lemma finRecOn_mk {C : (∀ i, Quotient (S i)) → Sort*}
    (a : ∀ i, α i) :
    finRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a := by
  unfold finRecOn
  simp

Computation Rule for Recursion on Finite Product Quotients

Informal description

For any type family $C$ indexed by $\forall i, \text{Quotient}(S_i)$ and any function $a \colon \forall i, \alpha_i$, the application of the recursion principle $\text{finRecOn}$ to the equivalence class $\llbracket a \rrbracket$ is equal to the function that evaluates $f$ at $a$, where $f$ is a function from $\forall i, \alpha_i$ to $C(\llbracket a \rrbracket)$ that respects the equivalence relations $S_i$.

Trunc.finChoice definition

(q : ∀ i, Trunc (α i)) : Trunc (∀ i, α i)

Full source

/-- 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. -/
def finChoice (q : ∀ i, Trunc (α i)) : Trunc (∀ i, α i) :=
  Quotient.map' id (fun _ _ _ => trivial) (Quotient.finChoice q)

Finite choice of representatives in product truncations

Informal description

Given a finite type $\iota$ and for each $i \in \iota$ a truncation $\text{Trunc}(\alpha_i)$ of a type $\alpha_i$, the function $\text{finChoice}$ constructs an element of the truncation of the product type $\forall i, \alpha_i$. This is done by lifting a function that selects representatives from each truncation to a function on the entire product type, respecting the trivial equivalence relation (where all elements are considered equivalent).

Trunc.finChoice_eq theorem

(f : ∀ i, α i) : (Trunc.finChoice fun i => Trunc.mk (f i)) = Trunc.mk f

Full source

theorem finChoice_eq (f : ∀ i, α i) : (Trunc.finChoice fun i => Trunc.mk (f i)) = Trunc.mk f :=
  Subsingleton.elim _ _

$\text{finChoice}$ preserves truncation of functions

Informal description

For any function $f \colon \forall i, \alpha_i$, the truncation of the product type $\forall i, \alpha_i$ obtained by applying $\text{finChoice}$ to the family of truncations $\lambda i, \text{Trunc.mk}(f i)$ is equal to the truncation of $f$ itself, i.e., $\text{Trunc.mk} f$.

Trunc.finLiftOn definition

(q : ∀ i, Trunc (α i)) (f : (∀ i, α i) → β) (h : ∀ (a b : ∀ i, α i), f a = f b) : β

Full source

/-- Lift a function on `∀ i, α i` to a function on `∀ i, Trunc (α i)`. -/
def finLiftOn (q : ∀ i, Trunc (α i)) (f : (∀ i, α i) → β) (h : ∀ (a b : ∀ i, α i), f a = f b) : β :=
  Quotient.finLiftOn q f (fun _ _ _ ↦ h _ _)

Lifting a constant function to a finite product of truncations

Informal description

Given a finite type $\iota$ and for each $i \in \iota$ a truncation $\text{Trunc}(\alpha_i)$ of a type $\alpha_i$, the function $\text{finLiftOn}$ lifts a function $f : (\forall i, \alpha_i) \to \beta$ that is constant on the equivalence classes (i.e., $f(a) = f(b)$ for all $a, b$) to a function on the product truncation $\forall i, \text{Trunc}(\alpha_i)$.

Trunc.finLiftOn_empty theorem

[e : IsEmpty ι] (q : ∀ i, Trunc (α i)) : finLiftOn (β := β) q = fun f _ ↦ f e.elim

Full source

@[simp]
lemma finLiftOn_empty [e : IsEmpty ι] (q : ∀ i, Trunc (α i)) :
    finLiftOn (β := β) q = fun f _ ↦ f e.elim :=
  funext₂ fun _ _ ↦ congrFun₂ (Quotient.finLiftOn_empty q) _ _

Behavior of `finLiftOn` on Empty Index Type for Truncations

Informal description

For any empty type $\iota$ and any family of truncations $q : \forall i, \text{Trunc}(\alpha_i)$, the function $\text{finLiftOn}$ applied to $q$ is equal to the function that takes any $f : (\forall i, \alpha_i) \to \beta$ and returns $f$ applied to the elimination of the empty type $\iota$.

Trunc.finLiftOn_mk theorem

(a : ∀ i, α i) : finLiftOn (β := β) (⟦a ·⟧) = fun f _ ↦ f a

Full source

@[simp]
lemma finLiftOn_mk (a : ∀ i, α i) :
    finLiftOn (β := β) (⟦a ·⟧) = fun f _ ↦ f a :=
  funext₂ fun _ _ ↦ congrFun₂ (Quotient.finLiftOn_mk a) _ _

Evaluation of Lifted Function on Truncated Product at Canonical Representative

Informal description

For any function $a \colon \forall i, \alpha_i$, the lifting operation $\text{finLiftOn}$ applied to the family of truncations $\llbracket a \rrbracket$ is equal to the evaluation of any function $f \colon (\forall i, \alpha_i) \to \beta$ at $a$, provided that $f$ is constant on the equivalence classes (i.e., $f(a) = f(b)$ for all $a, b$).

Trunc.finChoiceEquiv definition

: (∀ i, Trunc (α i)) ≃ Trunc (∀ i, α i)

Full source

/-- `Trunc.finChoice` as an equivalence. -/
@[simps]
def finChoiceEquiv : (∀ i, Trunc (α i)) ≃ Trunc (∀ i, α i) where
  toFun := finChoice
  invFun q i := q.map (· i)
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence between finite product of truncations and truncation of finite product

Informal description

The equivalence `Trunc.finChoiceEquiv` establishes a bijection between the type of functions `∀ i, Trunc (α i)` (where each `α i` is truncated) and the truncation of the product type `Trunc (∀ i, α i)`. - The forward direction is given by `finChoice`, which selects representatives from each truncation to form an element of the product type. - The backward direction maps a truncated product `q : Trunc (∀ i, α i)` to the function `λ i, q.map (· i)`, which evaluates the product at each index `i`. Both directions are well-defined up to the trivial equivalence relation (where all elements are considered equivalent), and the composition of these maps in either order yields the identity up to this equivalence.

Trunc.finRecOn definition

 {C : (∀ i, Trunc (α i)) → Sort*} (q : ∀ i, Trunc (α i)) (f : ∀ a : ∀ i, α i, C (mk <| a ·))
  (h : ∀ (a b : ∀ i, α i), (Eq.ndrec (f a) (funext fun _ ↦ Trunc.eq _ _)) = f b) : C q

Full source

/-- Recursion principle for `Trunc`s indexed by a finite type. -/
@[elab_as_elim]
def finRecOn {C : (∀ i, Trunc (α i)) → Sort*}
    (q : ∀ i, Trunc (α i))
    (f : ∀ a : ∀ i, α i, C (mk <| a ·))
    (h : ∀ (a b : ∀ i, α i), (Eq.ndrec (f a) (funext fun _ ↦ Trunc.eq _ _)) = f b) :
    C q :=
  Quotient.finRecOn q (f ·) (fun _ _ _ ↦ h _ _)

Dependent recursion principle for truncations indexed by finite types

Informal description

Given a finite type $\iota$ and for each $i \in \iota$ a truncation $\operatorname{Trunc}(\alpha_i)$ of $\alpha_i$, the function $\operatorname{finRecOn}$ provides a dependent recursion principle. For any type family $C$ indexed by $\forall i, \operatorname{Trunc}(\alpha_i)$, a function $f \colon \forall a \colon \forall i, \alpha_i, C(\operatorname{mk}(a))$, and a proof $h$ that $f$ respects the truncation equivalence (i.e., for any $a, b \colon \forall i, \alpha_i$, the values $f(a)$ and $f(b)$ are equal when transported appropriately), the function $\operatorname{finRecOn}$ constructs an element of $C(q)$ for any $q \colon \forall i, \operatorname{Trunc}(\alpha_i)$.

Trunc.finRecOn_mk theorem

{C : (∀ i, Trunc (α i)) → Sort*} (a : ∀ i, α i) : finRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a

Full source

@[simp]
lemma finRecOn_mk {C : (∀ i, Trunc (α i)) → Sort*}
    (a : ∀ i, α i) :
    finRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a := by
  unfold finRecOn
  simp

Computation Rule for Recursion on Finite Product Truncations

Informal description

For any type family $C$ indexed by $\forall i, \operatorname{Trunc}(\alpha_i)$ and any function $a \colon \forall i, \alpha_i$, the application of the recursion principle $\operatorname{finRecOn}$ to the equivalence class $\llbracket a \rrbracket$ is equal to the function that evaluates $f$ at $a$, where $f$ is a function from $\forall i, \alpha_i$ to $C(\llbracket a \rrbracket)$ that respects the truncation equivalence.

Main definitions