@[simp]
def
category_theory.iso.app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
(X : C) :
The application of a natural isomorphism to an object. We put this definition in a different
namespace, so that we can use α.app
@[simp]
theorem
category_theory.iso.hom_inv_id_app_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
(X : C)
{X' : D}
(f' : F.obj X ⟶ X') :
@[simp]
theorem
category_theory.iso.hom_inv_id_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
(X : C) :
@[simp]
theorem
category_theory.iso.inv_hom_id_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
(X : C) :
@[simp]
theorem
category_theory.iso.inv_hom_id_app_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
(X : C)
{X' : D}
(f' : G.obj X ⟶ X') :
@[simp]
theorem
category_theory.nat_iso.trans_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G H : C ⥤ D}
(α : F ≅ G)
(β : G ≅ H)
(X : C) :
theorem
category_theory.nat_iso.app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
(X : C) :
theorem
category_theory.nat_iso.app_inv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
(X : C) :
@[instance]
def
category_theory.nat_iso.hom_app_is_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
(X : C) :
category_theory.is_iso (α.hom.app X)
Equations
- category_theory.nat_iso.hom_app_is_iso α X = {inv := α.inv.app X, hom_inv_id' := _, inv_hom_id' := _}
@[instance]
def
category_theory.nat_iso.inv_app_is_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
(X : C) :
category_theory.is_iso (α.inv.app X)
Equations
- category_theory.nat_iso.inv_app_is_iso α X = {inv := α.hom.app X, hom_inv_id' := _, inv_hom_id' := _}
Unfortunately we need a separate set of cancellation lemmas for components of natural isomorphisms,
because the simp normal form is α.hom.app X, rather than α.app.hom X.
(With the later, the morphism would be visibly part of an isomorphism, so general lemmas about isomorphisms would apply.)
In the future, we should consider a redesign that changes this simp norm form, but for now it breaks too many proofs.
@[simp]
theorem
category_theory.nat_iso.cancel_nat_iso_hom_right_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
{W X X' : D}
{Y : C}
(f : W ⟶ X)
(g : X ⟶ F.obj Y)
(f' : W ⟶ X')
(g' : X' ⟶ F.obj Y) :
@[simp]
theorem
category_theory.nat_iso.cancel_nat_iso_inv_right_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G)
{W X X' : D}
{Y : C}
(f : W ⟶ X)
(g : X ⟶ G.obj Y)
(f' : W ⟶ X')
(g' : X' ⟶ G.obj Y) :
def
category_theory.nat_iso.is_iso_of_is_iso_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ⟶ G)
[Π (X : C), category_theory.is_iso (α.app X)] :
Equations
- category_theory.nat_iso.is_iso_of_is_iso_app α = {inv := {app := λ (X : C), category_theory.is_iso.inv (α.app X), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[instance]
def
category_theory.nat_iso.is_iso_of_is_iso_app'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ⟶ G)
[H : Π (X : C), category_theory.is_iso (α.app X)] :
def
category_theory.nat_iso.is_iso_app_of_is_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ⟶ G)
[category_theory.is_iso α]
(X : C) :
category_theory.is_iso (α.app X)
Equations
- category_theory.nat_iso.is_iso_app_of_is_iso α X = {inv := (category_theory.is_iso.inv α).app X, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.nat_iso.of_components
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(app : Π (X : C), F.obj X ≅ G.obj X) :
Equations
- category_theory.nat_iso.of_components app naturality = category_theory.as_iso {app := λ (X : C), (app X).hom, naturality' := naturality}
@[simp]
theorem
category_theory.nat_iso.of_components.app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(app' : Π (X : C), F.obj X ≅ G.obj X)
(naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app' Y).hom = (app' X).hom ≫ G.map f)
(X : C) :
(category_theory.nat_iso.of_components app' naturality).app X = app' X
@[simp]
theorem
category_theory.nat_iso.of_components.hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(app : Π (X : C), F.obj X ≅ G.obj X)
(naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f)
(X : C) :
(category_theory.nat_iso.of_components app naturality).hom.app X = (app X).hom
@[simp]
theorem
category_theory.nat_iso.of_components.inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(app : Π (X : C), F.obj X ≅ G.obj X)
(naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f)
(X : C) :
(category_theory.nat_iso.of_components app naturality).inv.app X = (app X).inv
def
category_theory.nat_iso.hcomp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{F G : C ⥤ D}
{H I : D ⥤ E} :
Equations
- category_theory.nat_iso.hcomp α β = {hom := α.hom ◫ β.hom, inv := α.inv ◫ β.inv, hom_inv_id' := _, inv_hom_id' := _}