[Merged by Bors] - feat(topology/discrete_quotient): Add a few lemmas about discrete quotients

[adamtopaz]

This PR adds the discrete_quotient.map construction and generally improves on the discrete_quotient API.

---

[jcommelin]

LGTM

[jcommelin]

Suggested change

	@[simp]
	lemma comap_id : S.comap (continuous_id : continuous (id : X → X)) = S := by {ext, refl}
	@[simp]
	lemma comap_comp {Z : Type*} [topological_space Z] {g : Z → Y} (cont' : continuous g) :
	S.comap (continuous.comp cont cont') = (S.comap cont).comap cont' := by {ext, refl}
	@[simp]
	lemma comap_id : S.comap (continuous_id : continuous (id : X → X)) = S := by { ext, refl }
	@[simp]
	lemma comap_comp {Z : Type*} [topological_space Z] {g : Z → Y} (cont' : continuous g) :
	S.comap (continuous.comp cont cont') = (S.comap cont).comap cont' := by { ext, refl }

[jcommelin]

Suggested change

	lemma of_le_refl {A : discrete_quotient X} : of_le (le_refl A) = id := by {ext ⟨⟩, refl}
	lemma of_le_refl_apply {A : discrete_quotient X} (a : A) : of_le (le_refl A) a = a := by simp
	@[simp]
	lemma of_le_comp {A B C : discrete_quotient X} (h1 : A ≤ B) (h2 : B ≤ C) :
	of_le (le_trans h1 h2) = of_le h2 ∘ of_le h1 := by {ext ⟨⟩, refl}
	lemma of_le_refl {A : discrete_quotient X} : of_le (le_refl A) = id := by { ext ⟨⟩, refl }
	lemma of_le_refl_apply {A : discrete_quotient X} (a : A) : of_le (le_refl A) a = a := by simp
	@[simp]
	lemma of_le_comp {A B C : discrete_quotient X} (h1 : A ≤ B) (h2 : B ≤ C) :
	of_le (le_trans h1 h2) = of_le h2 ∘ of_le h1 := by { ext ⟨⟩, refl }

[jcommelin]

Suggested change

	lemma map_id : map (le_rel_id A) = id := by {ext ⟨⟩, refl}
	@[simp]
	lemma map_comp {Z : Type*} [topological_space Z] {g : Z → Y} {cont' : continuous g}
	{C : discrete_quotient Z} (h1 : le_rel cont' C A) (h2 : le_rel cont A B) :
	map (le_rel_comp h1 h2) = map h2 ∘ map h1 := by {ext ⟨⟩, refl}
	@[simp]
	lemma of_le_map {C : discrete_quotient X} (cond : le_rel cont A B) (h : B ≤ C) :
	map (le_rel_trans cond h) = of_le h ∘ map cond := by {ext ⟨⟩, refl}
	@[simp]
	lemma of_le_map_apply {C : discrete_quotient X} (cond : le_rel cont A B) (h : B ≤ C) (a : A) :
	map (le_rel_trans cond h) a = of_le h (map cond a) := by {rcases a, refl}
	@[simp]
	lemma map_of_le {C : discrete_quotient Y} (cond : le_rel cont A B) (h : C ≤ A) :
	map (le_trans h cond) = map cond ∘ of_le h := by {ext ⟨⟩, refl}
	@[simp]
	lemma map_of_le_apply {C : discrete_quotient Y} (cond : le_rel cont A B) (h : C ≤ A) (c : C) :
	map (le_trans h cond) c = map cond (of_le h c) := by {rcases c, refl}
	lemma map_id : map (le_rel_id A) = id := by { ext ⟨⟩, refl }
	@[simp]
	lemma map_comp {Z : Type*} [topological_space Z] {g : Z → Y} {cont' : continuous g}
	{C : discrete_quotient Z} (h1 : le_rel cont' C A) (h2 : le_rel cont A B) :
	map (le_rel_comp h1 h2) = map h2 ∘ map h1 := by { ext ⟨⟩, refl }
	@[simp]
	lemma of_le_map {C : discrete_quotient X} (cond : le_rel cont A B) (h : B ≤ C) :
	map (le_rel_trans cond h) = of_le h ∘ map cond := by { ext ⟨⟩, refl }
	@[simp]
	lemma of_le_map_apply {C : discrete_quotient X} (cond : le_rel cont A B) (h : B ≤ C) (a : A) :
	map (le_rel_trans cond h) a = of_le h (map cond a) := by { rcases a, refl }
	@[simp]
	lemma map_of_le {C : discrete_quotient Y} (cond : le_rel cont A B) (h : C ≤ A) :
	map (le_trans h cond) = map cond ∘ of_le h := by { ext ⟨⟩, refl }
	@[simp]
	lemma map_of_le_apply {C : discrete_quotient Y} (cond : le_rel cont A B) (h : C ≤ A) (c : C) :
	map (le_trans h cond) c = map cond (of_le h c) := by { rcases c, refl }

[jcommelin]

@adamtopaz I think the style guide prefers a bit more spacing: by { tac1, tac2 }.

[adamtopaz]

@adamtopaz I think the style guide prefers a bit more spacing: by { tac1, tac2 }.

Sorry... old habits die hard. I think I got them all.

[jcommelin]

Thanks 🎉

bors merge

[bors]

This PR was included in a batch that was canceled, it will be automatically retried

[bors]

Canceled.

[PatrickMassot]

bors merge

[bors]

This PR was included in a batch that was canceled, it will be automatically retried

[bors]

This PR was included in a batch that timed out, it will be automatically retried

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests