From c07be8a4ce40d4870c01f17e19788c41b403e71a Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 13 Jul 2023 06:40:40 -0600 Subject: [PATCH] Enderton. Finish most equivalence class exercises. --- Bookshelf/Enderton/Set.tex | 164 +++++++++++++++++++++++--- Bookshelf/Enderton/Set/Chapter_3.lean | 116 ++++++++++++++++-- Bookshelf/Enderton/Set/Relation.lean | 21 +++- 3 files changed, 266 insertions(+), 35 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 6cbc510..9393eb7 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -3446,7 +3446,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \end{proof} -\subsection{\pending{Theorem 3Q}}% +\subsection{\unverified{Theorem 3Q}}% \hyperlabel{sub:theorem-3q} \begin{theorem}[3Q] @@ -3480,7 +3480,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. Since $F$ is compatible, $F(x_1)RF(x_2)$. Another application of \nameref{sub:lemma-3n} implies that $[F(x_1)]_R = [F(x_2)]_R$. - Thus $\hat{F}$ is be single-valued. + Thus $\hat{F}$ is single-valued. Uniqueness follows immediately from the \nameref{ref:extensionality-axiom}. @@ -3491,7 +3491,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. By \nameref{sub:lemma-3n}, $[x]_R = [y]_R$. For the sake of contradiction, suppose a function $\hat{F}$ exists satisfying \eqref{sub:theorem-3q-eq1}. - Then $\hat{F}([x]_R) = \hat{F}([y]_R)$ and $[F(x)]_R = [F(y)]_R$. + Then $\hat{F}([x]_R) = \hat{F}([y]_R)$ meaning $[F(x)]_R = [F(y)]_R$. Then \nameref{sub:lemma-3n} implies $F(x)RF(y)$, a contradiction. Therefore our original hypothesis must be incorrect. That is, there is no function $\hat{F}$ satisfying \eqref{sub:theorem-3q-eq1}. @@ -4777,10 +4777,22 @@ Assume that $F \colon \powerset{A} \rightarrow \powerset{A}$ and that $F$ has Define $$B = \bigcap\{X \subseteq A \mid F(X) \subseteq X\} \quad\text{and}\quad C = \bigcup\{X \subseteq A \mid X \subseteq F(X)\}.$$ -\begin{enumerate}[(a)] - \item Show that $F(B) = B$ and $F(C) = C$. - \item Show that if $F(X) = X$, then $B \subseteq X \subseteq C$. -\end{enumerate} + +\subsubsection{\sorry{Exercise 3.30 (a)}}% +\hyperlabel{ssub:exercise-3.30-a} + +Show that $F(B) = B$ and $F(C) = C$. + +\begin{proof} + + TODO + +\end{proof} + +\subsubsection{\sorry{Exercise 3.30 (b)}}% +\hyperlabel{ssub:exercise-3.30-b} + +Show that if $F(X) = X$, then $B \subseteq X \subseteq C$. \begin{proof} @@ -5257,7 +5269,7 @@ Show that if we start with the equivalence relation $R_\Pi$ of the preceding \end{proof} -\subsection{\sorry{Exercise 3.39}}% +\subsection{\verified{Exercise 3.39}}% \hyperlabel{sub:exercise-3.39} Assume that we start with an equivalence relation $R$ on $A$ and define $\Pi$ to @@ -5266,11 +5278,44 @@ Show that $R_\Pi$, as defined in Exercise 37, is just $R$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.exercise\_3\_39} + + By definition, + \begin{equation} + \hyperlabel{sub:exercise-3.39-eq1} + R_\Pi = \{ (x, y) \mid (\exists B \in \Pi)(x \in B \land y \in B) \}. + \end{equation} + We prove that $R_\Pi = R$. + By the \nameref{ref:extensionality-axiom}, these two sets are equal when + $$(x, y) \in R_\Pi \iff (x, y) \in R.$$ + We prove both directions of this biconditional. + + \paragraph{($\Rightarrow$)}% + + Let $(x, y) \in R_\Pi$. + By \eqref{sub:exercise-3.39-eq1}, there exists some $B \in \Pi$ such that + $x \in B$ and $y \in B$. + Since $\Pi = A / R = \{[x]_R \mid x \in A\}$, there must exist some + $z \in A$ such that $B = [z]_R$. + By definition of an \nameref{ref:equivalence-class}, $x \in [z]_R$ implies + that $zRx$ and $y \in [z]_R$ implies $zRy$. + Since $R$ is \nameref{ref:symmetric}, $xRz$. + Since $R$ is \nameref{ref:transitive}, $xRy$. + + \paragraph{($\Leftarrow$)}% + + Let $(x, y) \in R$. + By definition of an \nameref{ref:equivalence-class}, $x \in [x]_R$ and + $y \in [x]_R$. + Note also that $[x]_R \in A / R = \Pi$. + Thus there exists some $B \in \Pi$ such that $x \in B$ and $y \in B$, namely + $B = [x]_R$. + By \eqref{sub:exercise-3.39-eq1}, $(x, y) \in R_\Pi$. \end{proof} -\subsection{\pending{Exercise 3.40}}% +\subsection{\unverified{Exercise 3.40}}% \hyperlabel{sub:exercise-3.40} Define an equivalence relation $R$ on the set $P$ of positive integers by @@ -5294,25 +5339,106 @@ Is there a function $f \colon P / R \rightarrow P / R$ such that \end{proof} -\subsection{\sorry{Exercise 3.41}}% +\subsection{\unverified{Exercise 3.41}}% \hyperlabel{sub:exercise-3.41} Let $\mathbb{R}$ be the set of real numbers and define the relation $Q$ on $\mathbb{R} \times \mathbb{R}$ by $\pair{u, v}Q\pair{x, y}$ iff $u + y = x + v$. -\begin{enumerate}[(a)] - \item Show that $Q$ is an equivalence relation on - $\mathbb{R} \times \mathbb{R}$. - \item Is there a function $G \colon (\mathbb{R} \times \mathbb{R}) / Q - \rightarrow (\mathbb{R} \times \mathbb{R}) / Q$ satisfying the equation - $$G([\pair{x, y}]_Q) = [\pair{x + 2y, y + 2x}]_Q?$$ +\subsubsection{\verified{Exercise 3.41a}}% +\hyperlabel{ssub:exercise-3.41-a} -\end{enumerate} +Show that $Q$ is an equivalence relation on $\mathbb{R} \times \mathbb{R}$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.exercise\_3\_41\_a} + + We show (i) $Q$ is \nameref{ref:reflexive} on $\mathbb{R} \times \mathbb{R}$, + (ii) $Q$ is \nameref{ref:symmetric}, and (iii) $Q$ is + \nameref{ref:transitive}. + + \paragraph{(i)}% + + Let $\pair{x, y} \in R \times R$. + Since $x + y = x + y$, it immediately follows $\pair{x, y}Q\pair{x, y}$. + Thus $Q$ is reflexive on $\mathbb{R}$. + + \paragraph{(ii)}% + + Let $\pair{\pair{u, v}, \pair{x, y}} \in Q$. + Then $u + y = x + v$. + Likewise, $x + v = u + y$. + This immediately implies that $\pair{\pair{x, y}, \pair{u, v}} \in Q$. + Thus $Q$ is symmetric. + + \paragraph{(iii)}% + + Let $\pair{\pair{u, v}, \pair{x, y}} \in Q$ and + $\pair{\pair{x, y}, \pair{a, b}} \in Q$. + Then $u + y = x + v$ and $x + b = a + y$. + Rearranging terms, we have $u - v = x - y$ and $x - y = a - b$. + Thus $u - v = a - b$. + Rearranging terms once more yields $u + b = a + v$. + Thus $\pair{\pair{u, v}, \pair{a, b}} \in Q$. + Therefore $Q$ is transitive. + +\end{proof} + +\subsubsection{\unverified{Exercise 3.41b}}% +\hyperlabel{ssub:exercise-3.41-b} + +Is there a function $G \colon (\mathbb{R} \times \mathbb{R}) / Q + \rightarrow (\mathbb{R} \times \mathbb{R}) / Q$ satisfying the equation + \begin{equation} + \hyperlabel{ssub:exercise-3.41-b-eq1} + G([\pair{x, y}]_Q) = [\pair{x + 2y, y + 2x}]_Q? + \end{equation} + +\begin{proof} + + Let $f \colon \mathbb{R} \times \mathbb{R} + \rightarrow \mathbb{R} \times \mathbb{R}$ be given by + $f(\pair{x, y}) = \pair{x + 2y, y + 2x}$. + We show (i) that $f$ is \nameref{ref:compatible} with $Q$ and then (ii) + there exists such a function satisfying \eqref{ssub:exercise-3.41-b-eq1}. + + \paragraph{(i)}% + \hyperlabel{par:exercise-3.41-b-i} + + Let $\pair{u, v}, \pair{x, y} \in \mathbb{R} \times \mathbb{R}$ such that + $\pair{u, v} Q \pair{x, y}$. + Thus + \begin{equation} + \hyperlabel{ssub:exercise-3.41-b-eq2} + u + y = x + v + \end{equation} + Next consider + \begin{align*} + f(\pair{u, v}) & = \pair{u + 2v, v + 2u}, \\ + f(\pair{x, y}) & = \pair{x + 2y, y + 2x}. + \end{align*} + Then + \begin{align*} + u + y & = x + v \\ + \iff 3u + 3y & = 3x + 3v \\ + \iff (u + y) + (2u + 2y) & = (x + v) + (2x + 2v) \\ + \iff (x + v) + (2u + 2y) & = (u + y) + (2x + 2v) + & \eqref{ssub:exercise-3.41-b-eq2} \\ + \iff (x + 2y) + (v + 2u) & = (u + 2v) + (y + 2x) \\ + \iff (u + 2v) + (y + 2x) & = (x + 2y) + (v + 2u). + \end{align*} + This last equality shows $f(\pair{u, v}) \,Q\, f(\pair{x, y})$. + Thus $f$ is compatible with $Q$. + + \paragraph{(ii)}% + + By \nameref{par:exercise-3.41-b-i} and \nameref{sub:theorem-3q}, there + exists a unique $G \colon (\mathbb{R} \times \mathbb{R}) / Q \rightarrow + (\mathbb{R} \times \mathbb{R}) / Q$ satisfying + \eqref{ssub:exercise-3.41-b-eq1}. \end{proof} diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 9d05af8..6f2f93f 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -2,6 +2,7 @@ import Bookshelf.Enderton.Set.Chapter_2 import Bookshelf.Enderton.Set.OrderedPair import Bookshelf.Enderton.Set.Relation import Common.Logic.Basic +import Mathlib.Data.Real.Basic import Mathlib.Tactic.CasesM /-! # Enderton.Set.Chapter_3 @@ -1928,7 +1929,7 @@ theorem exercise_3_36 {f : Set.HRelation α β} /-- #### Exercise 3.37 -Assume that `Π` is a partition of a set `A`. Define the relation `Rₚ` as +Assume that `P` is a partition of a set `A`. Define the relation `Rₚ` as follows: ``` xRₚy ↔ (∃ B ∈ Π)(x ∈ B ∧ y ∈ B). @@ -1940,7 +1941,7 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α} (hP : isPartition P A) (Rₚ : Set.Relation α) (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B) : isEquivalence Rₚ A := by - have hR : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by + have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by ext p have (x, y) := p exact hRₚ x y @@ -1948,7 +1949,7 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α} refine ⟨?_, ?_, ?_, ?_⟩ · -- `fld Rₚ ⊆ A` show ∀ x, x ∈ fld Rₚ → x ∈ A - rw [hR] + rw [hRₚ_eq] intro x hx unfold fld dom ran at hx simp only [ @@ -1969,23 +1970,23 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α} · -- `isReflexive Rₚ A` intro x hx - rw [hR] + rw [hRₚ_eq] simp only [Set.mem_setOf_eq, and_self] exact hP.exhaustive x hx · -- `isSymmetric Rₚ` intro x y h - rw [hR] at h + rw [hRₚ_eq] at h simp only [Set.mem_setOf_eq] at h have ⟨B, hB⟩ := h - rw [hR] + rw [hRₚ_eq] simp only [Set.mem_setOf_eq] conv at hB => right; rw [and_comm] exact ⟨B, hB⟩ · -- `isTransitive Rₚ` intro x y z hx hy - rw [hR] at hx hy + rw [hRₚ_eq] at hx hy simp only [Set.mem_setOf_eq] at hx hy have ⟨B₁, hB₁⟩ := hx have ⟨B₂, hB₂⟩ := hy @@ -1999,7 +2000,7 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α} intro h' rw [Set.ext_iff] at h' exact (h' y).mp ⟨hy₁, hy₂⟩ - rw [hR] + rw [hRₚ_eq] simp only [Set.mem_setOf_eq] exact ⟨B₁, hB₁.left, hB₁.right.left, by rw [hB]; exact hB₂.right.right⟩ @@ -2013,7 +2014,7 @@ theorem exercise_3_38 {P : Set (Set α)} {A : Set α} (hP : isPartition P A) (Rₚ : Set.Relation α) (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B) : modEquiv (exercise_3_37 hP Rₚ hRₚ) = P := by - have hR : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by + have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by ext p have (x, y) := p exact hRₚ x y @@ -2030,13 +2031,13 @@ theorem exercise_3_38 {P : Set (Set α)} {A : Set α} ext y apply Iff.intro · intro hy - rw [← hx.right, hR] at hy + rw [← hx.right, hRₚ_eq] at hy have ⟨B₁, hB₁⟩ := hy have := hB'.right B₁ ⟨hB₁.left, hB₁.right.left⟩ rw [← this] exact hB₁.right.right · intro hy - rw [← hx.right, hR] + rw [← hx.right, hRₚ_eq] exact ⟨B', hB'.left.left, hB'.left.right, hy⟩ · intro hB @@ -2067,10 +2068,101 @@ theorem exercise_3_38 {P : Set (Set α)} {A : Set α} rw [this] exact hB₁.right _ = {t | (x, t) ∈ Rₚ } := by - rw [hR] + rw [hRₚ_eq] simp only [Set.mem_setOf_eq] _ = neighborhood Rₚ x := rfl +/-- #### Exercise 3.39 + +Assume that we start with an equivalence relation `R` on `A` and define `P` to +be the partition `A / R`. Show that `Rₚ`, as defined in Exercise 37, is just +`R`. +-/ +theorem exercise_3_39 {P : Set (Set α)} {R Rₚ : Set.Relation α} {A : Set α} + (hR : isEquivalence R A) (hP : P = modEquiv hR) + (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B) + : Rₚ = R := by + have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by + ext p + have (x, y) := p + exact hRₚ x y + + ext p + have (x, y) := p + apply Iff.intro + · intro hp + rw [hRₚ_eq] at hp + have ⟨B, hB, hx, hy⟩ := hp + rw [hP] at hB + have ⟨z, hz⟩ := hB + rw [← hz.right] at hx hy + exact neighborhood_mem_imp_relate hR hx hy + · intro hp + have hxA : x ∈ A := hR.b_on (Or.inl (mem_pair_imp_fst_mem_dom hp)) + have hyA : y ∈ A := hR.b_on (Or.inr (mem_pair_imp_snd_mem_ran hp)) + rw [hRₚ_eq] + have hx : x ∈ neighborhood R x := neighborhood_self_mem hR hxA + have hy : y ∈ neighborhood R x := by + rw [← neighborhood_eq_iff_mem_relate hR hxA hyA] at hp + rw [hp] + exact neighborhood_self_mem hR hyA + refine ⟨neighborhood R x, ?_, ⟨hx, hy⟩⟩ + rw [hP] + exact ⟨x, hxA, rfl⟩ +lemma test {x y z : ℝ} (h : x + y = z) : (x = z - y) := by apply? +/-- #### Exercise 3.41 (a) + +Let `ℝ` be the set of real numbers and define the realtion `Q` on `ℝ × ℝ` by +`⟨u, v⟩ Q ⟨x, y⟩` **iff** `u + y = x + v`. Show that `Q` is an equivalence +relation on `ℝ × ℝ`. +-/ +theorem exercise_3_41_a {Q : Set.Relation (ℝ × ℝ)} + (hQ : ∀ u v x y, ((u, v), (x, y)) ∈ Q ↔ u + y = x + v) + : isEquivalence Q (Set.univ : Set (ℝ × ℝ)) := by + have hQ_eq : Q = {p | p.1.1 + p.2.2 = p.2.1 + p.1.2} := by + ext p + apply Iff.intro <;> + · intro hp + rwa [hQ] at * + + refine ⟨?_, ?_, ?_, ?_⟩ + + · -- `fld Q ⊆ Set.univ` + show ∀ p, p ∈ fld Q → p ∈ Set.univ + intro _ _ + simp only [Set.mem_univ] + + · -- `isReflexive Q Set.univ` + intro (x, y) _ + rw [hQ_eq] + simp + + · -- `isSymmetric Q` + intro (u, v) (x, y) hp + rw [hQ_eq] at * + exact Eq.symm hp + + · -- `isTransitive Q` + unfold isTransitive + intro (u, v) (x, y) (a, b) h₁ h₂ + rw [hQ_eq] at * + simp at h₁ h₂ + simp + have h₁' : u - v = x - y := by + have := sub_eq_of_eq_add h₁ + rw [add_sub_right_comm] at this + exact eq_sub_of_add_eq this + have h₂' : x - y = a - b := by + have := sub_eq_of_eq_add h₂ + rw [add_sub_right_comm] at this + exact eq_sub_of_add_eq this + rw [h₂'] at h₁' + have := eq_add_of_sub_eq' h₁' + rw [← add_sub_assoc] at this + have := add_eq_of_eq_sub this + conv => right; rw [add_comm] + exact this + end Relation end Enderton.Set.Chapter_3 \ No newline at end of file diff --git a/Bookshelf/Enderton/Set/Relation.lean b/Bookshelf/Enderton/Set/Relation.lean index 0c15504..7c989e6 100644 --- a/Bookshelf/Enderton/Set/Relation.lean +++ b/Bookshelf/Enderton/Set/Relation.lean @@ -533,7 +533,7 @@ def neighborhood (R : Relation α) (x : α) := { t | (x, t) ∈ R } The neighborhood with some respect to an equivalence relation `R` on set `A` and member `x` contains `x`. -/ -theorem neighborhood_self_mem {R : Set.Relation α} {A : Set α} {x : α} +theorem neighborhood_self_mem {R : Set.Relation α} {A : Set α} (hR : isEquivalence R A) (hx : x ∈ A) : x ∈ neighborhood R x := hR.refl x hx @@ -541,7 +541,7 @@ theorem neighborhood_self_mem {R : Set.Relation α} {A : Set α} {x : α} Assume that `R` is an equivalence relation on `A` and that `x` and `y` belong to `A`. Then `[x]_R = [y]_R ↔ xRy`. -/ -theorem neighborhood_iff_mem {R : Set.Relation α} {A : Set α} {x y : α} +theorem neighborhood_eq_iff_mem_relate {R : Set.Relation α} {A : Set α} (hR : isEquivalence R A) (_ : x ∈ A) (hy : y ∈ A) : neighborhood R x = neighborhood R y ↔ (x, y) ∈ R := by apply Iff.intro @@ -558,6 +558,19 @@ theorem neighborhood_iff_mem {R : Set.Relation α} {A : Set α} {x y : α} · intro ht exact hR.trans h ht +/-- +Assume that `R` is an equivalence relation on `A`. If two sets `x` and `y` +belong to the same neighborhood, then `xRy`. +-/ +theorem neighborhood_mem_imp_relate {R : Set.Relation α} {A : Set α} + (hR : isEquivalence R A) + (hx : x ∈ neighborhood R z) (hy : y ∈ neighborhood R z) + : (x, y) ∈ R := by + unfold neighborhood at hx hy + simp only [mem_setOf_eq] at hx hy + have := hR.symm hx + exact hR.trans this hy + /-- A **partition** `Π` of a set `A` is a set of nonempty subsets of `A` that is disjoint and exhaustive. @@ -622,8 +635,8 @@ theorem modEquiv_partition {A : Set α} {R : Relation α} (hR : isEquivalence R have : z ∈ fld R := Or.inr (mem_pair_imp_snd_mem_ran hz.left) exact hR.b_on this rw [ - ← neighborhood_iff_mem hR hx.left hz_mem, - ← neighborhood_iff_mem hR hy.left hz_mem, + ← neighborhood_eq_iff_mem_relate hR hx.left hz_mem, + ← neighborhood_eq_iff_mem_relate hR hy.left hz_mem, hx.right, hy.right ] at hz rw [hz.left, hz.right] at nXY