Mathlib.CategoryTheory.Iso

CategoryTheory.Iso structure

{C : Type u} [Category.{v} C] (X Y : C)

Full source

/-- An isomorphism (a.k.a. an invertible morphism) between two objects of a category.
The inverse morphism is bundled.

See also `CategoryTheory.Core` for the category with the same objects and isomorphisms playing
the role of morphisms. -/
@[stacks 0017]
structure Iso {C : Type u} [Category.{v} C] (X Y : C) where
  /-- The forward direction of an isomorphism. -/
  hom : X ⟶ Y
  /-- The backwards direction of an isomorphism. -/
  inv : Y ⟶ X
  /-- Composition of the two directions of an isomorphism is the identity on the source. -/
  hom_inv_id : hom ≫ inv = 𝟙 X := by aesop_cat
  /-- Composition of the two directions of an isomorphism in reverse order
  is the identity on the target. -/
  inv_hom_id : inv ≫ hom = 𝟙 Y := by aesop_cat

Isomorphism in a category

Informal description

An isomorphism between two objects $X$ and $Y$ in a category $\mathcal{C}$ consists of a pair of morphisms $f : X \to Y$ and $g : Y \to X$ such that $f \circ g = \text{id}_Y$ and $g \circ f = \text{id}_X$. This structure represents a bundled version of an invertible morphism in category theory.

CategoryTheory.term_≅_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for an isomorphism in a category. -/
infixr:10 " ≅ " => Iso

Isomorphism notation

Informal description

The notation `X ≅ Y` denotes an isomorphism between objects `X` and `Y` in a category.

CategoryTheory.Iso.ext theorem

⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β

Full source

@[ext]
theorem ext ⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β :=
  suffices α.inv = β.inv by
    cases α
    cases β
    cases w
    cases this
    rfl
  calc
    α.inv = α.inv ≫ β.hom ≫ β.inv   := by rw [Iso.hom_inv_id, Category.comp_id]
    _     = (α.inv ≫ α.hom) ≫ β.inv := by rw [Category.assoc, ← w]
    _     = β.inv                    := by rw [Iso.inv_hom_id, Category.id_comp]

Extensionality of Isomorphisms via Homomorphism Equality

Informal description

For any two isomorphisms $\alpha, \beta \colon X \cong Y$ in a category $\mathcal{C}$, if their underlying homomorphisms are equal ($\alpha_{\text{hom}} = \beta_{\text{hom}}$), then $\alpha = \beta$.

CategoryTheory.Iso.symm definition

(I : X ≅ Y) : Y ≅ X

Full source

/-- Inverse isomorphism. -/
@[symm]
def symm (I : X ≅ Y) : Y ≅ X where
  hom := I.inv
  inv := I.hom

Inverse isomorphism

Informal description

Given an isomorphism $I \colon X \cong Y$ in a category $\mathcal{C}$, the inverse isomorphism $I^{-1} \colon Y \cong X$ is defined by swapping the morphisms, i.e., the homomorphism of $I^{-1}$ is the inverse of $I$, and the inverse of $I^{-1}$ is the homomorphism of $I$.

CategoryTheory.Iso.symm_hom theorem

(α : X ≅ Y) : α.symm.hom = α.inv

Full source

@[simp]
theorem symm_hom (α : X ≅ Y) : α.symm.hom = α.inv :=
  rfl

Homomorphism of Inverse Isomorphism Equals Inverse Morphism

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$, the homomorphism of the inverse isomorphism $\alpha^{-1}$ is equal to the inverse morphism of $\alpha$, i.e., $\alpha^{-1}_{\text{hom}} = \alpha_{\text{inv}}$.

CategoryTheory.Iso.symm_inv theorem

(α : X ≅ Y) : α.symm.inv = α.hom

Full source

@[simp]
theorem symm_inv (α : X ≅ Y) : α.symm.inv = α.hom :=
  rfl

Inverse of Inverse Isomorphism Equals Original Homomorphism

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$, the inverse morphism of the inverse isomorphism $\alpha^{-1}$ is equal to the homomorphism of $\alpha$, i.e., $\alpha^{-1}_{\text{inv}} = \alpha_{\text{hom}}$.

CategoryTheory.Iso.symm_mk theorem

 {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id) :
  Iso.symm { hom, 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 }

Full source

@[simp]
theorem symm_mk {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id) :
    Iso.symm { hom, 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

Inverse of Constructed Isomorphism Equals Swapped Construction

Informal description

Given objects $X$ and $Y$ in a category $\mathcal{C}$, and morphisms $f \colon X \to Y$ and $g \colon Y \to X$ satisfying $f \circ g = \text{id}_Y$ and $g \circ f = \text{id}_X$, the inverse isomorphism of the isomorphism constructed from $(f, g)$ is equal to the isomorphism constructed from $(g, f)$ with the composition conditions swapped. In other words, if $\alpha$ is the isomorphism defined by $\alpha_{\text{hom}} = f$ and $\alpha_{\text{inv}} = g$, then $\alpha^{-1}$ is the isomorphism defined by $\alpha^{-1}_{\text{hom}} = g$ and $\alpha^{-1}_{\text{inv}} = f$.

CategoryTheory.Iso.symm_symm_eq theorem

{X Y : C} (α : X ≅ Y) : α.symm.symm = α

Full source

@[simp]
theorem symm_symm_eq {X Y : C} (α : X ≅ Y) : α.symm.symm = α := rfl

Double Inverse of Isomorphism Equals Original Isomorphism

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$, the double inverse of $\alpha$ is equal to $\alpha$ itself, i.e., $(\alpha^{-1})^{-1} = \alpha$.

CategoryTheory.Iso.symm_bijective theorem

{X Y : C} : Function.Bijective (symm : (X ≅ Y) → _)

Full source

theorem symm_bijective {X Y : C} : Function.Bijective (symm : (X ≅ Y) → _) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm_eq, symm_symm_eq⟩

Bijectivity of the Inverse Isomorphism Map

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$, the function that maps an isomorphism $\alpha \colon X \cong Y$ to its inverse $\alpha^{-1} \colon Y \cong X$ is bijective.

CategoryTheory.Iso.symm_eq_iff theorem

{X Y : C} {α β : X ≅ Y} : α.symm = β.symm ↔ α = β

Full source

@[simp]
theorem symm_eq_iff {X Y : C} {α β : X ≅ Y} : α.symm = β.symm ↔ α = β :=
  symm_bijective.injective.eq_iff

Inverse Isomorphism Equality Criterion: $\alpha^{-1} = \beta^{-1} \leftrightarrow \alpha = \beta$

Informal description

For any two isomorphisms $\alpha, \beta \colon X \cong Y$ in a category $\mathcal{C}$, the inverses $\alpha^{-1}$ and $\beta^{-1}$ are equal if and only if $\alpha$ and $\beta$ are equal.

CategoryTheory.Iso.nonempty_iso_symm theorem

(X Y : C) : Nonempty (X ≅ Y) ↔ Nonempty (Y ≅ X)

Full source

theorem nonempty_iso_symm (X Y : C) : NonemptyNonempty (X ≅ Y) ↔ Nonempty (Y ≅ X) :=
  ⟨fun h => ⟨h.some.symm⟩, fun h => ⟨h.some.symm⟩⟩

Existence of Isomorphism is Symmetric

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$, there exists an isomorphism from $X$ to $Y$ if and only if there exists an isomorphism from $Y$ to $X$.

CategoryTheory.Iso.refl definition

(X : C) : X ≅ X

Full source

/-- Identity isomorphism. -/
@[refl, simps]
def refl (X : C) : X ≅ X where
  hom := 𝟙 X
  inv := 𝟙 X

Identity isomorphism

Informal description

The identity isomorphism on an object $X$ in a category $\mathcal{C}$ consists of the identity morphism $\text{id}_X : X \to X$ as both the forward and backward morphisms.

CategoryTheory.Iso.instInhabited instance

: Inhabited (X ≅ X)

Full source

instance : Inhabited (X ≅ X) := ⟨Iso.refl X⟩

Inhabited Type of Self-Isomorphisms

Informal description

For any object $X$ in a category $\mathcal{C}$, the type of isomorphisms $X \cong X$ is inhabited, with the identity isomorphism $\text{id}_X$ as its canonical element.

CategoryTheory.Iso.nonempty_iso_refl theorem

(X : C) : Nonempty (X ≅ X)

Full source

theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩

Existence of Identity Isomorphism in a Category

Informal description

For any object $X$ in a category $\mathcal{C}$, there exists an isomorphism from $X$ to itself, namely the identity isomorphism $\text{id}_X \colon X \cong X$.

CategoryTheory.Iso.refl_symm theorem

(X : C) : (Iso.refl X).symm = Iso.refl X

Full source

@[simp]
theorem refl_symm (X : C) : (Iso.refl X).symm = Iso.refl X := rfl

Inverse of Identity Isomorphism is Identity

Informal description

For any object $X$ in a category $\mathcal{C}$, the inverse of the identity isomorphism $\text{id}_X \colon X \cong X$ is equal to itself, i.e., $(\text{id}_X)^{-1} = \text{id}_X$.

CategoryTheory.Iso.trans definition

(α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z

Full source

/-- Composition of two isomorphisms -/
@[simps]
def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z where
  hom := α.hom ≫ β.hom
  inv := β.inv ≫ α.inv

Composition of isomorphisms

Informal description

Given isomorphisms $\alpha \colon X \cong Y$ and $\beta \colon Y \cong Z$ in a category $\mathcal{C}$, the composition $\alpha \ggg \beta$ is an isomorphism from $X$ to $Z$, where the forward morphism is the composition $\alpha_{\text{hom}} \circ \beta_{\text{hom}}$ and the inverse morphism is the composition $\beta_{\text{inv}} \circ \alpha_{\text{inv}}$.

CategoryTheory.Iso.instTransIso instance

: Trans (α := C) (· ≅ ·) (· ≅ ·) (· ≅ ·)

Full source

@[simps]
instance instTransIso : Trans (α := C) (· ≅ ·) (· ≅ ·) (· ≅ ·) where
  trans := trans

Transitivity of Isomorphism Composition in a Category

Informal description

The composition of isomorphisms in a category $\mathcal{C}$ is transitive. That is, given isomorphisms $\alpha \colon X \cong Y$ and $\beta \colon Y \cong Z$, there exists a composite isomorphism $\alpha \ggg \beta \colon X \cong Z$.

CategoryTheory.Iso.term_≪≫_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for composition of isomorphisms. -/
infixr:80 " ≪≫ " => Iso.trans

Composition of isomorphisms

Informal description

The notation `≪≫` represents the composition of two isomorphisms in a category, where given isomorphisms $\alpha : X \cong Y$ and $\beta : Y \cong Z$, the composition $\alpha \ggg \beta$ is an isomorphism from $X$ to $Z$.

CategoryTheory.Iso.trans_mk theorem

 {X Y Z : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id) (hom' : Y ⟶ Z) (inv' : Z ⟶ Y) (hom_inv_id')
  (inv_hom_id') (hom_inv_id'') (inv_hom_id'') :
  Iso.trans ⟨hom, inv, hom_inv_id, inv_hom_id⟩ ⟨hom', inv', hom_inv_id', inv_hom_id'⟩ =
    ⟨hom ≫ hom', inv' ≫ inv, hom_inv_id'', inv_hom_id''⟩

Full source

@[simp]
theorem trans_mk {X Y Z : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id)
    (hom' : Y ⟶ Z) (inv' : Z ⟶ Y) (hom_inv_id') (inv_hom_id') (hom_inv_id'') (inv_hom_id'') :
    Iso.trans ⟨hom, inv, hom_inv_id, inv_hom_id⟩ ⟨hom', inv', hom_inv_id', inv_hom_id'⟩ =
     ⟨hom ≫ hom', inv' ≫ inv, hom_inv_id'', inv_hom_id''⟩ :=
  rfl

Composition of Constructed Isomorphisms via Forward and Inverse Morphisms

Informal description

Given morphisms $f \colon X \to Y$ and $g \colon Y \to X$ with $f \circ g = \text{id}_Y$ and $g \circ f = \text{id}_X$, and morphisms $f' \colon Y \to Z$ and $g' \colon Z \to Y$ with $f' \circ g' = \text{id}_Z$ and $g' \circ f' = \text{id}_Y$, the composition of the isomorphisms $\langle f, g, \text{hom\_inv\_id}, \text{inv\_hom\_id} \rangle$ and $\langle f', g', \text{hom\_inv\_id}', \text{inv\_hom\_id}' \rangle$ is equal to the isomorphism $\langle f \circ f', g' \circ g, \text{hom\_inv\_id}'', \text{inv\_hom\_id}'' \rangle$.

CategoryTheory.Iso.trans_symm theorem

(α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).symm = β.symm ≪≫ α.symm

Full source

@[simp]
theorem trans_symm (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).symm = β.symm ≪≫ α.symm :=
  rfl

Inverse of Composition of Isomorphisms

Informal description

For any isomorphisms $\alpha \colon X \cong Y$ and $\beta \colon Y \cong Z$ in a category $\mathcal{C}$, the inverse of the composition $\alpha \circ \beta$ is equal to the composition of the inverses $\beta^{-1} \circ \alpha^{-1}$.

CategoryTheory.Iso.trans_assoc theorem

{Z' : C} (α : X ≅ Y) (β : Y ≅ Z) (γ : Z ≅ Z') : (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ

Full source

@[simp]
theorem trans_assoc {Z' : C} (α : X ≅ Y) (β : Y ≅ Z) (γ : Z ≅ Z') :
    (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ := by
  ext; simp only [trans_hom, Category.assoc]

Associativity of Isomorphism Composition in a Category

Informal description

For any isomorphisms $\alpha \colon X \cong Y$, $\beta \colon Y \cong Z$, and $\gamma \colon Z \cong Z'$ in a category $\mathcal{C}$, the composition of isomorphisms is associative, i.e., $(\alpha \circ \beta) \circ \gamma = \alpha \circ (\beta \circ \gamma)$.

CategoryTheory.Iso.refl_trans theorem

(α : X ≅ Y) : Iso.refl X ≪≫ α = α

Full source

@[simp]
theorem refl_trans (α : X ≅ Y) : Iso.reflIso.refl X ≪≫ α = α := by ext; apply Category.id_comp

Identity isomorphism composition: $\text{id}_X \circ \alpha = \alpha$

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$, the composition of the identity isomorphism on $X$ with $\alpha$ equals $\alpha$, i.e., $\text{id}_X \circ \alpha = \alpha$.

CategoryTheory.Iso.trans_refl theorem

(α : X ≅ Y) : α ≪≫ Iso.refl Y = α

Full source

@[simp]
theorem trans_refl (α : X ≅ Y) : α ≪≫ Iso.refl Y = α := by ext; apply Category.comp_id

Right Identity Law for Isomorphism Composition

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$, the composition of $\alpha$ with the identity isomorphism on $Y$ is equal to $\alpha$, i.e., $\alpha \ggg \text{id}_Y = \alpha$.

CategoryTheory.Iso.symm_self_id theorem

(α : X ≅ Y) : α.symm ≪≫ α = Iso.refl Y

Full source

@[simp]
theorem symm_self_id (α : X ≅ Y) : α.symm ≪≫ α = Iso.refl Y :=
  ext α.inv_hom_id

Inverse Composition Yields Identity Isomorphism

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$, the composition of its inverse $\alpha^{-1}$ with $\alpha$ equals the identity isomorphism on $Y$, i.e., $\alpha^{-1} \circ \alpha = \text{id}_Y$.

CategoryTheory.Iso.self_symm_id theorem

(α : X ≅ Y) : α ≪≫ α.symm = Iso.refl X

Full source

@[simp]
theorem self_symm_id (α : X ≅ Y) : α ≪≫ α.symm = Iso.refl X :=
  ext α.hom_inv_id

Composition of Isomorphism with Its Inverse Yields Identity

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$, the composition of $\alpha$ with its inverse $\alpha^{-1}$ is equal to the identity isomorphism on $X$, i.e., $\alpha \circ \alpha^{-1} = \text{id}_X$.

CategoryTheory.Iso.symm_self_id_assoc theorem

(α : X ≅ Y) (β : Y ≅ Z) : α.symm ≪≫ α ≪≫ β = β

Full source

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

Isomorphism cancellation: $\alpha^{-1} \circ \alpha \circ \beta = \beta$

Informal description

For any isomorphisms $\alpha \colon X \cong Y$ and $\beta \colon Y \cong Z$ in a category $\mathcal{C}$, the composition $\alpha^{-1} \circ \alpha \circ \beta$ equals $\beta$.

CategoryTheory.Iso.self_symm_id_assoc theorem

(α : X ≅ Y) (β : X ≅ Z) : α ≪≫ α.symm ≪≫ β = β

Full source

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

Composition with Inverse and Isomorphism: $\alpha \circ \alpha^{-1} \circ \beta = \beta$

Informal description

For any isomorphisms $\alpha \colon X \cong Y$ and $\beta \colon X \cong Z$ in a category $\mathcal{C}$, the composition $\alpha \circ \alpha^{-1} \circ \beta$ equals $\beta$.

CategoryTheory.Iso.inv_comp_eq theorem

(α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : α.inv ≫ f = g ↔ f = α.hom ≫ g

Full source

theorem inv_comp_eq (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : α.inv ≫ fα.inv ≫ f = g ↔ f = α.hom ≫ g :=
  ⟨fun H => by simp [H.symm], fun H => by simp [H]⟩

Inverse Composition Equivalence for Isomorphisms

Informal description

Let $\mathcal{C}$ be a category, and let $\alpha : X \cong Y$ be an isomorphism in $\mathcal{C}$. For any morphisms $f : X \to Z$ and $g : Y \to Z$, the composition $\alpha^{-1} \circ f$ equals $g$ if and only if $f$ equals $\alpha \circ g$.

CategoryTheory.Iso.comp_inv_eq theorem

(α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : f ≫ α.inv = g ↔ f = g ≫ α.hom

Full source

theorem comp_inv_eq (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : f ≫ α.invf ≫ α.inv = g ↔ f = g ≫ α.hom :=
  ⟨fun H => by simp [H.symm], fun H => by simp [H]⟩

Composition with Inverse Equals Morphism iff Morphism Equals Composition with Hom

Informal description

Let $\mathcal{C}$ be a category, and let $\alpha : X \cong Y$ be an isomorphism in $\mathcal{C}$. For any morphisms $f : Z \to Y$ and $g : Z \to X$, the composition $f \circ \alpha^{-1}$ equals $g$ if and only if $f$ equals $g \circ \alpha$.

CategoryTheory.Iso.inv_eq_inv theorem

(f g : X ≅ Y) : f.inv = g.inv ↔ f.hom = g.hom

Full source

theorem inv_eq_inv (f g : X ≅ Y) : f.inv = g.inv ↔ f.hom = g.hom :=
  have : ∀ {X Y : C} (f g : X ≅ Y), f.hom = g.hom → f.inv = g.inv := fun f g h => by rw [ext h]
  ⟨this f.symm g.symm, this f g⟩

Inverse Equality of Isomorphisms is Equivalent to Homomorphism Equality

Informal description

For any two isomorphisms $f, g \colon X \cong Y$ in a category $\mathcal{C}$, the inverses of $f$ and $g$ are equal ($f^{-1} = g^{-1}$) if and only if their underlying homomorphisms are equal ($f = g$).

CategoryTheory.Iso.hom_comp_eq_id theorem

(α : X ≅ Y) {f : Y ⟶ X} : α.hom ≫ f = 𝟙 X ↔ f = α.inv

Full source

theorem hom_comp_eq_id (α : X ≅ Y) {f : Y ⟶ X} : α.hom ≫ fα.hom ≫ f = 𝟙 X ↔ f = α.inv := by
  rw [← eq_inv_comp, comp_id]

Composition with Isomorphism Homomorphism Equals Identity iff Morphism is Inverse

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$ and any morphism $f \colon Y \to X$, the composition $\alpha_{\text{hom}} \circ f$ equals the identity morphism $\text{id}_X$ if and only if $f$ is equal to the inverse morphism $\alpha_{\text{inv}}$ of $\alpha$.

CategoryTheory.Iso.comp_hom_eq_id theorem

(α : X ≅ Y) {f : Y ⟶ X} : f ≫ α.hom = 𝟙 Y ↔ f = α.inv

Full source

theorem comp_hom_eq_id (α : X ≅ Y) {f : Y ⟶ X} : f ≫ α.homf ≫ α.hom = 𝟙 Y ↔ f = α.inv := by
  rw [← eq_comp_inv, id_comp]

Composition with Isomorphism Homomorphism Equals Identity iff Morphism is Inverse

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$ and any morphism $f \colon Y \to X$, the composition $f \circ \alpha_{\text{hom}}$ equals the identity morphism $\text{id}_Y$ if and only if $f$ is equal to the inverse morphism $\alpha_{\text{inv}}$ of $\alpha$.

CategoryTheory.Iso.inv_comp_eq_id theorem

(α : X ≅ Y) {f : X ⟶ Y} : α.inv ≫ f = 𝟙 Y ↔ f = α.hom

Full source

theorem inv_comp_eq_id (α : X ≅ Y) {f : X ⟶ Y} : α.inv ≫ fα.inv ≫ f = 𝟙 Y ↔ f = α.hom :=
  hom_comp_eq_id α.symm

Inverse Composition Equals Identity iff Morphism is Homomorphism

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$ and any morphism $f \colon X \to Y$, the composition $\alpha_{\text{inv}} \circ f$ equals the identity morphism $\text{id}_Y$ if and only if $f$ is equal to the homomorphism $\alpha_{\text{hom}}$ of $\alpha$.

CategoryTheory.Iso.comp_inv_eq_id theorem

(α : X ≅ Y) {f : X ⟶ Y} : f ≫ α.inv = 𝟙 X ↔ f = α.hom

Full source

theorem comp_inv_eq_id (α : X ≅ Y) {f : X ⟶ Y} : f ≫ α.invf ≫ α.inv = 𝟙 X ↔ f = α.hom :=
  comp_hom_eq_id α.symm

Composition with Isomorphism Inverse Equals Identity iff Morphism is Homomorphism

Informal description

For any isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$ and any morphism $f \colon X \to Y$, the composition $f \circ \alpha_{\text{inv}}$ equals the identity morphism $\text{id}_X$ if and only if $f$ is equal to the homomorphism $\alpha_{\text{hom}}$ of $\alpha$.

CategoryTheory.Iso.hom_eq_inv theorem

(α : X ≅ Y) (β : Y ≅ X) : α.hom = β.inv ↔ β.hom = α.inv

Full source

theorem hom_eq_inv (α : X ≅ Y) (β : Y ≅ X) : α.hom = β.inv ↔ β.hom = α.inv := by
  rw [← symm_inv, inv_eq_inv α.symm β, eq_comm]
  rfl

Homomorphism Equals Inverse iff Inverse Equals Homomorphism for Isomorphisms

Informal description

For any isomorphisms $\alpha \colon X \cong Y$ and $\beta \colon Y \cong X$ in a category $\mathcal{C}$, the homomorphism of $\alpha$ equals the inverse of $\beta$ if and only if the homomorphism of $\beta$ equals the inverse of $\alpha$. In symbols: \[ \alpha_{\text{hom}} = \beta_{\text{inv}} \leftrightarrow \beta_{\text{hom}} = \alpha_{\text{inv}}. \]

CategoryTheory.Iso.homToEquiv definition

(α : X ≅ Y) {Z : C} : (Z ⟶ X) ≃ (Z ⟶ Y)

Full source

/-- The bijection `(Z ⟶ X) ≃ (Z ⟶ Y)` induced by `α : X ≅ Y`. -/
@[simps]
def homToEquiv (α : X ≅ Y) {Z : C} : (Z ⟶ X) ≃ (Z ⟶ Y) where
  toFun f := f ≫ α.hom
  invFun g := g ≫ α.inv
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Bijection of morphisms to domain induced by an isomorphism

Informal description

Given an isomorphism $\alpha : X \cong Y$ in a category $\mathcal{C}$, the bijection $(Z \to X) \simeq (Z \to Y)$ is defined by mapping a morphism $f : Z \to X$ to $f \circ \alpha$ and a morphism $g : Z \to Y$ to $g \circ \alpha^{-1}$.

CategoryTheory.Iso.homFromEquiv definition

(α : X ≅ Y) {Z : C} : (X ⟶ Z) ≃ (Y ⟶ Z)

Full source

/-- The bijection `(X ⟶ Z) ≃ (Y ⟶ Z)` induced by `α : X ≅ Y`. -/
@[simps]
def homFromEquiv (α : X ≅ Y) {Z : C} : (X ⟶ Z) ≃ (Y ⟶ Z) where
  toFun f := α.inv ≫ f
  invFun g := α.hom ≫ g
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Bijection of morphisms induced by an isomorphism

Informal description

Given an isomorphism $\alpha : X \cong Y$ in a category $\mathcal{C}$, the bijection $(X \to Z) \simeq (Y \to Z)$ is defined by mapping a morphism $f : X \to Z$ to $\alpha^{-1} \circ f$ and a morphism $g : Y \to Z$ to $\alpha \circ g$.

CategoryTheory.IsIso structure

(f : X ⟶ Y)

Full source

/-- `IsIso` typeclass expressing that a morphism is invertible. -/
class IsIso (f : X ⟶ Y) : Prop where
  /-- The existence of an inverse morphism. -/
  out : ∃ inv : Y ⟶ X, f ≫ inv = 𝟙 X ∧ inv ≫ f = 𝟙 Y

Isomorphism in a category

Informal description

The typeclass `IsIso` asserts that a morphism $ f : X \to Y $ in a category is an isomorphism, i.e., there exists an inverse morphism $ f^{-1} : Y \to X $ such that $ f \circ f^{-1} = \text{id}_X $ and $ f^{-1} \circ f = \text{id}_Y $.

CategoryTheory.inv definition

(f : X ⟶ Y) [I : IsIso f] : Y ⟶ X

Full source

/-- The inverse of a morphism `f` when we have `[IsIso f]`.
-/
noncomputable def inv (f : X ⟶ Y) [I : IsIso f] : Y ⟶ X :=
  Classical.choose I.1

Inverse of an isomorphism in a category

Informal description

Given a morphism $ f : X \to Y $ in a category, if $ f $ is an isomorphism (i.e., `[IsIso f]` holds), then `inv f` is the inverse morphism $ f^{-1} : Y \to X $.

CategoryTheory.IsIso.hom_inv_id theorem

(f : X ⟶ Y) [I : IsIso f] : f ≫ inv f = 𝟙 X

Full source

@[simp]
theorem hom_inv_id (f : X ⟶ Y) [I : IsIso f] : f ≫ inv f = 𝟙 X :=
  (Classical.choose_spec I.1).left

Composition of an isomorphism with its inverse yields the identity

Informal description

For any morphism $ f : X \to Y $ in a category, if $ f $ is an isomorphism, then the composition $ f \circ f^{-1} $ is equal to the identity morphism $ \text{id}_X $ on $ X $.

CategoryTheory.IsIso.inv_hom_id theorem

(f : X ⟶ Y) [I : IsIso f] : inv f ≫ f = 𝟙 Y

Full source

@[simp]
theorem inv_hom_id (f : X ⟶ Y) [I : IsIso f] : invinv f ≫ f = 𝟙 Y :=
  (Classical.choose_spec I.1).right

Inverse Composition Yields Identity: $ f^{-1} \circ f = \text{id}_Y $

Informal description

For any morphism $ f : X \to Y $ in a category, if $ f $ is an isomorphism, then the composition $ f^{-1} \circ f $ is equal to the identity morphism $ \text{id}_Y $ on $ Y $.

CategoryTheory.IsIso.hom_inv_id_assoc theorem

(f : X ⟶ Y) [I : IsIso f] {Z} (g : X ⟶ Z) : f ≫ inv f ≫ g = g

Full source

@[simp]
theorem hom_inv_id_assoc (f : X ⟶ Y) [I : IsIso f] {Z} (g : X ⟶ Z) : f ≫ inv f ≫ g = g := by
  simp [← Category.assoc]

Associativity of Composition with Inverse: $f \circ f^{-1} \circ g = g$ for Isomorphisms

Informal description

For any morphism $f : X \to Y$ in a category, if $f$ is an isomorphism, then for any morphism $g : X \to Z$, the composition $f \circ f^{-1} \circ g$ is equal to $g$.

CategoryTheory.IsIso.inv_hom_id_assoc theorem

(f : X ⟶ Y) [I : IsIso f] {Z} (g : Y ⟶ Z) : inv f ≫ f ≫ g = g

Full source

@[simp]
theorem inv_hom_id_assoc (f : X ⟶ Y) [I : IsIso f] {Z} (g : Y ⟶ Z) : invinv f ≫ f ≫ g = g := by
  simp [← Category.assoc]

Associativity of Inverse Composition: $(f^{-1} \circ f) \circ g = g$ for Isomorphisms

Informal description

For any morphism $f : X \to Y$ in a category, if $f$ is an isomorphism, then for any morphism $g : Y \to Z$, the composition $(f^{-1} \circ f) \circ g$ is equal to $g$.

CategoryTheory.Iso.isIso_hom theorem

(e : X ≅ Y) : IsIso e.hom

Full source

lemma Iso.isIso_hom (e : X ≅ Y) : IsIso e.hom :=
  ⟨e.inv, by simp, by simp⟩

Homomorphism of an isomorphism is invertible

Informal description

For any isomorphism $e : X \cong Y$ in a category $\mathcal{C}$, the morphism $e_{\text{hom}} : X \to Y$ is an isomorphism.

CategoryTheory.Iso.isIso_inv theorem

(e : X ≅ Y) : IsIso e.inv

Full source

lemma Iso.isIso_inv (e : X ≅ Y) : IsIso e.inv := e.symm.isIso_hom

Inverse of an Isomorphism is an Isomorphism

Informal description

For any isomorphism $e \colon X \cong Y$ in a category $\mathcal{C}$, the inverse morphism $e_{\text{inv}} \colon Y \to X$ is an isomorphism.

CategoryTheory.asIso definition

(f : X ⟶ Y) [IsIso f] : X ≅ Y

Full source

/-- Reinterpret a morphism `f` with an `IsIso f` instance as an `Iso`. -/
noncomputable def asIso (f : X ⟶ Y) [IsIso f] : X ≅ Y :=
  ⟨f, inv f, hom_inv_id f, inv_hom_id f⟩

Isomorphism from invertible morphism

Informal description

Given a morphism $ f : X \to Y $ in a category $\mathcal{C}$, if $ f $ is an isomorphism (i.e., `[IsIso f]` holds), then `asIso f` constructs an isomorphism $ X \cong Y $ with $ f $ as its forward morphism and `inv f` as its inverse morphism.

CategoryTheory.asIso_hom theorem

(f : X ⟶ Y) {_ : IsIso f} : (asIso f).hom = f

Full source

@[simp]
theorem asIso_hom (f : X ⟶ Y) {_ : IsIso f} : (asIso f).hom = f :=
  rfl

Forward Morphism of Isomorphism Construction

Informal description

For any morphism $f \colon X \to Y$ in a category $\mathcal{C}$ that is an isomorphism (i.e., `[IsIso f]` holds), the forward morphism of the isomorphism `asIso f` is equal to $f$.

CategoryTheory.asIso_inv theorem

(f : X ⟶ Y) {_ : IsIso f} : (asIso f).inv = inv f

Full source

@[simp]
theorem asIso_inv (f : X ⟶ Y) {_ : IsIso f} : (asIso f).inv = inv f :=
  rfl

Inverse of Isomorphism Construction Equals Categorical Inverse

Informal description

For any morphism $f : X \to Y$ in a category that is an isomorphism, the inverse morphism of the isomorphism `asIso f` equals the categorical inverse `inv f$ of $f$.

CategoryTheory.IsIso.epi_of_iso instance

(f : X ⟶ Y) [IsIso f] : Epi f

Full source

instance (priority := 100) epi_of_iso (f : X ⟶ Y) [IsIso f] : Epi f where
  left_cancellation g h w := by
    rw [← IsIso.inv_hom_id_assoc f g, w, IsIso.inv_hom_id_assoc f h]

Isomorphisms are Epimorphisms

Informal description

For any isomorphism $f : X \to Y$ in a category, $f$ is an epimorphism.

CategoryTheory.IsIso.mono_of_iso instance

(f : X ⟶ Y) [IsIso f] : Mono f

Full source

instance (priority := 100) mono_of_iso (f : X ⟶ Y) [IsIso f] : Mono f where
  right_cancellation g h w := by
    rw [← Category.comp_id g, ← Category.comp_id h, ← IsIso.hom_inv_id f,
      ← Category.assoc, w, ← Category.assoc]

Isomorphisms are Monomorphisms

Informal description

For any isomorphism $f : X \to Y$ in a category, $f$ is a monomorphism.

CategoryTheory.IsIso.inv_eq_of_hom_inv_id theorem

{f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (hom_inv_id : f ≫ g = 𝟙 X) : inv f = g

Full source

@[aesop apply safe (rule_sets := [CategoryTheory])]
theorem inv_eq_of_hom_inv_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (hom_inv_id : f ≫ g = 𝟙 X) :
    inv f = g := by
  apply (cancel_epi f).mp
  simp [hom_inv_id]

Inverse Characterization via Left Composition Identity: $\text{inv}(f) = g$ when $f \circ g = \text{id}_X$

Informal description

For any isomorphism $f : X \to Y$ in a category and any morphism $g : Y \to X$ such that $f \circ g = \text{id}_X$, the inverse of $f$ is equal to $g$.

CategoryTheory.IsIso.inv_eq_of_inv_hom_id theorem

{f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (inv_hom_id : g ≫ f = 𝟙 Y) : inv f = g

Full source

theorem inv_eq_of_inv_hom_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (inv_hom_id : g ≫ f = 𝟙 Y) :
    inv f = g := by
  apply (cancel_mono f).mp
  simp [inv_hom_id]

Inverse Characterization via Right Composition Identity: $\text{inv}(f) = g$ when $g \circ f = \text{id}_Y$

Informal description

For any isomorphism $f : X \to Y$ in a category and any morphism $g : Y \to X$ such that $g \circ f = \text{id}_Y$, the inverse of $f$ is equal to $g$.

CategoryTheory.IsIso.id instance

(X : C) : IsIso (𝟙 X)

Full source

instance id (X : C) : IsIso (𝟙 X) := ⟨⟨𝟙 X, by simp⟩⟩

Identity Morphism is an Isomorphism

Informal description

For any object $X$ in a category $\mathcal{C}$, the identity morphism $\text{id}_X : X \to X$ is an isomorphism.

CategoryTheory.IsIso.inv_isIso instance

[IsIso f] : IsIso (inv f)

Full source

instance inv_isIso [IsIso f] : IsIso (inv f) :=
  (asIso f).isIso_inv

Inverse of an Isomorphism is an Isomorphism

Informal description

For any morphism $f : X \to Y$ in a category $\mathcal{C}$, if $f$ is an isomorphism, then its inverse $f^{-1} : Y \to X$ is also an isomorphism.

CategoryTheory.IsIso.comp_isIso instance

[IsIso f] [IsIso h] : IsIso (f ≫ h)

Full source

instance (priority := 900) comp_isIso [IsIso f] [IsIso h] : IsIso (f ≫ h) :=
  (asIsoasIso f ≪≫ asIso h).isIso_hom

Composition of Isomorphisms is an Isomorphism

Informal description

For any two morphisms $f$ and $h$ in a category $\mathcal{C}$, if both $f$ and $h$ are isomorphisms, then their composition $f \circ h$ is also an isomorphism.

CategoryTheory.IsIso.comp_isIso' theorem

(_ : IsIso f) (_ : IsIso h) : IsIso (f ≫ h)

Full source

/--
The composition of isomorphisms is an isomorphism. Here the arguments of type `IsIso` are
explicit, to make this easier to use with the `refine` tactic, for instance.
-/
lemma comp_isIso' (_ : IsIso f) (_ : IsIso h) : IsIso (f ≫ h) := inferInstance

Composition of Isomorphisms is an Isomorphism (explicit version)

Informal description

Given two morphisms $f$ and $h$ in a category $\mathcal{C}$, if both $f$ and $h$ are isomorphisms, then their composition $f \circ h$ is also an isomorphism.

CategoryTheory.IsIso.inv_id theorem

: inv (𝟙 X) = 𝟙 X

Full source

@[simp]
theorem inv_id : inv (𝟙 X) = 𝟙 X := by
  apply inv_eq_of_hom_inv_id
  simp

Inverse of Identity Morphism is Identity

Informal description

The inverse of the identity morphism $\text{id}_X : X \to X$ in a category is itself, i.e., $\text{inv}(\text{id}_X) = \text{id}_X$.

CategoryTheory.IsIso.inv_comp theorem

[IsIso f] [IsIso h] : inv (f ≫ h) = inv h ≫ inv f

Full source

@[simp, reassoc]
theorem inv_comp [IsIso f] [IsIso h] : inv (f ≫ h) = invinv h ≫ inv f := by
  apply inv_eq_of_hom_inv_id
  simp

Inverse of Composition: $(f \circ h)^{-1} = h^{-1} \circ f^{-1}$

Informal description

For any two isomorphisms $f$ and $h$ in a category, the inverse of their composition is equal to the composition of their inverses in reverse order, i.e., $(f \circ h)^{-1} = h^{-1} \circ f^{-1}$.

CategoryTheory.IsIso.inv_inv theorem

[IsIso f] : inv (inv f) = f

Full source

@[simp]
theorem inv_inv [IsIso f] : inv (inv f) = f := by
  apply inv_eq_of_hom_inv_id
  simp

Double Inverse of an Isomorphism Equals Original Morphism

Informal description

For any isomorphism $f : X \to Y$ in a category, the inverse of the inverse of $f$ is equal to $f$ itself, i.e., $(f^{-1})^{-1} = f$.

CategoryTheory.IsIso.Iso.inv_inv theorem

(f : X ≅ Y) : inv f.inv = f.hom

Full source

@[simp]
theorem Iso.inv_inv (f : X ≅ Y) : inv f.inv = f.hom := by
  apply inv_eq_of_hom_inv_id
  simp

Double Inverse of an Isomorphism Equals Original Morphism: $(f^{-1})^{-1} = f$

Informal description

For any isomorphism $f \colon X \cong Y$ in a category $\mathcal{C}$, the inverse of the inverse morphism $f_{\text{inv}}$ is equal to the original morphism $f_{\text{hom}}$, i.e., $(f^{-1})^{-1} = f$.

CategoryTheory.IsIso.Iso.inv_hom theorem

(f : X ≅ Y) : inv f.hom = f.inv

Full source

@[simp]
theorem Iso.inv_hom (f : X ≅ Y) : inv f.hom = f.inv := by
  apply inv_eq_of_hom_inv_id
  simp

Inverse of Isomorphism Homomorphism Equals Its Inverse Morphism

Informal description

For any isomorphism $f \colon X \cong Y$ in a category, the inverse of the homomorphism $f_{\text{hom}} \colon X \to Y$ is equal to the inverse morphism $f_{\text{inv}} \colon Y \to X$ defined by the isomorphism.

CategoryTheory.IsIso.inv_comp_eq theorem

(α : X ⟶ Y) [IsIso α] {f : X ⟶ Z} {g : Y ⟶ Z} : inv α ≫ f = g ↔ f = α ≫ g

Full source

@[simp]
theorem inv_comp_eq (α : X ⟶ Y) [IsIso α] {f : X ⟶ Z} {g : Y ⟶ Z} : invinv α ≫ finv α ≫ f = g ↔ f = α ≫ g :=
  (asIso α).inv_comp_eq

Inverse Composition Equivalence for Isomorphisms

Informal description

Let $\mathcal{C}$ be a category, and let $\alpha : X \to Y$ be an isomorphism in $\mathcal{C}$. For any morphisms $f : X \to Z$ and $g : Y \to Z$, the composition $\alpha^{-1} \circ f$ equals $g$ if and only if $f$ equals $\alpha \circ g$.

CategoryTheory.IsIso.comp_inv_eq theorem

(α : X ⟶ Y) [IsIso α] {f : Z ⟶ Y} {g : Z ⟶ X} : f ≫ inv α = g ↔ f = g ≫ α

Full source

@[simp]
theorem comp_inv_eq (α : X ⟶ Y) [IsIso α] {f : Z ⟶ Y} {g : Z ⟶ X} : f ≫ inv αf ≫ inv α = g ↔ f = g ≫ α :=
  (asIso α).comp_inv_eq

Composition with Inverse Equals Morphism iff Morphism Equals Composition with Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $\alpha : X \to Y$ be an isomorphism in $\mathcal{C}$. For any morphisms $f : Z \to Y$ and $g : Z \to X$, the composition $f \circ \alpha^{-1}$ equals $g$ if and only if $f$ equals $g \circ \alpha$.

CategoryTheory.IsIso.of_isIso_comp_left theorem

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [IsIso (f ≫ g)] : IsIso g

Full source

theorem of_isIso_comp_left {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [IsIso (f ≫ g)] :
    IsIso g := by
  rw [← id_comp g, ← inv_hom_id f, assoc]
  infer_instance

Isomorphism Property via Left Composition with Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $f : X \to Y$ and $g : Y \to Z$ be morphisms in $\mathcal{C}$. If $f$ is an isomorphism and the composition $f \circ g$ is also an isomorphism, then $g$ is an isomorphism.

CategoryTheory.IsIso.of_isIso_comp_right theorem

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] [IsIso (f ≫ g)] : IsIso f

Full source

theorem of_isIso_comp_right {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] [IsIso (f ≫ g)] :
    IsIso f := by
  rw [← comp_id f, ← hom_inv_id g, ← assoc]
  infer_instance

Right Factor of Isomorphism Composition is Isomorphism

Informal description

Let $f : X \to Y$ and $g : Y \to Z$ be morphisms in a category $\mathcal{C}$. If $g$ is an isomorphism and the composition $f \circ g$ is also an isomorphism, then $f$ is an isomorphism.

CategoryTheory.IsIso.of_isIso_fac_left theorem

{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [IsIso f] [hh : IsIso h] (w : f ≫ g = h) : IsIso g

Full source

theorem of_isIso_fac_left {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [IsIso f]
    [hh : IsIso h] (w : f ≫ g = h) : IsIso g := by
  rw [← w] at hh
  haveI := hh
  exact of_isIso_comp_left f g

Left Factor of Isomorphism Composition is Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $f : X \to Y$, $g : Y \to Z$, and $h : X \to Z$ be morphisms in $\mathcal{C}$. If $f$ is an isomorphism, $h$ is an isomorphism, and the composition $f \circ g$ equals $h$ (i.e., $f \circ g = h$), then $g$ is an isomorphism.

CategoryTheory.IsIso.of_isIso_fac_right theorem

{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [IsIso g] [hh : IsIso h] (w : f ≫ g = h) : IsIso f

Full source

theorem of_isIso_fac_right {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [IsIso g]
    [hh : IsIso h] (w : f ≫ g = h) : IsIso f := by
  rw [← w] at hh
  haveI := hh
  exact of_isIso_comp_right f g

Right Factor of Isomorphism Composition is Isomorphism

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be morphisms in a category $\mathcal{C}$, and let $h \colon X \to Z$ be their composition, i.e., $f \circ g = h$. If $g$ is an isomorphism and $h$ is an isomorphism, then $f$ is also an isomorphism.

CategoryTheory.IsIso.inv_eq_inv theorem

{f g : X ⟶ Y} [IsIso f] [IsIso g] : inv f = inv g ↔ f = g

Full source

theorem IsIso.inv_eq_inv {f g : X ⟶ Y} [IsIso f] [IsIso g] : invinv f = inv g ↔ f = g :=
  Iso.inv_eq_inv (asIso f) (asIso g)

Inverse Equality of Isomorphisms is Equivalent to Morphism Equality

Informal description

For any two isomorphisms $f, g \colon X \to Y$ in a category $\mathcal{C}$, the inverses $f^{-1}$ and $g^{-1}$ are equal if and only if $f$ and $g$ are equal.

CategoryTheory.hom_comp_eq_id theorem

(g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} : g ≫ f = 𝟙 X ↔ f = inv g

Full source

theorem hom_comp_eq_id (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} : g ≫ fg ≫ f = 𝟙 X ↔ f = inv g :=
  (asIso g).hom_comp_eq_id

Composition with Isomorphism Equals Identity iff Morphism is Inverse

Informal description

For any isomorphism $g \colon X \to Y$ in a category $\mathcal{C}$ and any morphism $f \colon Y \to X$, the composition $g \circ f$ equals the identity morphism $\text{id}_X$ if and only if $f$ is equal to the inverse morphism $g^{-1}$ of $g$.

CategoryTheory.comp_hom_eq_id theorem

(g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} : f ≫ g = 𝟙 Y ↔ f = inv g

Full source

theorem comp_hom_eq_id (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} : f ≫ gf ≫ g = 𝟙 Y ↔ f = inv g :=
  (asIso g).comp_hom_eq_id

Composition with Isomorphism Equals Identity iff Morphism is Inverse

Informal description

For any isomorphism $g \colon X \to Y$ in a category $\mathcal{C}$ and any morphism $f \colon Y \to X$, the composition $f \circ g$ equals the identity morphism $\text{id}_Y$ if and only if $f$ is equal to the inverse morphism $g^{-1}$ of $g$.

CategoryTheory.inv_comp_eq_id theorem

(g : X ⟶ Y) [IsIso g] {f : X ⟶ Y} : inv g ≫ f = 𝟙 Y ↔ f = g

Full source

theorem inv_comp_eq_id (g : X ⟶ Y) [IsIso g] {f : X ⟶ Y} : invinv g ≫ finv g ≫ f = 𝟙 Y ↔ f = g :=
  (asIso g).inv_comp_eq_id

Inverse Composition Equals Identity iff Morphism is Original Isomorphism

Informal description

For any isomorphism $g \colon X \to Y$ in a category $\mathcal{C}$ and any morphism $f \colon X \to Y$, the composition $g^{-1} \circ f$ equals the identity morphism $\text{id}_Y$ if and only if $f = g$.

CategoryTheory.comp_inv_eq_id theorem

(g : X ⟶ Y) [IsIso g] {f : X ⟶ Y} : f ≫ inv g = 𝟙 X ↔ f = g

Full source

theorem comp_inv_eq_id (g : X ⟶ Y) [IsIso g] {f : X ⟶ Y} : f ≫ inv gf ≫ inv g = 𝟙 X ↔ f = g :=
  (asIso g).comp_inv_eq_id

Composition with Inverse Isomorphism Yields Identity iff Morphism is the Isomorphism

Informal description

For any isomorphism $g \colon X \to Y$ in a category $\mathcal{C}$ and any morphism $f \colon X \to Y$, the composition $f \circ g^{-1}$ equals the identity morphism $\text{id}_X$ if and only if $f = g$.

CategoryTheory.isIso_of_hom_comp_eq_id theorem

(g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} (h : g ≫ f = 𝟙 X) : IsIso f

Full source

theorem isIso_of_hom_comp_eq_id (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} (h : g ≫ f = 𝟙 X) : IsIso f := by
  rw [(hom_comp_eq_id _).mp h]
  infer_instance

Morphism is Isomorphism if Composition with Isomorphism Yields Identity

Informal description

Let $g \colon X \to Y$ be an isomorphism in a category $\mathcal{C}$ and $f \colon Y \to X$ be a morphism such that $g \circ f = \text{id}_X$. Then $f$ is an isomorphism.

CategoryTheory.isIso_of_comp_hom_eq_id theorem

(g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} (h : f ≫ g = 𝟙 Y) : IsIso f

Full source

theorem isIso_of_comp_hom_eq_id (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} (h : f ≫ g = 𝟙 Y) : IsIso f := by
  rw [(comp_hom_eq_id _).mp h]
  infer_instance

Morphism is Isomorphism if Post-Composition with Isomorphism Yields Identity

Informal description

Let $g \colon X \to Y$ be an isomorphism in a category $\mathcal{C}$ and $f \colon Y \to X$ be a morphism such that $f \circ g = \text{id}_Y$. Then $f$ is an isomorphism.

CategoryTheory.Iso.inv_ext theorem

{f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : f.hom ≫ g = 𝟙 X) : f.inv = g

Full source

@[aesop apply safe (rule_sets := [CategoryTheory])]
theorem inv_ext {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : f.hom ≫ g = 𝟙 X) : f.inv = g :=
  ((hom_comp_eq_id f).1 hom_inv_id).symm

Inverse of Isomorphism is Unique Given Homomorphism Composition Condition

Informal description

For any isomorphism $f \colon X \cong Y$ in a category $\mathcal{C}$ and any morphism $g \colon Y \to X$, if the composition $f_{\text{hom}} \circ g$ equals the identity morphism $\text{id}_X$, then the inverse morphism $f_{\text{inv}}$ of $f$ is equal to $g$.

CategoryTheory.Iso.inv_ext' theorem

{f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : f.hom ≫ g = 𝟙 X) : g = f.inv

Full source

@[aesop apply safe (rule_sets := [CategoryTheory])]
theorem inv_ext' {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : f.hom ≫ g = 𝟙 X) : g = f.inv :=
  (hom_comp_eq_id f).1 hom_inv_id

Uniqueness of Isomorphism Inverse via Homomorphism Composition

Informal description

For any isomorphism $f \colon X \cong Y$ in a category $\mathcal{C}$ and any morphism $g \colon Y \to X$, if the composition $f_{\text{hom}} \circ g$ equals the identity morphism $\text{id}_X$, then $g$ is equal to the inverse morphism $f_{\text{inv}}$ of $f$.

CategoryTheory.Iso.cancel_iso_hom_left theorem

{X Y Z : C} (f : X ≅ Y) (g g' : Y ⟶ Z) : f.hom ≫ g = f.hom ≫ g' ↔ g = g'

Full source

@[simp]
theorem cancel_iso_hom_left {X Y Z : C} (f : X ≅ Y) (g g' : Y ⟶ Z) :
    f.hom ≫ gf.hom ≫ g = f.hom ≫ g' ↔ g = g' := by
  simp only [cancel_epi]

Left cancellation of isomorphism homomorphism

Informal description

For any isomorphism $f \colon X \cong Y$ and any morphisms $g, g' \colon Y \to Z$ in a category $\mathcal{C}$, the compositions $f_{\text{hom}} \circ g$ and $f_{\text{hom}} \circ g'$ are equal if and only if $g = g'$.

CategoryTheory.Iso.cancel_iso_inv_left theorem

{X Y Z : C} (f : Y ≅ X) (g g' : Y ⟶ Z) : f.inv ≫ g = f.inv ≫ g' ↔ g = g'

Full source

@[simp]
theorem cancel_iso_inv_left {X Y Z : C} (f : Y ≅ X) (g g' : Y ⟶ Z) :
    f.inv ≫ gf.inv ≫ g = f.inv ≫ g' ↔ g = g' := by
  simp only [cancel_epi]

Left cancellation of isomorphism inverse: $f^{-1} \circ g = f^{-1} \circ g' \leftrightarrow g = g'$

Informal description

For any isomorphism $f \colon Y \cong X$ and any morphisms $g, g' \colon Y \to Z$ in a category $\mathcal{C}$, the compositions $f^{-1} \circ g$ and $f^{-1} \circ g'$ are equal if and only if $g = g'$.

CategoryTheory.Iso.cancel_iso_hom_right theorem

{X Y Z : C} (f f' : X ⟶ Y) (g : Y ≅ Z) : f ≫ g.hom = f' ≫ g.hom ↔ f = f'

Full source

@[simp]
theorem cancel_iso_hom_right {X Y Z : C} (f f' : X ⟶ Y) (g : Y ≅ Z) :
    f ≫ g.homf ≫ g.hom = f' ≫ g.hom ↔ f = f' := by
  simp only [cancel_mono]

Right cancellation of isomorphism homomorphism

Informal description

For any morphisms $f, f' \colon X \to Y$ and any isomorphism $g \colon Y \cong Z$ in a category $\mathcal{C}$, the compositions $f \circ g_{\text{hom}}$ and $f' \circ g_{\text{hom}}$ are equal if and only if $f = f'$.

CategoryTheory.Iso.cancel_iso_inv_right theorem

{X Y Z : C} (f f' : X ⟶ Y) (g : Z ≅ Y) : f ≫ g.inv = f' ≫ g.inv ↔ f = f'

Full source

@[simp]
theorem cancel_iso_inv_right {X Y Z : C} (f f' : X ⟶ Y) (g : Z ≅ Y) :
    f ≫ g.invf ≫ g.inv = f' ≫ g.inv ↔ f = f' := by
  simp only [cancel_mono]

Cancellation of Isomorphism Inverse on the Right

Informal description

For any morphisms $f, f' \colon X \to Y$ and isomorphism $g \colon Z \cong Y$ in a category $\mathcal{C}$, the equality $f \circ g^{-1} = f' \circ g^{-1}$ holds if and only if $f = f'$.

CategoryTheory.Iso.cancel_iso_hom_right_assoc theorem

 {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) (h : Y ≅ Z) :
  f ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom ↔ f ≫ g = f' ≫ g'

Full source

@[simp]
theorem cancel_iso_hom_right_assoc {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
    (g' : X' ⟶ Y) (h : Y ≅ Z) : f ≫ g ≫ h.homf ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom ↔ f ≫ g = f' ≫ g' := by
  simp only [← Category.assoc, cancel_mono]

Cancellation of Isomorphism Homomorphism in Composition

Informal description

For any morphisms $f \colon W \to X$, $g \colon X \to Y$, $f' \colon W \to X'$, $g' \colon X' \to Y$ in a category $\mathcal{C}$, and any isomorphism $h \colon Y \cong Z$, the equality $f \circ g \circ h_{\text{hom}} = f' \circ g' \circ h_{\text{hom}}$ holds if and only if $f \circ g = f' \circ g'$.

CategoryTheory.Iso.cancel_iso_inv_right_assoc theorem

 {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) (h : Z ≅ Y) :
  f ≫ g ≫ h.inv = f' ≫ g' ≫ h.inv ↔ f ≫ g = f' ≫ g'

Full source

@[simp]
theorem cancel_iso_inv_right_assoc {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
    (g' : X' ⟶ Y) (h : Z ≅ Y) : f ≫ g ≫ h.invf ≫ g ≫ h.inv = f' ≫ g' ≫ h.inv ↔ f ≫ g = f' ≫ g' := by
  simp only [← Category.assoc, cancel_mono]

Cancellation of Isomorphism Inverse in Composition: $f \circ g \circ h^{-1} = f' \circ g' \circ h^{-1} \leftrightarrow f \circ g = f' \circ g'$

Informal description

For any morphisms $f \colon W \to X$, $g \colon X \to Y$, $f' \colon W \to X'$, $g' \colon X' \to Y$ in a category $\mathcal{C}$, and any isomorphism $h \colon Z \cong Y$, the equality $f \circ g \circ h^{-1} = f' \circ g' \circ h^{-1}$ holds if and only if $f \circ g = f' \circ g'$.

CategoryTheory.Iso.map_hom_inv_id theorem

(F : C ⥤ D) : F.map e.hom ≫ F.map e.inv = 𝟙 _

Full source

@[reassoc (attr := simp)]
lemma map_hom_inv_id (F : C ⥤ D) :
    F.map e.hom ≫ F.map e.inv = 𝟙 _ := by
  rw [← F.map_comp, e.hom_inv_id, F.map_id]

Functor Preserves Isomorphism Composition: $F(e) \circ F(e^{-1}) = \text{id}$

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories and any isomorphism $e \colon X \cong Y$ in $\mathcal{C}$, the composition of the functor-applied morphisms $F(e_{\text{hom}}) \circ F(e_{\text{inv}})$ equals the identity morphism on $F(Y)$, i.e., $F(e_{\text{hom}}) \circ F(e_{\text{inv}}) = \text{id}_{F(Y)}$.

CategoryTheory.Iso.map_inv_hom_id theorem

(F : C ⥤ D) : F.map e.inv ≫ F.map e.hom = 𝟙 _

Full source

@[reassoc (attr := simp)]
lemma map_inv_hom_id (F : C ⥤ D) :
    F.map e.inv ≫ F.map e.hom = 𝟙 _ := by
  rw [← F.map_comp, e.inv_hom_id, F.map_id]

Functoriality of Isomorphism Composition: $F(e^{-1}) \circ F(e) = \text{id}$

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories and any isomorphism $e \colon X \cong Y$ in $\mathcal{C}$, the composition of the functor-applied inverse morphism $F(e^{-1})$ followed by the functor-applied forward morphism $F(e)$ equals the identity morphism on $F(Y)$, i.e., $F(e^{-1}) \circ F(e) = \text{id}_{F(Y)}$.

CategoryTheory.Functor.mapIso definition

(F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y

Full source

/-- A functor `F : C ⥤ D` sends isomorphisms `i : X ≅ Y` to isomorphisms `F.obj X ≅ F.obj Y` -/
@[simps]
def mapIso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y where
  hom := F.map i.hom
  inv := F.map i.inv

Functorial mapping of isomorphisms

Informal description

Given a functor $ F : \mathcal{C} \to \mathcal{D} $ between categories and an isomorphism $ i : X \cong Y $ in $ \mathcal{C} $, the functor $ F $ maps $ i $ to an isomorphism $ F(X) \cong F(Y) $ in $ \mathcal{D} $, where the morphisms are given by $ F(i_{\text{hom}}) $ and $ F(i_{\text{inv}}) $.

CategoryTheory.Functor.mapIso_symm theorem

(F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.mapIso i.symm = (F.mapIso i).symm

Full source

@[simp]
theorem mapIso_symm (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.mapIso i.symm = (F.mapIso i).symm :=
  rfl

Functoriality of Inverse Isomorphism: $F(i^{-1}) = F(i)^{-1}$

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories and any isomorphism $i \colon X \cong Y$ in $\mathcal{C}$, the functor $F$ maps the inverse isomorphism $i^{-1} \colon Y \cong X$ to the inverse of the isomorphism $F(i) \colon F(X) \cong F(Y)$, i.e., $F(i^{-1}) = F(i)^{-1}$.

CategoryTheory.Functor.mapIso_trans theorem

(F : C ⥤ D) {X Y Z : C} (i : X ≅ Y) (j : Y ≅ Z) : F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j

Full source

@[simp]
theorem mapIso_trans (F : C ⥤ D) {X Y Z : C} (i : X ≅ Y) (j : Y ≅ Z) :
    F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j := by
  ext; apply Functor.map_comp

Functoriality of Isomorphism Composition: $F(i \circ j) = F(i) \circ F(j)$

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories and any isomorphisms $i \colon X \cong Y$ and $j \colon Y \cong Z$ in $\mathcal{C}$, the functor $F$ maps the composition of isomorphisms $i \ggg j$ to the composition of the mapped isomorphisms $F(i) \ggg F(j)$, i.e., $F(i \ggg j) = F(i) \ggg F(j)$.

CategoryTheory.Functor.mapIso_refl theorem

(F : C ⥤ D) (X : C) : F.mapIso (Iso.refl X) = Iso.refl (F.obj X)

Full source

@[simp]
theorem mapIso_refl (F : C ⥤ D) (X : C) : F.mapIso (Iso.refl X) = Iso.refl (F.obj X) :=
  Iso.ext <| F.map_id X

Functoriality of Identity Isomorphism: $F(\text{id}_X) = \text{id}_{F(X)}$

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories and any object $X$ in $\mathcal{C}$, the functor $F$ maps the identity isomorphism $\text{id}_X \colon X \cong X$ to the identity isomorphism $\text{id}_{F(X)} \colon F(X) \cong F(X)$.

CategoryTheory.Functor.map_isIso instance

(F : C ⥤ D) (f : X ⟶ Y) [IsIso f] : IsIso (F.map f)

Full source

instance map_isIso (F : C ⥤ D) (f : X ⟶ Y) [IsIso f] : IsIso (F.map f) :=
  (F.mapIso (asIso f)).isIso_hom

Functor Preserves Isomorphisms

Informal description

For any functor $F : \mathcal{C} \to \mathcal{D}$ between categories and any isomorphism $f : X \to Y$ in $\mathcal{C}$, the morphism $F(f) : F(X) \to F(Y)$ is also an isomorphism in $\mathcal{D}$.

CategoryTheory.Functor.map_inv theorem

(F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] : F.map (inv f) = inv (F.map f)

Full source

@[simp]
theorem map_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] : F.map (inv f) = inv (F.map f) := by
  apply eq_inv_of_hom_inv_id
  simp [← F.map_comp]

Functoriality of Inverse Morphism: $F(f^{-1}) = (F(f))^{-1}$

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories and any isomorphism $f \colon X \to Y$ in $\mathcal{C}$, the functor $F$ maps the inverse morphism $f^{-1}$ to the inverse of $F(f)$, i.e., $F(f^{-1}) = (F(f))^{-1}$.

CategoryTheory.Functor.map_hom_inv theorem

(F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] : F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)

Full source

@[reassoc]
theorem map_hom_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] :
    F.map f ≫ F.map (inv f) = 𝟙 (F.obj X) := by simp

Functoriality of Isomorphism Composition: $F(f) \circ F(f^{-1}) = \text{id}_{F(X)}$

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories and any isomorphism $f \colon X \to Y$ in $\mathcal{C}$, the composition of $F(f)$ with its inverse $F(f^{-1})$ equals the identity morphism on $F(X)$, i.e., $F(f) \circ F(f^{-1}) = \text{id}_{F(X)}$.

CategoryTheory.Functor.map_inv_hom theorem

(F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] : F.map (inv f) ≫ F.map f = 𝟙 (F.obj Y)

Full source

@[reassoc]
theorem map_inv_hom (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] :
    F.map (inv f) ≫ F.map f = 𝟙 (F.obj Y) := by simp

Functoriality of Inverse Composition: $F(f^{-1}) \circ F(f) = \text{id}_{F(Y)}$

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories and any isomorphism $f \colon X \to Y$ in $\mathcal{C}$, the composition of the functor-applied inverse morphism with the functor-applied morphism yields the identity on $F(Y)$, i.e., $F(f^{-1}) \circ F(f) = \text{id}_{F(Y)}$.

Mathlib.CategoryTheory.Iso

Main definitions

Notations

Tags