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! ๐