This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 299
/
quotient.lean
88 lines (78 loc) · 3.39 KB
/
quotient.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import data.fintype.basic
/-!
# Quotients of families indexed by a finite type
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
This file provides `quotient.fin_choice`, a mechanism to go from a finite family of quotients
to a quotient of finite families.
## Main definitions
* `quotient.fin_choice`
-/
/-- An auxiliary function for `quotient.fin_choice`. 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`. -/
def quotient.fin_choice_aux {ι : Type*} [decidable_eq ι]
{α : ι → Type*} [S : ∀ i, setoid (α i)] :
Π (l : list ι), (Π i ∈ l, quotient (S i)) → @quotient (Π i ∈ l, α i) (by apply_instance)
| [] f := ⟦λ i, false.elim⟧
| (i :: l) f := begin
refine quotient.lift_on₂ (f i (list.mem_cons_self _ _))
(quotient.fin_choice_aux l (λ j h, f j (list.mem_cons_of_mem _ h)))
_ _,
exact λ a l, ⟦λ j h,
if e : j = i then by rw e; exact a else
l _ (h.resolve_left e)⟧,
refine λ a₁ l₁ a₂ l₂ h₁ h₂, quotient.sound (λ j h, _),
by_cases e : j = i; simp [e],
{ subst j, exact h₁ },
{ exact h₂ _ _ }
end
theorem quotient.fin_choice_aux_eq {ι : Type*} [decidable_eq ι]
{α : ι → Type*} [S : ∀ i, setoid (α i)] :
∀ (l : list ι) (f : Π i ∈ l, α i), quotient.fin_choice_aux l (λ i h, ⟦f i h⟧) = ⟦f⟧
| [] f := quotient.sound (λ i h, h.elim)
| (i :: l) f := begin
simp [quotient.fin_choice_aux, quotient.fin_choice_aux_eq l],
refine quotient.sound (λ j h, _),
by_cases e : j = i; simp [e],
subst j, refl
end
/-- 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. -/
def quotient.fin_choice {ι : Type*} [decidable_eq ι] [fintype ι]
{α : ι → Type*} [S : ∀ i, setoid (α i)]
(f : Π i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
quotient.lift_on (@quotient.rec_on _ _ (λ l : multiset ι,
@quotient (Π i ∈ l, α i) (by apply_instance))
finset.univ.1
(λ l, quotient.fin_choice_aux l (λ i _, f i))
(λ a b h, begin
have := λ a, quotient.fin_choice_aux_eq a (λ i h, quotient.out (f i)),
simp [quotient.out_eq] at this,
simp [this],
let g := λ a:multiset ι, ⟦λ (i : ι) (h : i ∈ a), quotient.out (f i)⟧,
refine eq_of_heq ((eq_rec_heq _ _).trans (_ : g a == g b)),
congr' 1, exact quotient.sound h,
end))
(λ f, ⟦λ i, f i (finset.mem_univ _)⟧)
(λ a b h, quotient.sound $ λ i, h _ _)
theorem quotient.fin_choice_eq {ι : Type*} [decidable_eq ι] [fintype ι]
{α : ι → Type*} [∀ i, setoid (α i)]
(f : Π i, α i) : quotient.fin_choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
begin
let q, swap, change quotient.lift_on q _ _ = _,
have : q = ⟦λ i h, f i⟧,
{ dsimp only [q],
exact quotient.induction_on
(@finset.univ ι _).1 (λ l, quotient.fin_choice_aux_eq _ _) },
simp [this], exact setoid.refl _
end