Test 1
Throughout this problem
inductive A
| Mara | Aurelio | Andrea
deriving Fintype
(a) Find an invertible map {A \xrightarrow{f} A}, different from the identity map 1_A.
(b) Find an idempotent map {A \xrightarrow{e} A}, different from the identity map 1_A.
(c) Find another set B and two maps
B \xrightarrow{s} A \xrightarrow{r} B
for which {r \circ s = 1_B} and {s \circ r = e}. (In this part, e is still the map you chose in part (b).)
Solution: Problem 1
For part (a), we give a map f, and we show that f is invertible.
def f : A ⟶ A
| A.Mara => A.Aurelio
| A.Aurelio => A.Andrea
| A.Andrea => A.Mara
def finv : A ⟶ A
| A.Mara => A.Andrea
| A.Aurelio => A.Mara
| A.Andrea => A.Aurelio
example : IsIso f := {
out := ⊢ ∃ inv, inv ⊚ f = 𝟙 A ∧ f ⊚ inv = 𝟙 A
⊢ finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 A
⊢ finv ⊚ f = 𝟙 A⊢ f ⊚ finv = 𝟙 A
all_goals
x:A⊢ (f ⊚ finv) x = 𝟙 A x
⊢ (f ⊚ finv) A.Mara = 𝟙 A A.Mara⊢ (f ⊚ finv) A.Aurelio = 𝟙 A A.Aurelio⊢ (f ⊚ finv) A.Andrea = 𝟙 A A.Andrea ⊢ (f ⊚ finv) A.Mara = 𝟙 A A.Mara⊢ (f ⊚ finv) A.Aurelio = 𝟙 A A.Aurelio⊢ (f ⊚ finv) A.Andrea = 𝟙 A A.Andrea All goals completed! 🐙
}
For part (b), we give a map e, and we show that e is idempotent.
def e : A ⟶ A
| A.Mara => A.Mara
| A.Aurelio => A.Mara
| A.Andrea => A.Mara
instance : IsIdempotent e := {
idem := ⊢ e ⊚ e = e
x:A⊢ (e ⊚ e) x = e x
⊢ (e ⊚ e) A.Mara = e A.Mara⊢ (e ⊚ e) A.Aurelio = e A.Aurelio⊢ (e ⊚ e) A.Andrea = e A.Andrea ⊢ (e ⊚ e) A.Mara = e A.Mara⊢ (e ⊚ e) A.Aurelio = e A.Aurelio⊢ (e ⊚ e) A.Andrea = e A.Andrea All goals completed! 🐙
}
For part (c), we give a set B and maps r and s, and we show that they satisfy the required properties.
inductive B
| b
deriving Fintype
def r : A ⟶ B
| A.Mara => B.b
| A.Aurelio => B.b
| A.Andrea => B.b
def s : B ⟶ A
| B.b => A.Mara
example : r ⊚ s = 𝟙 B ∧ s ⊚ r = e := ⊢ r ⊚ s = 𝟙 B ∧ s ⊚ r = e
⊢ r ⊚ s = 𝟙 B⊢ s ⊚ r = e
⊢ r ⊚ s = 𝟙 B ⊢ r ⊚ s = 𝟙 B
All goals completed! 🐙
⊢ s ⊚ r = e ⊢ s ⊚ r = e
x:A⊢ (s ⊚ r) x = e x
⊢ (s ⊚ r) A.Mara = e A.Mara⊢ (s ⊚ r) A.Aurelio = e A.Aurelio⊢ (s ⊚ r) A.Andrea = e A.Andrea ⊢ (s ⊚ r) A.Mara = e A.Mara⊢ (s ⊚ r) A.Aurelio = e A.Aurelio⊢ (s ⊚ r) A.Andrea = e A.Andrea All goals completed! 🐙
\mathbb{R} is the set of all real numbers, and {\mathbb{R} \xrightarrow{f} \mathbb{R}} is the map given by the explicit formula {f(x) = 4x — 7} for each input x. Show that f has an inverse map. To do this, give an explicit formula for the inverse map g, and then show that
(a) {(g \circ f)(x) = x} for each real number x, and that
(b) {(f \circ g)(x) = x} for each real number x.
Solution: Problem 2
Put {g(x) = \dfrac{x + 7}{4}}; then we have
example (f : ℝ ⟶ ℝ) (hf : ∀ x : ℝ, f x = 4 * x - 7)
: ∃ g, ∀ x : ℝ, (g ⊚ f) x = x ∧ (f ⊚ g) x = x := f:ℝ ⟶ ℝhf:∀ (x : ℝ), f x = 4 * x - 7⊢ ∃ g, ∀ (x : ℝ), (g ⊚ f) x = x ∧ (f ⊚ g) x = x
f:ℝ ⟶ ℝhf:∀ (x : ℝ), f x = 4 * x - 7⊢ ∀ (x : ℝ), ((fun x ↦ (x + 7) / 4) ⊚ f) x = x ∧ (f ⊚ fun x ↦ (x + 7) / 4) x = x -- g
f:ℝ ⟶ ℝhf:∀ (x : ℝ), f x = 4 * x - 7x:ℝ⊢ ((fun x ↦ (x + 7) / 4) ⊚ f) x = x ∧ (f ⊚ fun x ↦ (x + 7) / 4) x = x
f:ℝ ⟶ ℝhf:∀ (x : ℝ), f x = 4 * x - 7x:ℝ⊢ (f x + 7) / 4 = x ∧ f ((x + 7) / 4) = x
f:ℝ ⟶ ℝhf:∀ (x : ℝ), f x = 4 * x - 7x:ℝ⊢ (f x + 7) / 4 = xf:ℝ ⟶ ℝhf:∀ (x : ℝ), f x = 4 * x - 7x:ℝ⊢ f ((x + 7) / 4) = x
f:ℝ ⟶ ℝhf:∀ (x : ℝ), f x = 4 * x - 7x:ℝ⊢ (f x + 7) / 4 = x -- Proof of part (a)
f:ℝ ⟶ ℝhf:∀ (x : ℝ), f x = 4 * x - 7x:ℝ⊢ (4 * x - 7 + 7) / 4 = x
All goals completed! 🐙
f:ℝ ⟶ ℝhf:∀ (x : ℝ), f x = 4 * x - 7x:ℝ⊢ f ((x + 7) / 4) = x -- Proof of part (b)
f:ℝ ⟶ ℝhf:∀ (x : ℝ), f x = 4 * x - 7x:ℝ⊢ 4 * ((x + 7) / 4) - 7 = x
All goals completed! 🐙