Article I: Sets, maps, composition

Until the introduction of the definition of category at the end of Article I, we implement all maps in the book as Lean functions.

Exercise 1 (p. 19)

Check to be sure you understand how we got diagrams (ii) and (iii) from the given diagram (i). Then fill in (iv) and (v) yourself, starting over from (i). Then check to see that (v) and (iii) are the same.

Solution: Exercise 1

For simplicity, we use types here instead of sets. We number the elements in each set/type from top to bottom (top left to bottom right for D).

inductive A
  | a₁ | a₂ | a₃

inductive B
  | b₁ | b₂ | b₃ | b₄

inductive C
  | c₁ | c₂ | c₃ | c₄ | c₅

inductive D
  | d₁ | d₂ | d₃ | d₄ | d₅ | d₆

def f : A → B
  | A.a₁ => B.b₁
  | A.a₂ => B.b₂
  | A.a₃ => B.b₃

def g : B → C
  | B.b₁ => C.c₂
  | B.b₂ => C.c₂
  | B.b₃ => C.c₄
  | B.b₄ => C.c₅

def h : C → D
  | C.c₁ => D.d₁
  | C.c₂ => D.d₁
  | C.c₃ => D.d₃
  | C.c₄ => D.d₃
  | C.c₅ => D.d₅

For diagram (iv), we have f as above and {h \circ g} as follows:

def hg : B → D
  | B.b₁ => D.d₁
  | B.b₂ => D.d₁
  | B.b₃ => D.d₃
  | B.b₄ => D.d₅

example : hg = h ∘ g := by⊢ hg = h ∘ g
  funext xhx:B⊢ hg x = (h ∘ g) x
  cases xh.b₁⊢ hg B.b₁ = (h ∘ g) B.b₁h.b₂⊢ hg B.b₂ = (h ∘ g) B.b₂h.b₃⊢ hg B.b₃ = (h ∘ g) B.b₃h.b₄⊢ hg B.b₄ = (h ∘ g) B.b₄ <;>h.b₁⊢ hg B.b₁ = (h ∘ g) B.b₁h.b₂⊢ hg B.b₂ = (h ∘ g) B.b₂h.b₃⊢ hg B.b₃ = (h ∘ g) B.b₃h.b₄⊢ hg B.b₄ = (h ∘ g) B.b₄ dsimp [g, h, hg]All goals completed! 🐙

For diagram (v), we have {(h \circ g) \circ f} as follows, which is indeed the same as {h \circ (g \circ f)} in diagram (iii):

def hgf : A → D
  | A.a₁ => D.d₁
  | A.a₂ => D.d₁
  | A.a₃ => D.d₃

example : hgf = (h ∘ g) ∘ f := by⊢ hgf = (h ∘ g) ∘ f
  funext xhx:A⊢ hgf x = ((h ∘ g) ∘ f) x
  cases xh.a₁⊢ hgf A.a₁ = ((h ∘ g) ∘ f) A.a₁h.a₂⊢ hgf A.a₂ = ((h ∘ g) ∘ f) A.a₂h.a₃⊢ hgf A.a₃ = ((h ∘ g) ∘ f) A.a₃ <;>h.a₁⊢ hgf A.a₁ = ((h ∘ g) ∘ f) A.a₁h.a₂⊢ hgf A.a₂ = ((h ∘ g) ∘ f) A.a₂h.a₃⊢ hgf A.a₃ = ((h ∘ g) ∘ f) A.a₃ dsimp [f, g, h, hgf]All goals completed! 🐙

Excerpt (p. 19)

One very useful sort of set is a 'singleton' set, a set with exactly one element.... Call this set '\mathbf{1}'.

We define \mathbf{1} in Lean as the finite set containing the single element of type Unit.

namespace CM_Finset

def One : Finset Unit := Finset.univ

end CM_Finset

Definition: Point (p. 19)

A point of a set X is a map {\mathbf{1} \rightarrow X}.

We define Point in Lean as a Map between Finsets. (The coercion allows a term inhabiting Map to be used directly as a function, so we can write f, John, and eggs below rather than f.toFun, John.toFun, and eggs.toFun.)

namespace CM_Finset

structure Map {α β : Type*} (X : Finset α) (Y : Finset β) where
  toFun : α → β
  maps_to_codomain : ∀ a : α, a ∈ X → toFun a ∈ Y

instance {α β : Type*} (X : Finset α) (Y : Finset β)
    : CoeFun (Map X Y) (fun _ ↦ α → β) where
  coe F := F.toFun

abbrev Point {β : Type*} (Y : Finset β) := Map One Y

end CM_Finset

Excerpt (p. 19)

Since a point is a map, we can compose it with another map, and get a point again.

We provide a Lean implementation below of the example given in the book on p. 19.

namespace CM_Finset

def A : Finset String := { "John", "Mary", "Sam" }
def B : Finset String := { "eggs", "coffee" }

def John : Point A := {
  toFun := fun _ ↦ "John"
  maps_to_codomain := by⊢ ∀ a ∈ One, "John" ∈ A simp [A]All goals completed! 🐙
}

def f : Map A B := {
  toFun
    | "John" => "eggs"
    | "Mary" => "eggs"
    | _ => "coffee"
  maps_to_codomain := by⊢ ∀ a ∈ A,
  (match a with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") ∈
    B
    intro _ haa✝:Stringha:a✝ ∈ A⊢ (match a✝ with
  | "John" => "eggs"
  | "Mary" => "eggs"
  | x => "coffee") ∈
  B
    dsimp [A, B] at *a✝:Stringha:a✝ ∈ {"John", "Mary", "Sam"}⊢ (match a✝ with
  | "John" => "eggs"
  | "Mary" => "eggs"
  | x => "coffee") ∈
  {"eggs", "coffee"}
    repeat rw [Finset.mem_insert] at *a✝:Stringha:a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ ∈ {"Sam"}⊢ (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") ∈
    {"coffee"}
    rw [Finset.mem_singleton] at *a✝:Stringha:a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ = "Sam"⊢ (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee"
    rcases ha with ha | ha | hainla✝:Stringha:a✝ = "John"⊢ (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee"inr.inla✝:Stringha:a✝ = "Mary"⊢ (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee"inr.inra✝:Stringha:a✝ = "Sam"⊢ (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee"
    all_goals
      subst hainr.inr⊢ (match "Sam" with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match "Sam" with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee"
      first | exact Or.inl rflinr.inr⊢ (match "Sam" with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match "Sam" with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee" | exact Or.inr rflAll goals completed! 🐙
}

def eggs : Point B := {
  toFun := fun _ ↦ "eggs"
  maps_to_codomain := by⊢ ∀ a ∈ One, "eggs" ∈ B simp [B]All goals completed! 🐙
}

example : f ∘ John = eggs := rfl

end CM_Finset

Replacing Finset with Set broadens the application to any set, not just finite sets.

namespace CM_Set

def One : Set Unit := Set.univ

structure Map {α β : Type*} (X : Set α) (Y : Set β) where
  toFun : α → β
  maps_to_codomain : ∀ a : α, a ∈ X → toFun a ∈ Y

instance {α β : Type*} (X : Set α) (Y : Set β)
    : CoeFun (Map X Y) (fun _ ↦ α → β) where
  coe F := F.toFun

abbrev Point {β : Type*} (Y : Set β) := Map One Y

def A : Set String := { "John", "Mary", "Sam" }
def B : Set String := { "eggs", "coffee" }

def John : Point A := {
  toFun := fun _ ↦ "John"
  maps_to_codomain := by⊢ ∀ a ∈ One, "John" ∈ A simp [A]All goals completed! 🐙
}

def f : Map A B := {
  toFun
    | "John" => "eggs"
    | "Mary" => "eggs"
    | _ => "coffee"
  maps_to_codomain := by⊢ ∀ a ∈ A,
  (match a with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") ∈
    B
    intro _ haa✝:Stringha:a✝ ∈ A⊢ (match a✝ with
  | "John" => "eggs"
  | "Mary" => "eggs"
  | x => "coffee") ∈
  B
    dsimp [A, B] at *a✝:Stringha:a✝ ∈ {"John", "Mary", "Sam"}⊢ (match a✝ with
  | "John" => "eggs"
  | "Mary" => "eggs"
  | x => "coffee") ∈
  {"eggs", "coffee"}
    repeat rw [Set.mem_insert_iff] at *a✝:Stringha:a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ ∈ {"Sam"}⊢ (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") ∈
    {"coffee"}
    rw [Set.mem_singleton_iff] at *a✝:Stringha:a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ = "Sam"⊢ (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee"
    rcases ha with ha | ha | hainla✝:Stringha:a✝ = "John"⊢ (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee"inr.inla✝:Stringha:a✝ = "Mary"⊢ (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee"inr.inra✝:Stringha:a✝ = "Sam"⊢ (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee"
    all_goals
      subst hainr.inr⊢ (match "Sam" with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match "Sam" with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee"
      first | exact Or.inl rflinr.inr⊢ (match "Sam" with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match "Sam" with
    | "John" => "eggs"
    | "Mary" => "eggs"
    | x => "coffee") =
    "coffee" | exact Or.inr rflAll goals completed! 🐙
}

def eggs : Point B := {
  toFun := fun _ ↦ "eggs"
  maps_to_codomain := by⊢ ∀ a ∈ One, "eggs" ∈ B simp [B]All goals completed! 🐙
}

example : f ∘ John = eggs := rfl

end CM_Set

Using types instead of sets is cleaner and further broadens the application to any type, not just sets.

def One := Unit

namespace CM_Type

def Point (Y : Type) := One → Y

def A := { a : String // a = "John" ∨ a = "Mary" ∨ a = "Sam" }
def B := { b : String // b = "eggs" ∨ b = "coffee" }

def John : Point A := fun _ ↦ ⟨"John", byx✝:One⊢ "John" = "John" ∨ "John" = "Mary" ∨ "John" = "Sam" simpAll goals completed! 🐙⟩

def f : A → B := fun a ↦
  match a.val with
  | "John" => ⟨"eggs", bya:A⊢ "eggs" = "eggs" ∨ "eggs" = "coffee" simpAll goals completed! 🐙⟩
  | "Mary" => ⟨"eggs", bya:A⊢ "eggs" = "eggs" ∨ "eggs" = "coffee" simpAll goals completed! 🐙⟩
  | _ => ⟨"coffee", bya:Ax✝:String⊢ "coffee" = "eggs" ∨ "coffee" = "coffee" simpAll goals completed! 🐙⟩

def eggs : Point B := fun _ ↦ ⟨"eggs", byx✝:One⊢ "eggs" = "eggs" ∨ "eggs" = "coffee" simpAll goals completed! 🐙⟩

example : f ∘ John = eggs := rfl

end CM_Type

We lift our definition for the function Point between types to the morphism Point in the category Type for later use. Note the application of ⟶ (\hom) for the morphism type instead of → (\r) for the function arrow.

def Point (Y : Type) := One ⟶ Y

For Exercises 2–5 which follow, rather than providing exhaustive lists of maps, it seems more useful at this stage to introduce what the book calls Alysia's formula, even though that formula doesn't appear until slightly later (on pp. 33–34). The formula states that the number of different maps between two finite sets is equal to the number of elements in the codomain raised to the power of the number of elements in the domain — that is, the number of maps is {(\#\beta)^{(\#\alpha)}}, where {\#\alpha} is the size of the domain \alpha and {\#\beta} is the size of the codomain \beta.

def Alysia's_formula (α β : Type*) [Fintype α] [Fintype β] : ℕ :=
  Fintype.card β ^ Fintype.card α

Exercise 2 (p. 20)

How many different maps f are there with domain A and codomain B?

Solution: Exercise 2

By Alysia's formula, we have {(\#B)^{(\#A)} = 2^3 = 8} different maps.

open CM_Finset

8#eval Alysia's_formula A B

Exercise 3 (p. 20)

Same, but for maps {A \xrightarrow{f} A}?

Solution: Exercise 3

By Alysia's formula, we have {(\#A)^{(\#A)} = 3^3 = 27} different maps.

open CM_Finset

27#eval Alysia's_formula A A

Exercise 4 (p. 20)

Same, but for maps {B \xrightarrow{f} A}?

Solution: Exercise 4

By Alysia's formula, we have {(\#A)^{(\#B)} = 3^2 = 9} different maps.

open CM_Finset

9#eval Alysia's_formula B A

Exercise 5 (p. 20)

Same, but for maps {B \xrightarrow{f} B}?

Solution: Exercise 5

By Alysia's formula, we have {(\#B)^{(\#B)} = 2^2 = 4} different maps.

open CM_Finset

4#eval Alysia's_formula B B

Exercises 6 and 7 concern idempotence, which the book formally introduces later on p. 54. For the purpose of these two exercises (and again aiming to avoid exhaustive lists of maps), we introduce the formula \sum_{k=0}^{n} {n \choose k} k^{n-k} for the total number of possible idempotents on a finite set. (See the Wikipedia article on idempotence for additional information.)

def idempotentCount (α : Type) [Fintype α] : ℕ :=
  let n := Fintype.card α
  ∑ k ∈ Finset.range (n + 1), (n.choose k) * k ^ (n - k)

Exercise 6 (p. 20)

How many maps {A \xrightarrow{f} A} satisfy {f \circ f = f}?

Solution: Exercise 6

By the formula above, we have 10 different maps.

open CM_Finset

10#eval idempotentCount A

Exercise 7 (p. 20)

How many maps {B \xrightarrow{g} B} satisfy {g \circ g = g}?

Solution: Exercise 7

By the formula above, we have 3 different maps.

open CM_Finset

3#eval idempotentCount B

Exercise 8 (p. 20)

Can you find a pair of maps {A \xrightarrow{f} B \xrightarrow{g} A} for which {g \circ f = 1_A}? If so, how many such pairs?

Solution: Exercise 8

No such pair exists, since the image of 1_A has 3 elements, but the image of {g \circ f} has only 2 elements.

open CM_Finset

We will begin using the Lean notation 𝟙 X, for the identity morphism on X, after we finish Article I and start working with morphisms and categories; for now, though, since we are still operating with functions and sets, we must define the identity map on A explicitly.

def idA : Map A A := {
  toFun := id
  maps_to_codomain := by⊢ ∀ a ∈ A, id a ∈ A
    intro _ haa✝:Stringha:a✝ ∈ A⊢ id a✝ ∈ A
    dsimp [A] at *a✝:Stringha:a✝ ∈ {"John", "Mary", "Sam"}⊢ a✝ ∈ {"John", "Mary", "Sam"}
    repeat rw [Finset.mem_insert] at *a✝:Stringha:a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ ∈ {"Sam"}⊢ a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ ∈ {"Sam"}
    rw [Finset.mem_singleton] at *a✝:Stringha:a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ = "Sam"⊢ a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ = "Sam"
    rcases ha with ha | ha | hainla✝:Stringha:a✝ = "John"⊢ a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ = "Sam"inr.inla✝:Stringha:a✝ = "Mary"⊢ a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ = "Sam"inr.inra✝:Stringha:a✝ = "Sam"⊢ a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ = "Sam"
    all_goals
      subst hainr.inr⊢ "Sam" = "John" ∨ "Sam" = "Mary" ∨ "Sam" = "Sam"
      first
      | exact Or.inl rflinr.inr⊢ "Sam" = "John" ∨ "Sam" = "Mary" ∨ "Sam" = "Sam"
      | exact Or.inr (Or.inl rfl)inr.inr⊢ "Sam" = "John" ∨ "Sam" = "Mary" ∨ "Sam" = "Sam"
      | exact Or.inr (Or.inr rfl)All goals completed! 🐙
}

open Finset in
example : ¬(∃ f : Map A B, ∃ g : Map B A, g ∘ f = idA) := by⊢ ¬∃ f g, g.toFun ∘ f.toFun = idA.toFun
  -- Convert to the equivalent statement ∀ f g, g ∘ f ≠ idA
  push_neg⊢ ∀ (f : Map A B) (g : Map B A), g.toFun ∘ f.toFun ≠ idA.toFun
  -- Assume that g ∘ f = idA for some f, g, and derive a contradiction
  intro f gf:Map A Bg:Map B A⊢ g.toFun ∘ f.toFun ≠ idA.toFun h_eqf:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFun⊢ False
  -- Since the functions g ∘ f and idA are equal, so are their images
  have h_img_eq
      : (image g (image f A)).card = (image idA A).card := by⊢ ¬∃ f g, g.toFun ∘ f.toFun = idA.toFun
    rw [image_image, h_eq]All goals completed! 🐙
  -- But the image of g(f(A)) has at most 2 elements,
  have h_card_gfA : (image g (image f A)).card ≤ 2 := by⊢ ¬∃ f g, g.toFun ∘ f.toFun = idA.toFun
    apply le_transaf:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))⊢ #(image g.toFun (image f.toFun A)) ≤ ?baf:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))⊢ ?b ≤ 2bf:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))⊢ ℕ
    ·af:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))⊢ #(image g.toFun (image f.toFun A)) ≤ ?b exact card_image_leAll goals completed! 🐙
    ·af:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))⊢ ?b ≤ 2 change (image f A).card ≤ B.cardaf:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))⊢ #(image f.toFun A) ≤ #B
      apply card_le_carda.af:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))⊢ image f.toFun A ⊆ B
      intro _ hfaa.af:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))a✝:Stringhfa:a✝ ∈ image f.toFun A⊢ a✝ ∈ B
      rw [mem_image] at hfaa.af:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))a✝:Stringhfa:∃ a ∈ A, f.toFun a = a✝⊢ a✝ ∈ B
      obtain ⟨a, ha, rfl⟩ := hfaa.af:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))a:Stringha:a ∈ A⊢ f.toFun a ∈ B
      exact f.maps_to_codomain a haAll goals completed! 🐙
  -- while the image of idA(A) has 3 elements
  have h_card_idA : (image idA A).card = 3 := rflf:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))h_card_gfA:#(image g.toFun (image f.toFun A)) ≤ 2 := 
  le_trans card_image_le
    (id
      (card_le_card fun ⦃a⦄ hfa ↦
        Exists.casesOn (Eq.mp (congrArg (fun _a ↦ _a) (propext mem_image)) hfa) fun a_1 h ↦
          And.casesOn h fun ha right ↦ right ▸ f.maps_to_codomain a_1 ha))h_card_idA:#(image idA.toFun A) = 3 := rfl⊢ False
  -- So we have a contradiction
  rw [h_img_eq, h_card_idA] at h_card_gfAf:Map A Bg:Map B Ah_eq:g.toFun ∘ f.toFun = idA.toFunh_img_eq:#(image g.toFun (image f.toFun A)) = #(image idA.toFun A) := 
  Eq.mpr (id (congrArg (fun _a ↦ #_a = #(image idA.toFun A)) image_image))
    (Eq.mpr (id (congrArg (fun _a ↦ #(image _a A) = #(image idA.toFun A)) h_eq)) (Eq.refl #(image idA.toFun A)))h_card_gfA:3 ≤ 2h_card_idA:#(image idA.toFun A) = 3⊢ False
  contradictionAll goals completed! 🐙

Exercise 9 (p. 20)

Can you find a pair of maps {B \xrightarrow{h} A \xrightarrow{k} B} for which {k \circ h = 1_B}? If so, how many such pairs?

Solution: Exercise 9

We define one pair h, k.

open CM_Finset

def h : Map B A := {
  toFun
    | "eggs" => "John"
    | _ => "Mary"
  maps_to_codomain := by⊢ ∀ a ∈ B,
  (match a with
    | "eggs" => "John"
    | x => "Mary") ∈
    A
    intro _ hba✝:Stringhb:a✝ ∈ B⊢ (match a✝ with
  | "eggs" => "John"
  | x => "Mary") ∈
  A
    dsimp [A, B] at *a✝:Stringhb:a✝ ∈ {"eggs", "coffee"}⊢ (match a✝ with
  | "eggs" => "John"
  | x => "Mary") ∈
  {"John", "Mary", "Sam"}
    repeat rw [Finset.mem_insert] at *a✝:Stringhb:a✝ = "eggs" ∨ a✝ ∈ {"coffee"}⊢ (match a✝ with
    | "eggs" => "John"
    | x => "Mary") =
    "John" ∨
  (match a✝ with
      | "eggs" => "John"
      | x => "Mary") =
      "Mary" ∨
    (match a✝ with
      | "eggs" => "John"
      | x => "Mary") ∈
      {"Sam"}
    rw [Finset.mem_singleton] at *a✝:Stringhb:a✝ = "eggs" ∨ a✝ = "coffee"⊢ (match a✝ with
    | "eggs" => "John"
    | x => "Mary") =
    "John" ∨
  (match a✝ with
      | "eggs" => "John"
      | x => "Mary") =
      "Mary" ∨
    (match a✝ with
      | "eggs" => "John"
      | x => "Mary") =
      "Sam"
    rcases hb with hb | hbinla✝:Stringhb:a✝ = "eggs"⊢ (match a✝ with
    | "eggs" => "John"
    | x => "Mary") =
    "John" ∨
  (match a✝ with
      | "eggs" => "John"
      | x => "Mary") =
      "Mary" ∨
    (match a✝ with
      | "eggs" => "John"
      | x => "Mary") =
      "Sam"inra✝:Stringhb:a✝ = "coffee"⊢ (match a✝ with
    | "eggs" => "John"
    | x => "Mary") =
    "John" ∨
  (match a✝ with
      | "eggs" => "John"
      | x => "Mary") =
      "Mary" ∨
    (match a✝ with
      | "eggs" => "John"
      | x => "Mary") =
      "Sam"
    all_goals
      subst hbinr⊢ (match "coffee" with
    | "eggs" => "John"
    | x => "Mary") =
    "John" ∨
  (match "coffee" with
      | "eggs" => "John"
      | x => "Mary") =
      "Mary" ∨
    (match "coffee" with
      | "eggs" => "John"
      | x => "Mary") =
      "Sam"
      first | exact Or.inl rflinr⊢ (match "coffee" with
    | "eggs" => "John"
    | x => "Mary") =
    "John" ∨
  (match "coffee" with
      | "eggs" => "John"
      | x => "Mary") =
      "Mary" ∨
    (match "coffee" with
      | "eggs" => "John"
      | x => "Mary") =
      "Sam" | exact Or.inr (Or.inl rfl)All goals completed! 🐙
}

def k : Map A B := {
  toFun
    | "John" => "eggs"
    | _ => "coffee"
  maps_to_codomain := by⊢ ∀ a ∈ A,
  (match a with
    | "John" => "eggs"
    | x => "coffee") ∈
    B
    intro _ haa✝:Stringha:a✝ ∈ A⊢ (match a✝ with
  | "John" => "eggs"
  | x => "coffee") ∈
  B
    dsimp [A, B] at *a✝:Stringha:a✝ ∈ {"John", "Mary", "Sam"}⊢ (match a✝ with
  | "John" => "eggs"
  | x => "coffee") ∈
  {"eggs", "coffee"}
    repeat rw [Finset.mem_insert] at *a✝:Stringha:a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ ∈ {"Sam"}⊢ (match a✝ with
    | "John" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | x => "coffee") ∈
    {"coffee"}
    rw [Finset.mem_singleton] at *a✝:Stringha:a✝ = "John" ∨ a✝ = "Mary" ∨ a✝ = "Sam"⊢ (match a✝ with
    | "John" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | x => "coffee") =
    "coffee"
    rcases ha with ha | ha | hainla✝:Stringha:a✝ = "John"⊢ (match a✝ with
    | "John" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | x => "coffee") =
    "coffee"inr.inla✝:Stringha:a✝ = "Mary"⊢ (match a✝ with
    | "John" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | x => "coffee") =
    "coffee"inr.inra✝:Stringha:a✝ = "Sam"⊢ (match a✝ with
    | "John" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "John" => "eggs"
    | x => "coffee") =
    "coffee"
    all_goals
      subst hainr.inr⊢ (match "Sam" with
    | "John" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match "Sam" with
    | "John" => "eggs"
    | x => "coffee") =
    "coffee"
      first | exact Or.inl rflinr.inr⊢ (match "Sam" with
    | "John" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match "Sam" with
    | "John" => "eggs"
    | x => "coffee") =
    "coffee" | exact Or.inr rflAll goals completed! 🐙
}

We define the identity map on B explicitly (see the earlier comment under Exercise 8).

def idB : Map B B := {
  toFun
    | "eggs" => "eggs"
    | _ => "coffee"
  maps_to_codomain := by⊢ ∀ a ∈ B,
  (match a with
    | "eggs" => "eggs"
    | x => "coffee") ∈
    B
    intro _ hba✝:Stringhb:a✝ ∈ B⊢ (match a✝ with
  | "eggs" => "eggs"
  | x => "coffee") ∈
  B
    dsimp [B] at *a✝:Stringhb:a✝ ∈ {"eggs", "coffee"}⊢ (match a✝ with
  | "eggs" => "eggs"
  | x => "coffee") ∈
  {"eggs", "coffee"}
    rw [Finset.mem_insert, Finset.mem_singleton] at *a✝:Stringhb:a✝ = "eggs" ∨ a✝ = "coffee"⊢ (match a✝ with
    | "eggs" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "eggs" => "eggs"
    | x => "coffee") =
    "coffee"
    rcases hb with hb | hbinla✝:Stringhb:a✝ = "eggs"⊢ (match a✝ with
    | "eggs" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "eggs" => "eggs"
    | x => "coffee") =
    "coffee"inra✝:Stringhb:a✝ = "coffee"⊢ (match a✝ with
    | "eggs" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match a✝ with
    | "eggs" => "eggs"
    | x => "coffee") =
    "coffee"
    all_goals
      subst hbinr⊢ (match "coffee" with
    | "eggs" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match "coffee" with
    | "eggs" => "eggs"
    | x => "coffee") =
    "coffee"
      first | exact Or.inl rflinr⊢ (match "coffee" with
    | "eggs" => "eggs"
    | x => "coffee") =
    "eggs" ∨
  (match "coffee" with
    | "eggs" => "eggs"
    | x => "coffee") =
    "coffee" | exact Or.inr rflAll goals completed! 🐙
}

A proof that {k ∘ h = 1_B} holds for our pair h, k is given below. (We define a macro for a repeated sequence of tactics to keep the proof concise.)

syntax "eval_map" Lean.Parser.Tactic.rwRule : tactic

macro_rules
  | `(tactic| eval_map $fn_name) =>
    `(tactic| (
        rw [$fn_name]
        dsimp only [DFunLike.coe]
        split
        · contradiction
        · rfl
      )
    )

example : k ∘ h = idB := by⊢ k.toFun ∘ h.toFun = idB.toFun
  funext xhx:String⊢ (k.toFun ∘ h.toFun) x = idB.toFun x
  rw [Function.comp_apply]hx:String⊢ k.toFun (h.toFun x) = idB.toFun x
  by_cases h_x_eggs : x = "eggs"posx:Stringh_x_eggs:x = "eggs"⊢ k.toFun (h.toFun x) = idB.toFun xnegx:Stringh_x_eggs:¬x = "eggs"⊢ k.toFun (h.toFun x) = idB.toFun x
  ·posx:Stringh_x_eggs:x = "eggs"⊢ k.toFun (h.toFun x) = idB.toFun x rw [h_x_eggs]posx:Stringh_x_eggs:x = "eggs"⊢ k.toFun (h.toFun "eggs") = idB.toFun "eggs"
    have h_eval : h "eggs" = "John" := rflposx:Stringh_x_eggs:x = "eggs"h_eval:h.toFun "eggs" = "John" := rfl⊢ k.toFun (h.toFun "eggs") = idB.toFun "eggs"
    have k_eval : k "John" = "eggs" := rflposx:Stringh_x_eggs:x = "eggs"h_eval:h.toFun "eggs" = "John" := rflk_eval:k.toFun "John" = "eggs" := rfl⊢ k.toFun (h.toFun "eggs") = idB.toFun "eggs"
    have idB_eval : idB "eggs" = "eggs" := rflposx:Stringh_x_eggs:x = "eggs"h_eval:h.toFun "eggs" = "John" := rflk_eval:k.toFun "John" = "eggs" := rflidB_eval:idB.toFun "eggs" = "eggs" := rfl⊢ k.toFun (h.toFun "eggs") = idB.toFun "eggs"
    rw [h_eval, k_eval, idB_eval]All goals completed! 🐙
  ·negx:Stringh_x_eggs:¬x = "eggs"⊢ k.toFun (h.toFun x) = idB.toFun x have h_eval : h x = "Mary" := by⊢ k.toFun ∘ h.toFun = idB.toFun eval_map hAll goals completed! 🐙
    have k_eval : k "Mary" = "coffee" := by⊢ k.toFun ∘ h.toFun = idB.toFun eval_map kAll goals completed! 🐙
    have idB_eval : idB x = "coffee" := by⊢ k.toFun ∘ h.toFun = idB.toFun eval_map idBAll goals completed! 🐙
    rw [h_eval, k_eval, idB_eval]All goals completed! 🐙

There are 12 such pairs: h(\mathit{eggs}) can take any one of three distinct values in A, leaving h(\mathit{coffee}) to take one of the two remaining values, which together gives {3 \times 2 = 6} combinations; and for each combination, k can map the element in A that is not in the image of h to either \mathit{eggs} or \mathit{coffee}.

1. Guide

Definition: Category (p. 21)

A category consists of the DATA:

(1) OBJECTS

(2) MAPS

(3) For each map f, one object as DOMAIN of f and one object as CODOMAIN of f

(4) For each object A an IDENTITY MAP, which has domain A and codomain A

(5) For each pair of maps {A \xrightarrow{f} B \xrightarrow{g} C}, a COMPOSITE MAP map {A \xrightarrow{g \;\mathrm{following}\; f} C}

satisfying the following RULES:

(i) IDENTITY LAWS: If {A \xrightarrow{f} B}, then {1_B \circ f = f} and {f \circ 1_A = f}

(ii) ASSOCIATIVE LAW: If {A \xrightarrow{f} B \xrightarrow{g} C \xrightarrow{h} D}, then {(h \circ g) \circ f = h \circ (g \circ f)}

We print the mathlib definition of Category below for reference.

class CategoryTheory.Category.{v, u} (obj : Type u) : Type (max u (v + 1))
number of parameters: 1
parents:
  CategoryTheory.Category.toCategoryStruct : CategoryStruct.{v, u} obj
fields:
  Quiver.Hom : obj → obj → Type v
  CategoryTheory.CategoryStruct.id : (X : obj) → X ⟶ X
  CategoryTheory.CategoryStruct.comp : {X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
  CategoryTheory.Category.id_comp : ∀ {X Y : obj} (f : X ⟶ Y), f ⊚ 𝟙 X = f := by
    cat_disch
  CategoryTheory.Category.comp_id : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 Y ⊚ f = f := by
    cat_disch
  CategoryTheory.Category.assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), h ⊚ g ⊚ f = (h ⊚ g) ⊚ f := by
    cat_disch
constructor:
  CategoryTheory.Category.mk.{v, u} {obj : Type u} [toCategoryStruct : CategoryStruct.{v, u} obj]
    (id_comp : ∀ {X Y : obj} (f : X ⟶ Y), f ⊚ 𝟙 X = f := by cat_disch)
    (comp_id : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 Y ⊚ f = f := by cat_disch)
    (assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), h ⊚ g ⊚ f = (h ⊚ g) ⊚ f := by cat_disch) :
    Category.{v, u} obj
field notation resolution order:
  CategoryTheory.Category, CategoryTheory.CategoryStruct, Quiver#print Category

class CategoryTheory.Category.{v, u} (obj : Type u) : Type (max u (v + 1))
number of parameters: 1
parents:
  CategoryTheory.Category.toCategoryStruct : CategoryStruct.{v, u} obj
fields:
  Quiver.Hom : obj → obj → Type v
  CategoryTheory.CategoryStruct.id : (X : obj) → X ⟶ X
  CategoryTheory.CategoryStruct.comp : {X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
  CategoryTheory.Category.id_comp : ∀ {X Y : obj} (f : X ⟶ Y), f ⊚ 𝟙 X = f := by
    cat_disch
  CategoryTheory.Category.comp_id : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 Y ⊚ f = f := by
    cat_disch
  CategoryTheory.Category.assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), h ⊚ g ⊚ f = (h ⊚ g) ⊚ f := by
    cat_disch
constructor:
  CategoryTheory.Category.mk.{v, u} {obj : Type u} [toCategoryStruct : CategoryStruct.{v, u} obj]
    (id_comp : ∀ {X Y : obj} (f : X ⟶ Y), f ⊚ 𝟙 X = f := by cat_disch)
    (comp_id : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 Y ⊚ f = f := by cat_disch)
    (assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), h ⊚ g ⊚ f = (h ⊚ g) ⊚ f := by cat_disch) :
    Category.{v, u} obj
field notation resolution order:
  CategoryTheory.Category, CategoryTheory.CategoryStruct, Quiver