Show that category isomorphisms form a group

Stream: new members

[Xipan Xiao]

Trying to prove the following (easy) theorem in category theory:
If A is an object in a category C , show that the invertible elements of Mor(A, A) form a group.

The proof is straighforward, I finished most of the part with one remaining goal: the inverse of a morphism composed itself is the identity. I tried something like:

  inv_mul_cancel a := by
    apply Subtype.ext
    exact IsIso.inv_comp_eq a.property

but it doesn't compile: typeclass instance problem is stuck, it is often due to metavariables
IsIso ?m.10230.

The complete code is pasted:

import Mathlib

open CategoryTheory

universe u

variable {C : Type u} [Category C]
variable (A : C)

/-- The type of invertible endomorphisms of A -/
def Aut' (A : C) := { f : A ⟶ A // IsIso f }

namespace Aut'

instance : One (Aut' A) where
  one := ⟨𝟙 A, inferInstance⟩

instance : Mul (Aut' A) where
  mul f g := ⟨f.val ≫ g.val, by refine IsIso.comp_isIso' f.property g.property⟩


@[ext]
lemma ext {f g : Aut' A} (h : f.val = g.val) : f = g := Subtype.ext h

/-- Proof that Aut'(A) forms a group under composition -/
instance : Group (Aut' A) where
  mul_assoc a b c := by
    apply Subtype.ext
    exact Category.assoc a.val b.val c.val

  one_mul a := by
    apply Subtype.ext
    exact Category.id_comp a.val

  mul_one a := by
    apply Subtype.ext
    exact Category.comp_id a.val

  inv a := by
    apply Subtype.mk
    exact (Subobject.isIso_iff_mk_eq_top (𝟙 A)).mpr rfl

  inv_mul_cancel a := by
    apply Subtype.ext
    exact IsIso.inv_comp_eq a.property

What could be the problem? The error message doesn't say much.

[Aaron Liu]

You wrote in the wrong inv operation

[Etienne Marion]

Yes you defined the inverse of any morphism as the identity. Moreover you should avoid tactic mode when defining data, it often makes things more complicated. Here is a way which works:

import Mathlib

open CategoryTheory

universe u

variable {C : Type u} [Category C]
variable (A : C)

/-- The type of invertible endomorphisms of A -/
def Aut' (A : C) := { f : A ⟶ A // IsIso f }

namespace Aut'

instance : One (Aut' A) where
  one := ⟨𝟙 A, inferInstance⟩

lemma one_def : (1 : Aut' A).1 = 𝟙 A := rfl

instance : Mul (Aut' A) where
  mul f g := ⟨f.val ≫ g.val, by refine IsIso.comp_isIso' f.property g.property⟩

lemma mul_def (f g : Aut' A) : (f * g).1 = f.1 ≫ g.1 := rfl

@[ext]
lemma ext {f g : Aut' A} (h : f.val = g.val) : f = g := Subtype.ext h

/-- Proof that Aut'(A) forms a group under composition -/
noncomputable instance : Group (Aut' A) where
  mul_assoc a b c := by
    apply Subtype.ext
    exact Category.assoc a.val b.val c.val

  one_mul a := by
    apply Subtype.ext
    exact Category.id_comp a.val

  mul_one a := by
    apply Subtype.ext
    exact Category.comp_id a.val

  inv a := ⟨@inv _ _ _ _ a.1 a.2, a.2.inv_isIso⟩

  inv_mul_cancel a := by
    apply Subtype.ext
    rw [mul_def, one_def]
    simp

[Edward van de Meent]

fwiw, it'll be useful to have the following too:

instance {a : Aut' A} : IsIso a.val := a.property

This allows you to skip the @explicit stuff