From 559951cd0e861fe41629d4e93ecef11cffb6502d Mon Sep 17 00:00:00 2001 From: prakol16 Date: Fri, 31 Dec 2021 22:23:23 +0000 Subject: [PATCH] feat(data/quot): Add quotient pi induction (#11137) I am planning to use this later to show that the (pi) product of homotopy classes of paths is well-defined, and prove properties about that product. Co-authored-by: prakol16 --- src/data/quot.lean | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/data/quot.lean b/src/data/quot.lean index 988a4928fdd17..8b5e2c379a0bd 100644 --- a/src/data/quot.lean +++ b/src/data/quot.lean @@ -249,6 +249,8 @@ by rw [← quotient.eq_mk_iff_out, quotient.out_eq] x.out = y.out ↔ x = y := ⟨λ h, quotient.out_equiv_out.1 $ h ▸ setoid.refl _, λ h, h ▸ rfl⟩ +section pi + instance pi_setoid {ι : Sort*} {α : ι → Sort*} [∀ i, setoid (α i)] : setoid (Π i, α i) := { r := λ a b, ∀ i, a i ≈ b i, iseqv := ⟨ @@ -262,10 +264,21 @@ noncomputable def quotient.choice {ι : Type*} {α : ι → Type*} [S : Π i, se (f : Π i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) := ⟦λ i, (f i).out⟧ -theorem quotient.choice_eq {ι : Type*} {α : ι → Type*} [Π i, setoid (α i)] +@[simp] theorem quotient.choice_eq {ι : Type*} {α : ι → Type*} [Π i, setoid (α i)] (f : Π i, α i) : quotient.choice (λ i, ⟦f i⟧) = ⟦f⟧ := quotient.sound $ λ i, quotient.mk_out _ +@[elab_as_eliminator] lemma quotient.induction_on_pi + {ι : Type*} {α : ι → Sort*} [s : ∀ i, setoid (α i)] + {p : (Π i, quotient (s i)) → Prop} (f : Π i, quotient (s i)) + (h : ∀ a : Π i, α i, p (λ i, ⟦a i⟧)) : p f := +begin + rw ← (funext (λ i, quotient.out_eq (f i)) : (λ i, ⟦(f i).out⟧) = f), + apply h, +end + +end pi + lemma nonempty_quotient_iff (s : setoid α) : nonempty (quotient s) ↔ nonempty α := ⟨assume ⟨a⟩, quotient.induction_on a nonempty.intro, assume ⟨a⟩, ⟨⟦a⟧⟩⟩