Session 4: Division of maps: Isomorphisms

2. Inverses versus reciprocals

Definition: Inverse, Isomorphism (p. 61)

If {A \xrightarrow{f} B}, an inverse for f is a map {B \xrightarrow{g} A} satisfying both g \circ f = 1_A \quad\text{and}\quad f \circ g = 1_B. If f has an inverse, we say that f is an isomorphism or invertible map.

See the original presentation of these definitions at the beginning of Article II.

Theorem (uniqueness of inverses) (p. 61)

Any map f has at most one inverse.

Proof (p. 61)

Say {A \xrightarrow{f} B}, and suppose that both {B \xrightarrow{g} A} and {B \xrightarrow{h} A} are inverses for f; so g \circ f = 1_A \quad\text{and}\quad f \circ g = 1_B,\\\ h \circ f = 1_A \quad\text{and}\quad f \circ h = 1_B. We only need two of these equations to prove that g and h are the same: g = 1_A \circ g = (h \circ f) \circ g = h \circ (f \circ g) = h \circ 1_B = h.

See the Lean implementation uniqueness_of_inverses under the original presentation of this theorem in Article II.

4. A small zoo of isomorphisms in other categories

In some of the Exercises that follow, we start to make use of mathlib's implementation of the Category class (see the definition of category at the end of Article I) ahead of our more extensive reliance on it in later Articles and Sessions.

Exercise 1 (p. 66)

Finish checking that d is an isomorphism in our category by showing that {h \circ d} and {d \circ h} are indeed identity maps.

Solution: Exercise 1

To begin tackling this Exercise, we first define an abstract algebraic object as a type equipped with a carrier set and a 'combining-rule', which operates on elements of the carrier set (and which has the closure property).

structure AlgebraicObj where
  t : Type
  carrier : Set t
  oper : t → t → t
  oper_mem {a b} : a ∈ carrier → b ∈ carrier → oper a b ∈ carrier

Next we register a Category instance for our algebraic object, defining maps/morphisms between algebraic objects as morphisms between their underlying types that map elements of the domain carrier set to elements of the codomain carrier set and that respect the combining-rules.

instance : Category AlgebraicObj where
  Hom X Y := {
    f : X.t ⟶ Y.t //
        (∀ x ∈ X.carrier, f x ∈ Y.carrier) -- maps to codomain
        ∧ (∀ x₁ ∈ X.carrier, -- respects combining-rules
             ∀ x₂ ∈ X.carrier, f (X.oper x₁ x₂) = Y.oper (f x₁) (f x₂))
  }
  id X := ⟨
    𝟙 X.t,
    byX:AlgebraicObj⊢ (∀ x ∈ X.carrier, 𝟙 X.t x ∈ X.carrier) ∧
  ∀ x₁ ∈ X.carrier, ∀ x₂ ∈ X.carrier, 𝟙 X.t (X.oper x₁ x₂) = X.oper (𝟙 X.t x₁) (𝟙 X.t x₂)
      constructorleftX:AlgebraicObj⊢ ∀ x ∈ X.carrier, 𝟙 X.t x ∈ X.carrierrightX:AlgebraicObj⊢ ∀ x₁ ∈ X.carrier, ∀ x₂ ∈ X.carrier, 𝟙 X.t (X.oper x₁ x₂) = X.oper (𝟙 X.t x₁) (𝟙 X.t x₂)
      ·leftX:AlgebraicObj⊢ ∀ x ∈ X.carrier, 𝟙 X.t x ∈ X.carrier intro _ hxleftX:AlgebraicObjx✝:X.thx:x✝ ∈ X.carrier⊢ 𝟙 X.t x✝ ∈ X.carrier
        exact hxAll goals completed! 🐙
      ·rightX:AlgebraicObj⊢ ∀ x₁ ∈ X.carrier, ∀ x₂ ∈ X.carrier, 𝟙 X.t (X.oper x₁ x₂) = X.oper (𝟙 X.t x₁) (𝟙 X.t x₂) introsrightX:AlgebraicObjx₁✝:X.ta✝¹:x₁✝ ∈ X.carrierx₂✝:X.ta✝:x₂✝ ∈ X.carrier⊢ 𝟙 X.t (X.oper x₁✝ x₂✝) = X.oper (𝟙 X.t x₁✝) (𝟙 X.t x₂✝)
        rflAll goals completed! 🐙
  ⟩
  comp := by⊢ {X Y Z : AlgebraicObj} →
  { f //
      (∀ x ∈ X.carrier, f x ∈ Y.carrier) ∧
        ∀ x₁ ∈ X.carrier, ∀ x₂ ∈ X.carrier, f (X.oper x₁ x₂) = Y.oper (f x₁) (f x₂) } →
    { f //
        (∀ x ∈ Y.carrier, f x ∈ Z.carrier) ∧
          ∀ x₁ ∈ Y.carrier, ∀ x₂ ∈ Y.carrier, f (Y.oper x₁ x₂) = Z.oper (f x₁) (f x₂) } →
      { f //
        (∀ x ∈ X.carrier, f x ∈ Z.carrier) ∧
          ∀ x₁ ∈ X.carrier, ∀ x₂ ∈ X.carrier, f (X.oper x₁ x₂) = Z.oper (f x₁) (f x₂) }
    rintro _ _ _ ⟨f, hf⟩ ⟨g, hg⟩X✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.thf:(∀ x ∈ X✝.carrier, f x ∈ Y✝.carrier) ∧ ∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)g:Y✝.t ⟶ Z✝.thg:(∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrier) ∧ ∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)⊢ { f //
  (∀ x ∈ X✝.carrier, f x ∈ Z✝.carrier) ∧
    ∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Z✝.oper (f x₁) (f x₂) }
    exact ⟨
      g ⊚ f,
      byX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.thf:(∀ x ∈ X✝.carrier, f x ∈ Y✝.carrier) ∧ ∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)g:Y✝.t ⟶ Z✝.thg:(∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrier) ∧ ∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)⊢ (∀ x ∈ X✝.carrier, (g ⊚ f) x ∈ Z✝.carrier) ∧
  ∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, (g ⊚ f) (X✝.oper x₁ x₂) = Z✝.oper ((g ⊚ f) x₁) ((g ⊚ f) x₂)
        obtain ⟨hf_mtc, hf_comb⟩ := hfX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thg:(∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrier) ∧ ∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)hf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)⊢ (∀ x ∈ X✝.carrier, (g ⊚ f) x ∈ Z✝.carrier) ∧
  ∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, (g ⊚ f) (X✝.oper x₁ x₂) = Z✝.oper ((g ⊚ f) x₁) ((g ⊚ f) x₂)
        obtain ⟨hg_mtc, hg_comb⟩ := hgX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)⊢ (∀ x ∈ X✝.carrier, (g ⊚ f) x ∈ Z✝.carrier) ∧
  ∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, (g ⊚ f) (X✝.oper x₁ x₂) = Z✝.oper ((g ⊚ f) x₁) ((g ⊚ f) x₂)
        constructorleftX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)⊢ ∀ x ∈ X✝.carrier, (g ⊚ f) x ∈ Z✝.carrierrightX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)⊢ ∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, (g ⊚ f) (X✝.oper x₁ x₂) = Z✝.oper ((g ⊚ f) x₁) ((g ⊚ f) x₂)
        ·leftX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)⊢ ∀ x ∈ X✝.carrier, (g ⊚ f) x ∈ Z✝.carrier intro x hxleftX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)x:X✝.thx:x ∈ X✝.carrier⊢ (g ⊚ f) x ∈ Z✝.carrier
          exact hg_mtc (f x) (hf_mtc x hx)All goals completed! 🐙
        ·rightX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)⊢ ∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, (g ⊚ f) (X✝.oper x₁ x₂) = Z✝.oper ((g ⊚ f) x₁) ((g ⊚ f) x₂) intro x₁ hx₁rightX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)x₁:X✝.thx₁:x₁ ∈ X✝.carrier⊢ ∀ x₂ ∈ X✝.carrier, (g ⊚ f) (X✝.oper x₁ x₂) = Z✝.oper ((g ⊚ f) x₁) ((g ⊚ f) x₂) x₂rightX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)x₁:X✝.thx₁:x₁ ∈ X✝.carrierx₂:X✝.t⊢ x₂ ∈ X✝.carrier → (g ⊚ f) (X✝.oper x₁ x₂) = Z✝.oper ((g ⊚ f) x₁) ((g ⊚ f) x₂) hx₂rightX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)x₁:X✝.thx₁:x₁ ∈ X✝.carrierx₂:X✝.thx₂:x₂ ∈ X✝.carrier⊢ (g ⊚ f) (X✝.oper x₁ x₂) = Z✝.oper ((g ⊚ f) x₁) ((g ⊚ f) x₂)
          dsimprightX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)x₁:X✝.thx₁:x₁ ∈ X✝.carrierx₂:X✝.thx₂:x₂ ∈ X✝.carrier⊢ g (f (X✝.oper x₁ x₂)) = Z✝.oper (g (f x₁)) (g (f x₂))
          have h₁ := hf_comb x₁ hx₁ x₂ hx₂rightX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)x₁:X✝.thx₁:x₁ ∈ X✝.carrierx₂:X✝.thx₂:x₂ ∈ X✝.carrierh₁:f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂) := hf_comb x₁ hx₁ x₂ hx₂⊢ g (f (X✝.oper x₁ x₂)) = Z✝.oper (g (f x₁)) (g (f x₂))
          rw [h₁]rightX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)x₁:X✝.thx₁:x₁ ∈ X✝.carrierx₂:X✝.thx₂:x₂ ∈ X✝.carrierh₁:f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂) := hf_comb x₁ hx₁ x₂ hx₂⊢ g (Y✝.oper (f x₁) (f x₂)) = Z✝.oper (g (f x₁)) (g (f x₂))
          have h₂ :=
            hg_comb (f x₁) (hf_mtc x₁ hx₁) (f x₂) (hf_mtc x₂ hx₂)rightX✝:AlgebraicObjY✝:AlgebraicObjZ✝:AlgebraicObjf:X✝.t ⟶ Y✝.tg:Y✝.t ⟶ Z✝.thf_mtc:∀ x ∈ X✝.carrier, f x ∈ Y✝.carrierhf_comb:∀ x₁ ∈ X✝.carrier, ∀ x₂ ∈ X✝.carrier, f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂)hg_mtc:∀ x ∈ Y✝.carrier, g x ∈ Z✝.carrierhg_comb:∀ x₁ ∈ Y✝.carrier, ∀ x₂ ∈ Y✝.carrier, g (Y✝.oper x₁ x₂) = Z✝.oper (g x₁) (g x₂)x₁:X✝.thx₁:x₁ ∈ X✝.carrierx₂:X✝.thx₂:x₂ ∈ X✝.carrierh₁:f (X✝.oper x₁ x₂) = Y✝.oper (f x₁) (f x₂) := hf_comb x₁ hx₁ x₂ hx₂h₂:g (Y✝.oper (f x₁) (f x₂)) = Z✝.oper (g (f x₁)) (g (f x₂)) := hg_comb (f x₁) (hf_mtc x₁ hx₁) (f x₂) (hf_mtc x₂ hx₂)⊢ g (Y✝.oper (f x₁) (f x₂)) = Z✝.oper (g (f x₁)) (g (f x₂))
          rw [h₂]All goals completed! 🐙
    ⟩

Lastly we define the concrete algebraic object of real numbers with addition as the combining-rule.

def RealAdd : AlgebraicObj := {
  t := ℝ
  carrier := Set.univ
  oper := (· + ·)
  oper_mem := fun _ _ ↦ Set.mem_univ _
}

We are now ready to complete the Exercise by defining d and h as morphisms in our category and showing that they are inverses.

def d : RealAdd ⟶ RealAdd := ⟨
  fun (x : ℝ) ↦ 2 * x,
  by⊢ (∀ x ∈ RealAdd.carrier, (fun x ↦ 2 * x) x ∈ RealAdd.carrier) ∧
  ∀ x₁ ∈ RealAdd.carrier,
    ∀ x₂ ∈ RealAdd.carrier,
      (fun x ↦ 2 * x) (RealAdd.oper x₁ x₂) = RealAdd.oper ((fun x ↦ 2 * x) x₁) ((fun x ↦ 2 * x) x₂)
    constructorleft⊢ ∀ x ∈ RealAdd.carrier, (fun x ↦ 2 * x) x ∈ RealAdd.carrierright⊢ ∀ x₁ ∈ RealAdd.carrier,
  ∀ x₂ ∈ RealAdd.carrier, (fun x ↦ 2 * x) (RealAdd.oper x₁ x₂) = RealAdd.oper ((fun x ↦ 2 * x) x₁) ((fun x ↦ 2 * x) x₂)
    ·left⊢ ∀ x ∈ RealAdd.carrier, (fun x ↦ 2 * x) x ∈ RealAdd.carrier exact fun _ _ ↦ Set.mem_univ _All goals completed! 🐙
    ·right⊢ ∀ x₁ ∈ RealAdd.carrier,
  ∀ x₂ ∈ RealAdd.carrier, (fun x ↦ 2 * x) (RealAdd.oper x₁ x₂) = RealAdd.oper ((fun x ↦ 2 * x) x₁) ((fun x ↦ 2 * x) x₂) introsrightx₁✝:RealAdd.ta✝¹:x₁✝ ∈ RealAdd.carrierx₂✝:RealAdd.ta✝:x₂✝ ∈ RealAdd.carrier⊢ (fun x ↦ 2 * x) (RealAdd.oper x₁✝ x₂✝) = RealAdd.oper ((fun x ↦ 2 * x) x₁✝) ((fun x ↦ 2 * x) x₂✝)
      dsimp [RealAdd]rightx₁✝:RealAdd.ta✝¹:x₁✝ ∈ RealAdd.carrierx₂✝:RealAdd.ta✝:x₂✝ ∈ RealAdd.carrier⊢ 2 * (x₁✝ + x₂✝) = 2 * x₁✝ + 2 * x₂✝
      ringAll goals completed! 🐙
⟩

noncomputable def h : RealAdd ⟶ RealAdd := ⟨
  fun (x : ℝ) ↦ x / 2,
  by⊢ (∀ x ∈ RealAdd.carrier, (fun x ↦ x / 2) x ∈ RealAdd.carrier) ∧
  ∀ x₁ ∈ RealAdd.carrier,
    ∀ x₂ ∈ RealAdd.carrier,
      (fun x ↦ x / 2) (RealAdd.oper x₁ x₂) = RealAdd.oper ((fun x ↦ x / 2) x₁) ((fun x ↦ x / 2) x₂)
    constructorleft⊢ ∀ x ∈ RealAdd.carrier, (fun x ↦ x / 2) x ∈ RealAdd.carrierright⊢ ∀ x₁ ∈ RealAdd.carrier,
  ∀ x₂ ∈ RealAdd.carrier, (fun x ↦ x / 2) (RealAdd.oper x₁ x₂) = RealAdd.oper ((fun x ↦ x / 2) x₁) ((fun x ↦ x / 2) x₂)
    ·left⊢ ∀ x ∈ RealAdd.carrier, (fun x ↦ x / 2) x ∈ RealAdd.carrier exact fun _ _ ↦ Set.mem_univ _All goals completed! 🐙
    ·right⊢ ∀ x₁ ∈ RealAdd.carrier,
  ∀ x₂ ∈ RealAdd.carrier, (fun x ↦ x / 2) (RealAdd.oper x₁ x₂) = RealAdd.oper ((fun x ↦ x / 2) x₁) ((fun x ↦ x / 2) x₂) introsrightx₁✝:RealAdd.ta✝¹:x₁✝ ∈ RealAdd.carrierx₂✝:RealAdd.ta✝:x₂✝ ∈ RealAdd.carrier⊢ (fun x ↦ x / 2) (RealAdd.oper x₁✝ x₂✝) = RealAdd.oper ((fun x ↦ x / 2) x₁✝) ((fun x ↦ x / 2) x₂✝)
      dsimp [RealAdd]rightx₁✝:RealAdd.ta✝¹:x₁✝ ∈ RealAdd.carrierx₂✝:RealAdd.ta✝:x₂✝ ∈ RealAdd.carrier⊢ (x₁✝ + x₂✝) / 2 = x₁✝ / 2 + x₂✝ / 2
      ringAll goals completed! 🐙
⟩

example : IsIso d := {
  out := by⊢ ∃ inv, inv ⊚ d = 𝟙 RealAdd ∧ d ⊚ inv = 𝟙 RealAdd
    use hh⊢ h ⊚ d = 𝟙 RealAdd ∧ d ⊚ h = 𝟙 RealAdd
    constructorh.left⊢ h ⊚ d = 𝟙 RealAddh.right⊢ d ⊚ h = 𝟙 RealAdd
    ·h.left⊢ h ⊚ d = 𝟙 RealAdd show h ⊚ d = 𝟙 RealAddh.left⊢ h ⊚ d = 𝟙 RealAdd
      have h₀ : h.val ∘ d.val = id := by⊢ ∃ inv, inv ⊚ d = 𝟙 RealAdd ∧ d ⊚ inv = 𝟙 RealAdd
        funext xhx:RealAdd.t⊢ (↑h ∘ ↑d) x = id x
        dsimp [d, h, RealAdd]hx:RealAdd.t⊢ 2 * x / 2 = x
        ringAll goals completed! 🐙
      exact Subtype.ext h₀All goals completed! 🐙
    ·h.right⊢ d ⊚ h = 𝟙 RealAdd show d ⊚ h = 𝟙 RealAddh.right⊢ d ⊚ h = 𝟙 RealAdd
      have h₀ : d.val ∘ h.val = id := by⊢ ∃ inv, inv ⊚ d = 𝟙 RealAdd ∧ d ⊚ inv = 𝟙 RealAdd
        funext xhx:RealAdd.t⊢ (↑d ∘ ↑h) x = id x
        dsimp [d, h, RealAdd]hx:RealAdd.t⊢ 2 * (x / 2) = x
        ringAll goals completed! 🐙
      exact Subtype.ext h₀All goals completed! 🐙
}

Exercise 2 (p. 66)

Find an isomorphism (\{\textit{odd}, \textit{even}\}, +) \xrightarrow{f} (\{\textit{positive}, \textit{negative}\}, \times). Hint: There are only two invertible maps of sets from {\{\textit{odd}, \textit{even}\}} to {\{\textit{pos.}, \textit{neg.}\}}. One of them 'respects the combining rules', but the other doesn't.

Solution: Exercise 2

For this Exercise, we continue to use the category of algebraic objects we defined in Exercise 1.

Define addition for parity and multiplication for sign, and allow use of + and * notation.

inductive Parity
  | odd | even

def add : Parity → Parity → Parity
  | Parity.odd, Parity.odd => Parity.even
  | Parity.odd, Parity.even => Parity.odd
  | Parity.even, Parity.odd => Parity.odd
  | Parity.even, Parity.even => Parity.even

instance : Add Parity where
  add := add

inductive Sign
  | pos | neg

def mul : Sign → Sign → Sign
  | Sign.pos, Sign.pos => Sign.pos
  | Sign.pos, Sign.neg => Sign.neg
  | Sign.neg, Sign.pos => Sign.neg
  | Sign.neg, Sign.neg => Sign.pos

instance : Mul Sign where
  mul := mul

Create algebraic objects for parity with addition and sign with multiplication.

def parityAdd : AlgebraicObj := {
  t := Parity
  carrier := Set.univ
  oper := (· + ·)
  oper_mem := fun _ _ ↦ Set.mem_univ _
}

def signMul : AlgebraicObj := {
  t := Sign
  carrier := Set.univ
  oper := (· * ·)
  oper_mem := fun _ _ ↦ Set.mem_univ _
}

Propose a map f from parity to sign, and its inverse, and form the corresponding morphisms between algebraic objects.

def f' : Parity ⟶ Sign
  | Parity.odd => Sign.neg
  | Parity.even => Sign.pos

def finv' : Sign ⟶ Parity
  | Sign.pos => Parity.even
  | Sign.neg => Parity.odd

def f : parityAdd ⟶ signMul := ⟨
  f',
  by⊢ (∀ x ∈ parityAdd.carrier, f' x ∈ signMul.carrier) ∧
  ∀ x₁ ∈ parityAdd.carrier, ∀ x₂ ∈ parityAdd.carrier, f' (parityAdd.oper x₁ x₂) = signMul.oper (f' x₁) (f' x₂)
    constructorleft⊢ ∀ x ∈ parityAdd.carrier, f' x ∈ signMul.carrierright⊢ ∀ x₁ ∈ parityAdd.carrier, ∀ x₂ ∈ parityAdd.carrier, f' (parityAdd.oper x₁ x₂) = signMul.oper (f' x₁) (f' x₂)
    ·left⊢ ∀ x ∈ parityAdd.carrier, f' x ∈ signMul.carrier exact fun _ _ ↦ Set.mem_univ _All goals completed! 🐙
    ·right⊢ ∀ x₁ ∈ parityAdd.carrier, ∀ x₂ ∈ parityAdd.carrier, f' (parityAdd.oper x₁ x₂) = signMul.oper (f' x₁) (f' x₂) intro a _righta:parityAdd.ta✝:a ∈ parityAdd.carrier⊢ ∀ x₂ ∈ parityAdd.carrier, f' (parityAdd.oper a x₂) = signMul.oper (f' a) (f' x₂) brighta:parityAdd.ta✝:a ∈ parityAdd.carrierb:parityAdd.t⊢ b ∈ parityAdd.carrier → f' (parityAdd.oper a b) = signMul.oper (f' a) (f' b) _righta:parityAdd.ta✝¹:a ∈ parityAdd.carrierb:parityAdd.ta✝:b ∈ parityAdd.carrier⊢ f' (parityAdd.oper a b) = signMul.oper (f' a) (f' b)
      cases aright.oddb:parityAdd.ta✝¹:b ∈ parityAdd.carriera✝:Parity.odd ∈ parityAdd.carrier⊢ f' (parityAdd.oper Parity.odd b) = signMul.oper (f' Parity.odd) (f' b)right.evenb:parityAdd.ta✝¹:b ∈ parityAdd.carriera✝:Parity.even ∈ parityAdd.carrier⊢ f' (parityAdd.oper Parity.even b) = signMul.oper (f' Parity.even) (f' b) <;>right.oddb:parityAdd.ta✝¹:b ∈ parityAdd.carriera✝:Parity.odd ∈ parityAdd.carrier⊢ f' (parityAdd.oper Parity.odd b) = signMul.oper (f' Parity.odd) (f' b)right.evenb:parityAdd.ta✝¹:b ∈ parityAdd.carriera✝:Parity.even ∈ parityAdd.carrier⊢ f' (parityAdd.oper Parity.even b) = signMul.oper (f' Parity.even) (f' b) cases bright.even.odda✝¹:Parity.even ∈ parityAdd.carriera✝:Parity.odd ∈ parityAdd.carrier⊢ f' (parityAdd.oper Parity.even Parity.odd) = signMul.oper (f' Parity.even) (f' Parity.odd)right.even.evena✝¹:Parity.even ∈ parityAdd.carriera✝:Parity.even ∈ parityAdd.carrier⊢ f' (parityAdd.oper Parity.even Parity.even) = signMul.oper (f' Parity.even) (f' Parity.even) <;>right.odd.odda✝¹:Parity.odd ∈ parityAdd.carriera✝:Parity.odd ∈ parityAdd.carrier⊢ f' (parityAdd.oper Parity.odd Parity.odd) = signMul.oper (f' Parity.odd) (f' Parity.odd)right.odd.evena✝¹:Parity.odd ∈ parityAdd.carriera✝:Parity.even ∈ parityAdd.carrier⊢ f' (parityAdd.oper Parity.odd Parity.even) = signMul.oper (f' Parity.odd) (f' Parity.even)right.even.odda✝¹:Parity.even ∈ parityAdd.carriera✝:Parity.odd ∈ parityAdd.carrier⊢ f' (parityAdd.oper Parity.even Parity.odd) = signMul.oper (f' Parity.even) (f' Parity.odd)right.even.evena✝¹:Parity.even ∈ parityAdd.carriera✝:Parity.even ∈ parityAdd.carrier⊢ f' (parityAdd.oper Parity.even Parity.even) = signMul.oper (f' Parity.even) (f' Parity.even) rflAll goals completed! 🐙
⟩

def finv : signMul ⟶ parityAdd := ⟨
  finv',
  by⊢ (∀ x ∈ signMul.carrier, finv' x ∈ parityAdd.carrier) ∧
  ∀ x₁ ∈ signMul.carrier, ∀ x₂ ∈ signMul.carrier, finv' (signMul.oper x₁ x₂) = parityAdd.oper (finv' x₁) (finv' x₂)
    constructorleft⊢ ∀ x ∈ signMul.carrier, finv' x ∈ parityAdd.carrierright⊢ ∀ x₁ ∈ signMul.carrier, ∀ x₂ ∈ signMul.carrier, finv' (signMul.oper x₁ x₂) = parityAdd.oper (finv' x₁) (finv' x₂)
    ·left⊢ ∀ x ∈ signMul.carrier, finv' x ∈ parityAdd.carrier exact fun _ _ ↦ Set.mem_univ _All goals completed! 🐙
    ·right⊢ ∀ x₁ ∈ signMul.carrier, ∀ x₂ ∈ signMul.carrier, finv' (signMul.oper x₁ x₂) = parityAdd.oper (finv' x₁) (finv' x₂) intro a _righta:signMul.ta✝:a ∈ signMul.carrier⊢ ∀ x₂ ∈ signMul.carrier, finv' (signMul.oper a x₂) = parityAdd.oper (finv' a) (finv' x₂) brighta:signMul.ta✝:a ∈ signMul.carrierb:signMul.t⊢ b ∈ signMul.carrier → finv' (signMul.oper a b) = parityAdd.oper (finv' a) (finv' b) _righta:signMul.ta✝¹:a ∈ signMul.carrierb:signMul.ta✝:b ∈ signMul.carrier⊢ finv' (signMul.oper a b) = parityAdd.oper (finv' a) (finv' b)
      cases aright.posb:signMul.ta✝¹:b ∈ signMul.carriera✝:Sign.pos ∈ signMul.carrier⊢ finv' (signMul.oper Sign.pos b) = parityAdd.oper (finv' Sign.pos) (finv' b)right.negb:signMul.ta✝¹:b ∈ signMul.carriera✝:Sign.neg ∈ signMul.carrier⊢ finv' (signMul.oper Sign.neg b) = parityAdd.oper (finv' Sign.neg) (finv' b) <;>right.posb:signMul.ta✝¹:b ∈ signMul.carriera✝:Sign.pos ∈ signMul.carrier⊢ finv' (signMul.oper Sign.pos b) = parityAdd.oper (finv' Sign.pos) (finv' b)right.negb:signMul.ta✝¹:b ∈ signMul.carriera✝:Sign.neg ∈ signMul.carrier⊢ finv' (signMul.oper Sign.neg b) = parityAdd.oper (finv' Sign.neg) (finv' b) cases bright.neg.posa✝¹:Sign.neg ∈ signMul.carriera✝:Sign.pos ∈ signMul.carrier⊢ finv' (signMul.oper Sign.neg Sign.pos) = parityAdd.oper (finv' Sign.neg) (finv' Sign.pos)right.neg.nega✝¹:Sign.neg ∈ signMul.carriera✝:Sign.neg ∈ signMul.carrier⊢ finv' (signMul.oper Sign.neg Sign.neg) = parityAdd.oper (finv' Sign.neg) (finv' Sign.neg) <;>right.pos.posa✝¹:Sign.pos ∈ signMul.carriera✝:Sign.pos ∈ signMul.carrier⊢ finv' (signMul.oper Sign.pos Sign.pos) = parityAdd.oper (finv' Sign.pos) (finv' Sign.pos)right.pos.nega✝¹:Sign.pos ∈ signMul.carriera✝:Sign.neg ∈ signMul.carrier⊢ finv' (signMul.oper Sign.pos Sign.neg) = parityAdd.oper (finv' Sign.pos) (finv' Sign.neg)right.neg.posa✝¹:Sign.neg ∈ signMul.carriera✝:Sign.pos ∈ signMul.carrier⊢ finv' (signMul.oper Sign.neg Sign.pos) = parityAdd.oper (finv' Sign.neg) (finv' Sign.pos)right.neg.nega✝¹:Sign.neg ∈ signMul.carriera✝:Sign.neg ∈ signMul.carrier⊢ finv' (signMul.oper Sign.neg Sign.neg) = parityAdd.oper (finv' Sign.neg) (finv' Sign.neg) rflAll goals completed! 🐙
⟩

Give a proof that our proposed map f is indeed an isomorphism.

example : IsIso f := {
  out := by⊢ ∃ inv, inv ⊚ f = 𝟙 parityAdd ∧ f ⊚ inv = 𝟙 signMul
    use finvh⊢ finv ⊚ f = 𝟙 parityAdd ∧ f ⊚ finv = 𝟙 signMul
    constructorh.left⊢ finv ⊚ f = 𝟙 parityAddh.right⊢ f ⊚ finv = 𝟙 signMul
    ·h.left⊢ finv ⊚ f = 𝟙 parityAdd have h₀ : finv.val ∘ f.val = id := by⊢ ∃ inv, inv ⊚ f = 𝟙 parityAdd ∧ f ⊚ inv = 𝟙 signMul
        funext xhx:parityAdd.t⊢ (↑finv ∘ ↑f) x = id x
        cases xh.odd⊢ (↑finv ∘ ↑f) Parity.odd = id Parity.oddh.even⊢ (↑finv ∘ ↑f) Parity.even = id Parity.even <;>h.odd⊢ (↑finv ∘ ↑f) Parity.odd = id Parity.oddh.even⊢ (↑finv ∘ ↑f) Parity.even = id Parity.even rflAll goals completed! 🐙
      exact Subtype.ext h₀All goals completed! 🐙
    ·h.right⊢ f ⊚ finv = 𝟙 signMul have h₀ : f.val ∘ finv.val = id := by⊢ ∃ inv, inv ⊚ f = 𝟙 parityAdd ∧ f ⊚ inv = 𝟙 signMul
        funext xhx:signMul.t⊢ (↑f ∘ ↑finv) x = id x
        cases xh.pos⊢ (↑f ∘ ↑finv) Sign.pos = id Sign.posh.neg⊢ (↑f ∘ ↑finv) Sign.neg = id Sign.neg <;>h.pos⊢ (↑f ∘ ↑finv) Sign.pos = id Sign.posh.neg⊢ (↑f ∘ ↑finv) Sign.neg = id Sign.neg rflAll goals completed! 🐙
      exact Subtype.ext h₀All goals completed! 🐙
}

Exercise 3 (p. 66)

An unscrupulous importer has sold to the algebraic category section of our zoo some creatures which are not isomorphisms. Unmask the impostors.

(a) {(\mathbb{R}, +) \xrightarrow{p} (\mathbb{R}, +)} by 'plus 1': {p\:x = x + 1}.

(b) {(\mathbb{R}, \times) \xrightarrow{\mathit{sq}} (\mathbb{R}, \times)} by 'squaring': {\mathit{sq}\:x = x^2}.

(c) {(\mathbb{R}, \times) \xrightarrow{\mathit{sq}} (\mathbb{R}_{\ge 0}, \times)} by 'squaring': {\mathit{sq}\:x = x^2}.

(d) {(\mathbb{R}, +) \xrightarrow{m} (\mathbb{R}, +)} by 'minus': {m\:x = -x}.

(e) {(\mathbb{R}, \times) \xrightarrow{m} (\mathbb{R}, \times)} by 'minus': {m\:x = -x}.

(f) {(\mathbb{R}, \times) \xrightarrow{c} (\mathbb{R}_{>0}, \times)} by 'cubing': {c\:x = x^3}.

Hints: Exactly one is genuine. Some of the cruder impostors fail to be maps in our category, i.e. don't respect the combining-rules. The crudest is not even a map of sets with the indicated domain and codomain.

Solution: Exercise 3

For clarity of presentation here, we restrict our use of the category of algebraic objects we defined in Exercise 1 to the one genuine case of (d).

(a) p fails to respect the combining-rules.

example {p : ℝ ⟶ ℝ} (hp : ∀ x : ℝ, p x = x + 1)
    : ¬(∀ a b : ℝ, p (a + b) = p a + p b) := byp:ℝ ⟶ ℝhp:∀ (x : ℝ), p x = x + 1⊢ ¬∀ (a b : ℝ), p (a + b) = p a + p b
  push_negp:ℝ ⟶ ℝhp:∀ (x : ℝ), p x = x + 1⊢ ∃ a b, p (a + b) ≠ p a + p b
  use 0, 0hp:ℝ ⟶ ℝhp:∀ (x : ℝ), p x = x + 1⊢ p (0 + 0) ≠ p 0 + p 0
  rw [add_zero, ne_eq, left_eq_add, hp]hp:ℝ ⟶ ℝhp:∀ (x : ℝ), p x = x + 1⊢ ¬0 + 1 = 0
  linarithAll goals completed! 🐙

(b) \mathit{sq} has no retraction.

example {sq : ℝ ⟶ ℝ} (hsq : ∀ x : ℝ, sq x = x ^ 2)
    : ¬(∃ r : ℝ → ℝ, (∀ x : ℝ, r (sq x) = x)) := bysq:ℝ ⟶ ℝhsq:∀ (x : ℝ), sq x = x ^ 2⊢ ¬∃ r, ∀ (x : ℝ), r (sq x) = x
  by_contra hsq:ℝ ⟶ ℝhsq:∀ (x : ℝ), sq x = x ^ 2h:∃ r, ∀ (x : ℝ), r (sq x) = x⊢ False
  obtain ⟨r, h⟩ := hsq:ℝ ⟶ ℝhsq:∀ (x : ℝ), sq x = x ^ 2r:ℝ → ℝh:∀ (x : ℝ), r (sq x) = x⊢ False
  have hpos : r (sq 1) = 1 := h 1sq:ℝ ⟶ ℝhsq:∀ (x : ℝ), sq x = x ^ 2r:ℝ → ℝh:∀ (x : ℝ), r (sq x) = xhpos:r (sq 1) = 1 := h 1⊢ False
  have hneg : r (sq (-1)) = -1 := h (-1)sq:ℝ ⟶ ℝhsq:∀ (x : ℝ), sq x = x ^ 2r:ℝ → ℝh:∀ (x : ℝ), r (sq x) = xhpos:r (sq 1) = 1 := h 1hneg:r (sq (-1)) = -1 := h (-1)⊢ False
  rw [hsq] at hpos hnegsq:ℝ ⟶ ℝhsq:∀ (x : ℝ), sq x = x ^ 2r:ℝ → ℝh:∀ (x : ℝ), r (sq x) = xhpos:r (1 ^ 2) = 1hneg:r ((-1) ^ 2) = -1⊢ False
  rw [neg_sq, hpos] at hnegsq:ℝ ⟶ ℝhsq:∀ (x : ℝ), sq x = x ^ 2r:ℝ → ℝh:∀ (x : ℝ), r (sq x) = xhpos:r (1 ^ 2) = 1hneg:1 = -1⊢ False
  linarithAll goals completed! 🐙

open NNReal in
example {sq : ℝ ⟶ ℝ≥0} (hsq : ∀ x : ℝ, sq x = x ^ 2)
    : ¬(∃ r : ℝ → ℝ, (∀ x : ℝ, r (sq x) = x)) := bysq:ℝ ⟶ ℝ≥0hsq:∀ (x : ℝ), ↑(sq x) = x ^ 2⊢ ¬∃ r, ∀ (x : ℝ), r ↑(sq x) = x
  by_contra hsq:ℝ ⟶ ℝ≥0hsq:∀ (x : ℝ), ↑(sq x) = x ^ 2h:∃ r, ∀ (x : ℝ), r ↑(sq x) = x⊢ False
  obtain ⟨r, h⟩ := hsq:ℝ ⟶ ℝ≥0hsq:∀ (x : ℝ), ↑(sq x) = x ^ 2r:ℝ → ℝh:∀ (x : ℝ), r ↑(sq x) = x⊢ False
  have hpos : r (sq 1) = 1 := h 1sq:ℝ ⟶ ℝ≥0hsq:∀ (x : ℝ), ↑(sq x) = x ^ 2r:ℝ → ℝh:∀ (x : ℝ), r ↑(sq x) = xhpos:r ↑(sq 1) = 1 := h 1⊢ False
  have hneg : r (sq (-1)) = -1 := h (-1)sq:ℝ ⟶ ℝ≥0hsq:∀ (x : ℝ), ↑(sq x) = x ^ 2r:ℝ → ℝh:∀ (x : ℝ), r ↑(sq x) = xhpos:r ↑(sq 1) = 1 := h 1hneg:r ↑(sq (-1)) = -1 := h (-1)⊢ False
  rw [hsq] at hpos hnegsq:ℝ ⟶ ℝ≥0hsq:∀ (x : ℝ), ↑(sq x) = x ^ 2r:ℝ → ℝh:∀ (x : ℝ), r ↑(sq x) = xhpos:r (1 ^ 2) = 1hneg:r ((-1) ^ 2) = -1⊢ False
  rw [neg_sq, hpos] at hnegsq:ℝ ⟶ ℝ≥0hsq:∀ (x : ℝ), ↑(sq x) = x ^ 2r:ℝ → ℝh:∀ (x : ℝ), r ↑(sq x) = xhpos:r (1 ^ 2) = 1hneg:1 = -1⊢ False
  linarithAll goals completed! 🐙

(d) m is genuine.

def m : RealAdd ⟶ RealAdd := ⟨
  fun (x : ℝ) ↦ -x,
  by⊢ (∀ x ∈ RealAdd.carrier, (fun x ↦ -x) x ∈ RealAdd.carrier) ∧
  ∀ x₁ ∈ RealAdd.carrier,
    ∀ x₂ ∈ RealAdd.carrier, (fun x ↦ -x) (RealAdd.oper x₁ x₂) = RealAdd.oper ((fun x ↦ -x) x₁) ((fun x ↦ -x) x₂)
    constructorleft⊢ ∀ x ∈ RealAdd.carrier, (fun x ↦ -x) x ∈ RealAdd.carrierright⊢ ∀ x₁ ∈ RealAdd.carrier,
  ∀ x₂ ∈ RealAdd.carrier, (fun x ↦ -x) (RealAdd.oper x₁ x₂) = RealAdd.oper ((fun x ↦ -x) x₁) ((fun x ↦ -x) x₂)
    ·left⊢ ∀ x ∈ RealAdd.carrier, (fun x ↦ -x) x ∈ RealAdd.carrier exact fun _ _ ↦ Set.mem_univ _All goals completed! 🐙
    ·right⊢ ∀ x₁ ∈ RealAdd.carrier,
  ∀ x₂ ∈ RealAdd.carrier, (fun x ↦ -x) (RealAdd.oper x₁ x₂) = RealAdd.oper ((fun x ↦ -x) x₁) ((fun x ↦ -x) x₂) introsrightx₁✝:RealAdd.ta✝¹:x₁✝ ∈ RealAdd.carrierx₂✝:RealAdd.ta✝:x₂✝ ∈ RealAdd.carrier⊢ (fun x ↦ -x) (RealAdd.oper x₁✝ x₂✝) = RealAdd.oper ((fun x ↦ -x) x₁✝) ((fun x ↦ -x) x₂✝)
      dsimp [RealAdd]rightx₁✝:RealAdd.ta✝¹:x₁✝ ∈ RealAdd.carrierx₂✝:RealAdd.ta✝:x₂✝ ∈ RealAdd.carrier⊢ -(x₁✝ + x₂✝) = -x₁✝ + -x₂✝
      ringAll goals completed! 🐙
⟩

def minv := m

example : IsIso m := {
  out := by⊢ ∃ inv, inv ⊚ m = 𝟙 RealAdd ∧ m ⊚ inv = 𝟙 RealAdd
    use minvh⊢ minv ⊚ m = 𝟙 RealAdd ∧ m ⊚ minv = 𝟙 RealAdd
    constructorh.left⊢ minv ⊚ m = 𝟙 RealAddh.right⊢ m ⊚ minv = 𝟙 RealAdd
    ·h.left⊢ minv ⊚ m = 𝟙 RealAdd have h₀ : minv.val ∘ m.val = id := by⊢ ∃ inv, inv ⊚ m = 𝟙 RealAdd ∧ m ⊚ inv = 𝟙 RealAdd
        funext xhx:RealAdd.t⊢ (↑minv ∘ ↑m) x = id x
        dsimp [m, minv]hx:RealAdd.t⊢ - -x = x
        Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ringAll goals completed! 🐙
      exact Subtype.ext h₀All goals completed! 🐙
    ·h.right⊢ m ⊚ minv = 𝟙 RealAdd have h₀ : m.val ∘ minv.val = id := by⊢ ∃ inv, inv ⊚ m = 𝟙 RealAdd ∧ m ⊚ inv = 𝟙 RealAdd
        funext xhx:RealAdd.t⊢ (↑m ∘ ↑minv) x = id x
        dsimp [m, minv]hx:RealAdd.t⊢ - -x = x
        Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ringAll goals completed! 🐙
      exact Subtype.ext h₀All goals completed! 🐙
}

(e) m fails to respect the combining-rules.

example {m : ℝ ⟶ ℝ} (hm : ∀ x : ℝ, m x = -x)
    : ¬(∀ a b : ℝ, m (a * b) = m a * m b) := bym:ℝ ⟶ ℝhm:∀ (x : ℝ), m x = -x⊢ ¬∀ (a b : ℝ), m (a * b) = m a * m b
  push_negm:ℝ ⟶ ℝhm:∀ (x : ℝ), m x = -x⊢ ∃ a b, m (a * b) ≠ m a * m b
  use 1, 1hm:ℝ ⟶ ℝhm:∀ (x : ℝ), m x = -x⊢ m (1 * 1) ≠ m 1 * m 1
  rw [mul_one, ne_eq, hm]hm:ℝ ⟶ ℝhm:∀ (x : ℝ), m x = -x⊢ ¬-1 = -1 * -1
  linarithAll goals completed! 🐙

(f) c has an invalid codomain.

abbrev ℝpos := { x : ℝ // x > 0 }

example {c : ℝ → ℝpos} (hc : ∀ x : ℝ, c x = x ^ 3)
    : ∃ x : ℝ, ¬(∃ y : ℝpos, y.val = c x) := byc:ℝ → ℝposhc:∀ (x : ℝ), ↑(c x) = x ^ 3⊢ ∃ x, ¬∃ y, ↑y = ↑(c x)
  push_negc:ℝ → ℝposhc:∀ (x : ℝ), ↑(c x) = x ^ 3⊢ ∃ x, ∀ (y : ℝpos), ↑y ≠ ↑(c x)
  use -1hc:ℝ → ℝposhc:∀ (x : ℝ), ↑(c x) = x ^ 3⊢ ∀ (y : ℝpos), ↑y ≠ ↑(c (-1))
  rw [hc]hc:ℝ → ℝposhc:∀ (x : ℝ), ↑(c x) = x ^ 3⊢ ∀ (y : ℝpos), ↑y ≠ (-1) ^ 3
  norm_numhc:ℝ → ℝposhc:∀ (x : ℝ), ↑(c x) = x ^ 3⊢ ∀ (a : ℝ), 0 < a → ¬a = -1
  introshc:ℝ → ℝposhc:∀ (x : ℝ), ↑(c x) = x ^ 3a✝:ℝb✝:0 < a✝⊢ ¬a✝ = -1
  linarithAll goals completed! 🐙