structure Category.Inverse {OA : Sort u_A} {x y : OA} {A : OA → OA → Sort v_A} [𝓐 : Category.Struct A] (f : A x y) : Sort (max 1 v_A)

An inverse for a particular morphism composes with it to form the identity.

It's useful to separate out the inverse itself from a full isomorphism, that way we can talk about a morphism with some structure having some property, and then how the inverse might gain an analogous property.

This is useful e.g. to say that a natural transformation + inverse to the carrier (without assuming naturality yet) is a natural isomorphism.

• inv : A y x
• inv_pre : self.inv ≫ f = Category.Struct.id
• inv_post : f ≫ self.inv = Category.Struct.id

theorem Category.Inverse.ext {OA : Sort u_A} {x y : OA} {A : OA → OA → Sort v_A} {𝓐 : Category.Struct A} {f : A x y} {x✝ y✝ : Category.Inverse f} (inv : x✝.inv = y✝.inv) : x✝ = y✝

def Category.Inverse.unique {OA : Sort u_A} {A : OA → OA → Sort v_A} [𝓐 : Category A] {x y : OA} (f : A x y) (g0 g1 : Category.Inverse f) : g0 = g1

Any inverse is as good as any other!

Equations

• ⋯ = ⋯

def Category.Inverse.comp {OA : Sort u_A} {A : OA → OA → Sort v_A} [𝓐 : Category A] {x y z : OA} {f0 : A x y} {f1 : A y z} (g0 : Category.Inverse f0) (g1 : Category.Inverse f1) : Category.Inverse (f0 ≫ f1)

Inverses naturally compose.

Equations

• g0.comp g1 = { inv := g1.inv ≫ g0.inv, inv_pre := ⋯, inv_post := ⋯ }

structure Category.Iso {OA : Sort u_A} (A : OA → OA → Sort v_A) [𝓐 : Category.Struct A] (x y : OA) : Sort (max 1 v_A)

Represents an isomorphism in some category.

An isomorphism is a morphism with an inverse.

• out : A x y
• inv : Category.Inverse self.out

theorem Category.Iso.ext {OA : Sort u_A} {A : OA → OA → Sort v_A} {𝓐 : Category.Struct A} {x y : OA} {x✝ y✝ : Category.Iso A x y} (out : x✝.out = y✝.out) (inv : HEq x✝.inv y✝.inv) : x✝ = y✝

@[simp]

def Category.Iso.eq_iff_out_eq {OA : Sort u_A} {A : OA → OA → Sort v_A} [𝓐 : Category A] {x y : OA} {f g : Category.Iso A x y} : f = g ↔ f.out = g.out

To compare isomorphisms, it suffices to compare the primary morphisms.

This is because any two inverses of a given morphism are equal.

Equations

• ⋯ = ⋯

def Category.Iso.id {OA : Sort u_A} {A : OA → OA → Sort v_A} [𝓐 : Category A] {x : OA} : Category.Iso A x x

There's a natural isomorphism from an object to itself.

Equations

• Category.Iso.id = { out := Category.Struct.id, inv := { inv := Category.Struct.id, inv_pre := ⋯, inv_post := ⋯ } }

def Category.Iso.from_eq {OA : Sort u_A} {A : OA → OA → Sort v_A} [𝓐 : Category A] {x y : OA} (h : x = y) : Category.Iso A x y

We can construct an isomorphism from an equality.

Equations

• Category.Iso.from_eq h = ⋯.mpr Category.Iso.id

def Category.Iso.comp {OA : Sort u_A} {A : OA → OA → Sort v_A} [𝓐 : Category A] {X Y Z : OA} (f : Category.Iso A X Y) (g : Category.Iso A Y Z) : Category.Iso A X Z

We can compose isomorphisms as well.

Equations

• f.comp g = { out := f.out ≫ g.out, inv := f.inv.comp g.inv }

instance Category.Iso.categoryStruct {OA : Sort u_A} {A : OA → OA → Sort v_A} [𝓐 : Category A] : Category.Struct (Category.Iso A)

Equations

• Category.Iso.categoryStruct = { id := fun {x : OA} => Category.Iso.id, comp := fun {a b c : OA} (f : Category.Iso A a b) (g : Category.Iso A b c) => f.comp g }

@[simp]

def Category.Iso.id_out {OA : Sort u_A} {A : OA → OA → Sort v_A} [𝓐 : Category A] {x : OA} : Category.Struct.id.out = Category.Struct.id

Equations

• ⋯ = ⋯

@[simp]

def Category.Iso.comp_out {OA : Sort u_A} {A : OA → OA → Sort v_A} [𝓐 : Category A] {x y z : OA} {f : Category.Iso A x y} {g : Category.Iso A y z} : (f ≫ g).out = f.out ≫ g.out

Equations

• ⋯ = ⋯

instance Category.Iso.category {OA : Sort u_A} {A : OA → OA → Sort v_A} [𝓐 : Category A] : Category (Category.Iso A)

Isomorphisms assemble into a category.

Equations

• Category.Iso.category = Category.mk ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Category.NatIso {OA : Sort u_A} {OB : Sort u_1} (A : OA → OA → Sort v_A) (B : OB → OB → Sort v_B) [𝓐 : Category A] [𝓑 : Category B] (x y : A ⥤ B) : Sort (max 1 (max 1 u_A) v_B)

A short abbreviation for natural isomorphisms.

We define these as simply being isomorphisms in the category of natural transformations.

This immediately gives us the fact that they form a category, making this a better definition.

Equations

• Category.NatIso A B = Category.Iso (Category.Nat A B)

def Category.«term_≅_» : Lean.TrailingParserDescr

Equations

• Category.«term_≅_» = Lean.ParserDescr.trailingNode `Category.«term_≅_» 82 83 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≅ ") (Lean.ParserDescr.cat `term 82))

def Category.NatIso.from_eq {OB : Sort u_1} {OA : Sort u_A} {A : OA → OA → Sort v_A} {B : OB → OB → Sort v_B} [𝓐 : Category A] [𝓑 : Category B] {F G : A ⥤ B} (h_eq : F = G) : Category.NatIso A B F G

Two functors that are equal are certainly isomorphic.

This turns out to be useful, because we have on-the-nose equality for equations involving the identity functor, but want to work with isomorphisms instead, usually.

Equations

• Category.NatIso.from_eq h_eq = Category.Iso.from_eq h_eq

def Category.NatIso.from_inverse {OB : Sort u_1} {OA : Sort u_A} {A : OA → OA → Sort v_A} {B : OB → OB → Sort v_B} [𝓐 : Category A] [𝓑 : Category B] {F G : A ⥤ B} (φ : Category.Nat A B F G) (inverse_on : (x : OA) → Category.Inverse (φ.on x)) : Category.NatIso A B F G

Construct a natural isomorphism from a transformation and a bundle of inverses.

The key proof involved here is that naturality of the bundle of inverses follows simply from the underlying transformation being natural.

Equations

• Category.NatIso.from_inverse φ inverse_on = { out := φ, inv := { inv := { on := fun (x : OA) => (inverse_on x).inv, natural := ⋯ }, inv_pre := ⋯, inv_post := ⋯ } }

def Category.NatIso.hcomp {OB : Sort u_1} {OC : Sort u_2} {OA : Sort u_A} {A : OA → OA → Sort v_A} {B : OB → OB → Sort v_B} {C : OC → OC → Sort v_C} [𝓐 : Category A] [𝓑 : Category B] [𝓒 : Category C] {F0 F1 : A ⥤ B} {G0 G1 : B ⥤ C} (h_F : Category.NatIso A B F0 F1) (h_G : Category.NatIso B C G0 G1) : Category.NatIso A C (F0 ⋙ G0) (F1 ⋙ G1)

Natural isomorphisms have a corresponding notion of horizontal composition.

Equations

• h_F.hcomp h_G = { out := h_F.out.hcomp h_G.out, inv := { inv := h_F.inv.inv.hcomp h_G.inv.inv, inv_pre := ⋯, inv_post := ⋯ } }