Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore(category_theory/isomorphism): docstring, DRY, add some trivial lemmas #1309

Merged
merged 5 commits into from
Aug 15, 2019
Merged

chore(category_theory/isomorphism): docstring, DRY, add some trivial lemmas #1309

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
67fc3aa
chore(category_theory/isomorphism): docstring, DRY, add some trivial …
urkud Aug 8, 2019
6d2ed7a
Merge branch 'master' into isomorphisms
urkud Aug 8, 2019
72b8ae2
Merge branch 'master' into isomorphisms
urkud Aug 10, 2019
83e9ad0
Merge branch 'master' into isomorphisms
urkud Aug 12, 2019
24387ae
Merge branch 'master' into isomorphisms
urkud Aug 15, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
133 changes: 88 additions & 45 deletions src/category_theory/isomorphism.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,30 @@ Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
-/
import category_theory.functor

/-!
# Isomorphisms

This file defines isomorphisms between objects of a category.

## Main definitions

- `structure iso` : a bundled isomorphism between two objects of a category;
- `class is_iso` : an unbundled version of `iso`; note that `is_iso f` is usually *not* a `Prop`,
because it holds the inverse morphism;
- `as_iso` : convert from `is_iso` to `iso`;
- `of_iso` : convert from `iso` to `is_iso`;
- standard operations on isomorphisms (composition, inverse etc)

## Notations

- `X ≅ Y` : same as `iso X Y`;
- `α ≪≫ β` : composition of two isomorphisms; it is called `iso.trans`

## Tags

category, category theory, isomorphism
-/

universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation

namespace category_theory
Expand Down Expand Up @@ -54,12 +78,19 @@ calc α.inv
iso.symm {hom := hom, inv := inv, hom_inv_id' := hom_inv_id, inv_hom_id' := inv_hom_id} =
{hom := inv, inv := hom, hom_inv_id' := inv_hom_id, inv_hom_id' := hom_inv_id} := rfl

@[simp] lemma symm_symm_eq {X Y : C} (α : X ≅ Y) : α.symm.symm = α :=
by cases α; refl

@[simp] lemma symm_eq_iff {X Y : C} {α β : X ≅ Y} : α.symm = β.symm ↔ α = β :=
⟨λ h, symm_symm_eq α ▸ symm_symm_eq β ▸ congr_arg symm h, congr_arg symm⟩

@[refl] def refl (X : C) : X ≅ X :=
{ hom := 𝟙 X,
inv := 𝟙 X }

@[simp] lemma refl_hom (X : C) : (iso.refl X).hom = 𝟙 X := rfl
@[simp] lemma refl_inv (X : C) : (iso.refl X).inv = 𝟙 X := rfl
@[simp] lemma refl_symm (X : C) : (iso.refl X).symm = iso.refl X := rfl

@[trans] def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z :=
{ hom := α.hom ≫ β.hom,
Expand All @@ -79,8 +110,22 @@ infixr ` ≪≫ `:80 := iso.trans -- type as `\ll \gg`.
{hom := hom ≫ hom', inv := inv' ≫ inv, hom_inv_id' := hom_inv_id'', inv_hom_id' := inv_hom_id''} :=
rfl

@[simp] lemma refl_symm (X : C) : (iso.refl X).hom = 𝟙 X := rfl
@[simp] lemma trans_symm (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).inv = β.inv ≫ α.inv := rfl
@[simp] lemma trans_symm (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).symm = β.symm ≪≫ α.symm := rfl
@[simp] lemma trans_assoc {Z' : C} (α : X ≅ Y) (β : Y ≅ Z) (γ : Z ≅ Z') :
(α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ :=
by ext; simp only [trans_hom, category.assoc]

@[simp] lemma refl_trans (α : X ≅ Y) : (iso.refl X) ≪≫ α = α := by ext; apply category.id_comp
@[simp] lemma trans_refl (α : X ≅ Y) : α ≪≫ (iso.refl Y) = α := by ext; apply category.comp_id

@[simp] lemma symm_self_id (α : X ≅ Y) : α.symm ≪≫ α = iso.refl Y := ext _ _ α.inv_hom_id
@[simp] lemma self_symm_id (α : X ≅ Y) : α ≪≫ α.symm = iso.refl X := ext _ _ α.hom_inv_id

@[simp] lemma symm_self_id_assoc (α : X ≅ Y) (β : Y ≅ Z) : α.symm ≪≫ α ≪≫ β = β :=
by rw [← trans_assoc, symm_self_id, refl_trans]

@[simp] lemma self_symm_id_assoc (α : X ≅ Y) (β : X ≅ Z) : α ≪≫ α.symm ≪≫ β = β :=
by rw [← trans_assoc, self_symm_id, refl_trans]

lemma inv_comp_eq (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : α.inv ≫ f = g ↔ f = α.hom ≫ g :=
⟨λ H, by simp [H.symm], λ H, by simp [H]⟩
Expand Down Expand Up @@ -116,52 +161,55 @@ class is_iso (f : X ⟶ Y) :=
(hom_inv_id' : f ≫ inv = 𝟙 X . obviously)
(inv_hom_id' : inv ≫ f = 𝟙 Y . obviously)

def inv (f : X ⟶ Y) [is_iso f] := is_iso.inv f
export is_iso (inv)

def as_iso (f : X ⟶ Y) [h : is_iso f] : X ≅ Y := { hom := f, ..h }

@[simp] lemma as_iso_hom (f : X ⟶ Y) [is_iso f] : (as_iso f).hom = f := rfl
@[simp] lemma as_iso_inv (f : X ⟶ Y) [is_iso f] : (as_iso f).inv = inv f := rfl

namespace is_iso

@[simp] lemma hom_inv_id (f : X ⟶ Y) [is_iso f] : f ≫ category_theory.inv f = 𝟙 X :=
@[simp] lemma hom_inv_id (f : X ⟶ Y) [is_iso f] : f ≫ inv f = 𝟙 X :=
is_iso.hom_inv_id' f
@[simp] lemma inv_hom_id (f : X ⟶ Y) [is_iso f] : category_theory.inv f ≫ f = 𝟙 Y :=
@[simp] lemma inv_hom_id (f : X ⟶ Y) [is_iso f] : inv f ≫ f = 𝟙 Y :=
is_iso.inv_hom_id' f

@[simp] lemma hom_inv_id_assoc {Z} (f : X ⟶ Y) [is_iso f] (g : X ⟶ Z) : f ≫ category_theory.inv f ≫ g = g :=
by rw [←category.assoc, hom_inv_id, category.id_comp]
@[simp] lemma inv_hom_id_assoc {Z} (f : X ⟶ Y) [is_iso f] (g : Y ⟶ Z) : category_theory.inv f ≫ f ≫ g = g :=
by rw [←category.assoc, inv_hom_id, category.id_comp]
@[simp] lemma hom_inv_id_assoc {Z} (f : X ⟶ Y) [is_iso f] (g : X ⟶ Z) :
f ≫ inv f ≫ g = g :=
(as_iso f).hom_inv_id_assoc g

@[simp] lemma inv_hom_id_assoc {Z} (f : X ⟶ Y) [is_iso f] (g : Y ⟶ Z) :
inv f ≫ f ≫ g = g :=
(as_iso f).inv_hom_id_assoc g

instance (X : C) : is_iso (𝟙 X) :=
{ inv := 𝟙 X }

instance of_iso (f : X ≅ Y) : is_iso f.hom :=
{ inv := f.inv }
{ .. f }

instance of_iso_inverse (f : X ≅ Y) : is_iso f.inv :=
{ inv := f.hom }
is_iso.of_iso f.symm

variables {f g : X ⟶ Y} {h : Y ⟶ Z}

instance inv_is_iso [is_iso f] : is_iso (category_theory.inv f) :=
{ inv := f,
hom_inv_id' := inv_hom_id f,
inv_hom_id' := hom_inv_id f }
instance inv_is_iso [is_iso f] : is_iso (inv f) :=
is_iso.of_iso_inverse (as_iso f)

instance comp_is_iso [is_iso f] [is_iso h] : is_iso (f ≫ h) :=
{ inv := category_theory.inv h ≫ category_theory.inv f,
hom_inv_id' := begin erw [category.assoc, hom_inv_id_assoc], exact hom_inv_id f, end,
inv_hom_id' := begin erw [category.assoc, inv_hom_id_assoc], exact inv_hom_id h, end }

@[simp] lemma inv_id : category_theory.inv (𝟙 X) = 𝟙 X := rfl
@[simp] lemma inv_comp [is_iso f] [is_iso h] :
category_theory.inv (f ≫ h) = category_theory.inv h ≫ category_theory.inv f := rfl
@[simp] lemma is_iso.inv_inv [is_iso f] : category_theory.inv (category_theory.inv f) = f := rfl
@[simp] lemma iso.inv_inv (f : X ≅ Y) :
category_theory.inv (f.inv) = f.hom := rfl
@[simp] lemma iso.inv_hom (f : X ≅ Y) :
category_theory.inv (f.hom) = f.inv := rfl
is_iso.of_iso $ (as_iso f) ≪≫ (as_iso h)

@[simp] lemma inv_id : inv (𝟙 X) = 𝟙 X := rfl
@[simp] lemma inv_comp [is_iso f] [is_iso h] : inv (f ≫ h) = inv h ≫ inv f := rfl
@[simp] lemma is_iso.inv_inv [is_iso f] : inv (inv f) = f := rfl
@[simp] lemma iso.inv_inv (f : X ≅ Y) : inv (f.inv) = f.hom := rfl
@[simp] lemma iso.inv_hom (f : X ≅ Y) : inv (f.hom) = f.inv := rfl

instance epi_of_iso (f : X ⟶ Y) [is_iso f] : epi f :=
{ left_cancellation := λ Z g h w,
-- This is an interesting test case for better rewrite automation.
by rw [←category.id_comp C g, ←category.id_comp C h, ←is_iso.inv_hom_id f, category.assoc, w, category.assoc] }
by rw [← is_iso.inv_hom_id_assoc f g, w, is_iso.inv_hom_id_assoc f h] }
instance mono_of_iso (f : X ⟶ Y) [is_iso f] : mono f :=
{ right_cancellation := λ Z g h w,
by rw [←category.comp_id C g, ←category.comp_id C h, ←is_iso.hom_inv_id f, ←category.assoc, w, ←category.assoc] }
Expand All @@ -176,12 +224,6 @@ begin
erw [inv_hom_id, p, inv_hom_id],
end

def as_iso (f : X ⟶ Y) [is_iso f] : X ≅ Y :=
{ hom := f, inv := inv f }

@[simp] lemma as_iso_hom (f : X ⟶ Y) [is_iso f] : (as_iso f).hom = f := rfl
@[simp] lemma as_iso_inv (f : X ⟶ Y) [is_iso f] : (as_iso f).inv = inv f := rfl

instance (f : X ⟶ Y) : subsingleton (is_iso f) :=
⟨λ a b,
suffices a.inv = b.inv, by cases a; cases b; congr; exact this,
Expand All @@ -191,11 +233,6 @@ instance (f : X ⟶ Y) : subsingleton (is_iso f) :=
lemma is_iso.inv_eq_inv {f g : X ⟶ Y} [is_iso f] [is_iso g] : inv f = inv g ↔ f = g :=
iso.inv_eq_inv (as_iso f) (as_iso g)

instance is_iso_comp (f : X ⟶ Y) (g : Y ⟶ Z) [is_iso f] [is_iso g] : is_iso (f ≫ g) :=
{ inv := inv g ≫ inv f }

instance is_iso_id : is_iso (𝟙 X) := { inv := 𝟙 X }

namespace functor

universes u₁ v₁ u₂ v₂
Expand All @@ -213,22 +250,28 @@ def map_iso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y :=
@[simp] lemma map_iso_hom (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : (F.map_iso i).hom = F.map i.hom := rfl
@[simp] lemma map_iso_inv (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : (F.map_iso i).inv = F.map i.inv := rfl

@[simp] lemma map_iso_symm (F : C ⥤ D) {X Y : C} (i : X ≅ Y) :
F.map_iso i.symm = (F.map_iso i).symm :=
rfl

@[simp] lemma map_iso_trans (F : C ⥤ D) {X Y Z : C} (i : X ≅ Y) (j : Y ≅ Z) :
F.map_iso (i ≪≫ j) = (F.map_iso i) ≪≫ (F.map_iso j) :=
by ext; apply functor.map_comp

instance (F : C ⥤ D) (f : X ⟶ Y) [is_iso f] : is_iso (F.map f) :=
{ ..(F.map_iso (as_iso f)) }
instance map_is_iso (F : C ⥤ D) (f : X ⟶ Y) [is_iso f] : is_iso (F.map f) :=
is_iso.of_iso $ F.map_iso (as_iso f)

@[simp] lemma map_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [is_iso f] :
F.map (inv f) = inv (F.map f) :=
rfl

@[simp] lemma map_hom_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [is_iso f] :
F.map f ≫ F.map (inv f) = 𝟙 (F.obj X) :=
by rw [←map_comp, is_iso.hom_inv_id, map_id]
by rw [map_inv, is_iso.hom_inv_id]

@[simp] lemma map_inv_hom (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [is_iso f] :
F.map (inv f) ≫ F.map f = 𝟙 (F.obj Y) :=
by rw [←map_comp, is_iso.inv_hom_id, map_id]

@[simp] lemma map_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [is_iso f] : F.map (inv f) = inv (F.map f) := rfl
by rw [map_inv, is_iso.inv_hom_id]

end functor

Expand Down