Documentation

Mathlib.CategoryTheory.FiberedCategory.HomLift

HomLift #

Given a functor p : 𝒳 ⥤ 𝒮, this file provides API for expressing the fact that p(φ) = f for given morphisms φ and f. The reason this API is needed is because, in general, p.map φ = f does not make sense when the domain and/or codomain of φ and f are not definitionally equal.

Main definition #

Given morphism φ : a ⟶ b in 𝒳 and f : R ⟶ S in 𝒮, p.IsHomLift f φ is a class, defined using the auxillary inductive type IsHomLiftAux which expresses the fact that f = p(φ).

We also define a macro subst_hom_lift p f φ which can be used to substitute f with p(φ) in a goal, this tactic is just short for obtain ⟨⟩ := Functor.IsHomLift.cond (p:=p) (f:=f) (φ:=φ), and it is used to make the code more readable.

inductive CategoryTheory.IsHomLiftAux {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} :

(R ⟶ S) → (a ⟶ b) → Prop

Helper-type for defining IsHomLift.

map: ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮] {p : CategoryTheory.Functor 𝒳 𝒮} {a b : 𝒳} (φ : a ⟶ b), CategoryTheory.IsHomLiftAux p (p.map φ) φ

Instances For

class CategoryTheory.Functor.IsHomLift {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) :

Given a functor p : 𝒳 ⥤ 𝒮, an arrow φ : a ⟶ b in 𝒳 and an arrow f : R ⟶ S in 𝒮, p.IsHomLift f φ expresses the fact that φ lifts f through p. This is often drawn as:

  a --φ--> b
  -        -
  |        |
  v        v
  R --f--> S

cond : CategoryTheory.IsHomLiftAux p f φ

Instances

theorem CategoryTheory.Functor.IsHomLift.cond {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] {p : CategoryTheory.Functor 𝒳 𝒮} {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [self : p.IsHomLift f φ] :

CategoryTheory.IsHomLiftAux p f φ

def CategoryTheory.tacticSubst_hom_lift___ :

Lean.ParserDescr

subst_hom_lift p f φ tries to substitute f with p(φ) by using p.IsHomLift f φ

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

instance CategoryTheory.instIsHomLiftMap {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {a : 𝒳} {b : 𝒳} (φ : a ⟶ b) :

p.IsHomLift (p.map φ) φ

For any arrow φ : a ⟶ b in 𝒳, φ lifts the arrow p.map φ in the base 𝒮

Equations

⋯ = ⋯

@[simp]

instance CategoryTheory.instIsHomLiftIdObj {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) (a : 𝒳) :

p.IsHomLift (CategoryTheory.CategoryStruct.id (p.obj a)) (CategoryTheory.CategoryStruct.id a)

Equations

⋯ = ⋯

theorem CategoryTheory.IsHomLift.id {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] {p : CategoryTheory.Functor 𝒳 𝒮} {R : 𝒮} {a : 𝒳} (ha : p.obj a = R) :

p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.CategoryStruct.id a)

theorem CategoryTheory.IsHomLift.domain_eq {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] :

p.obj a = R

theorem CategoryTheory.IsHomLift.codomain_eq {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] :

p.obj b = S

theorem CategoryTheory.IsHomLift.fac {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] :

f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (p.map φ) (CategoryTheory.eqToHom ⋯))

theorem CategoryTheory.IsHomLift.fac' {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] :

p.map φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))

theorem CategoryTheory.IsHomLift.commSq {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] :

CategoryTheory.CommSq (p.map φ) (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯) f

theorem CategoryTheory.IsHomLift.eq_of_isHomLift {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {a : 𝒳} {b : 𝒳} (f : p.obj a ⟶ p.obj b) (φ : a ⟶ b) [p.IsHomLift f φ] :

f = p.map φ

theorem CategoryTheory.IsHomLift.of_fac {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S) (h : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (p.map φ) (CategoryTheory.eqToHom hb))) :

p.IsHomLift f φ

theorem CategoryTheory.IsHomLift.of_fac' {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S) (h : p.map φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ha) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))) :

p.IsHomLift f φ

theorem CategoryTheory.IsHomLift.of_commSq {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S) (h : CategoryTheory.CommSq (p.map φ) (CategoryTheory.eqToHom ha) (CategoryTheory.eqToHom hb) f) :

p.IsHomLift f φ

instance CategoryTheory.IsHomLift.comp {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {T : 𝒮} {a : 𝒳} {b : 𝒳} {c : 𝒳} (f : R ⟶ S) (g : S ⟶ T) (φ : a ⟶ b) (ψ : b ⟶ c) [p.IsHomLift f φ] [p.IsHomLift g ψ] :

p.IsHomLift (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)

Equations

⋯ = ⋯

instance CategoryTheory.IsHomLift.lift_id_comp {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) (R : 𝒮) {a : 𝒳} {b : 𝒳} {c : 𝒳} (φ : a ⟶ b) (ψ : b ⟶ c) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) φ] [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ] :

p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.CategoryStruct.comp φ ψ)

If φ : a ⟶ b and ψ : b ⟶ c lift 𝟙 R, then so does φ ≫ ψ

Equations

⋯ = ⋯

instance CategoryTheory.IsHomLift.comp_lift_id_right {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {a : 𝒳} {b : 𝒳} {c : 𝒳} {S : 𝒮} {T : 𝒮} (f : S ⟶ T) (φ : a ⟶ b) [p.IsHomLift f φ] (ψ : b ⟶ c) [p.IsHomLift (CategoryTheory.CategoryStruct.id T) ψ] :

p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ ψ)

Equations

⋯ = ⋯

theorem CategoryTheory.IsHomLift.comp_lift_id_right' {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} {c : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] (T : 𝒮) (ψ : b ⟶ c) [p.IsHomLift (CategoryTheory.CategoryStruct.id T) ψ] :

p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ ψ)

If φ : a ⟶ b lifts f and ψ : b ⟶ c lifts 𝟙 T, then φ ≫ ψ lifts f

instance CategoryTheory.IsHomLift.comp_lift_id_left {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {a : 𝒳} {b : 𝒳} {c : 𝒳} {S : 𝒮} {T : 𝒮} (f : S ⟶ T) (ψ : b ⟶ c) [p.IsHomLift f ψ] (φ : a ⟶ b) [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ] :

p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ ψ)

Equations

⋯ = ⋯

theorem CategoryTheory.IsHomLift.comp_lift_id_left' {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {a : 𝒳} {b : 𝒳} {c : 𝒳} (R : 𝒮) (φ : a ⟶ b) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) φ] {S : 𝒮} {T : 𝒮} (f : S ⟶ T) (ψ : b ⟶ c) [p.IsHomLift f ψ] :

p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ ψ)

If φ : a ⟶ b lifts 𝟙 T and ψ : b ⟶ c lifts f, then φ ≫ ψ lifts f

theorem CategoryTheory.IsHomLift.eqToHom_domain_lift_id {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] {p : CategoryTheory.Functor 𝒳 𝒮} {a : 𝒳} {b : 𝒳} (hab : a = b) {R : 𝒮} (hR : p.obj a = R) :

p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.eqToHom hab)

theorem CategoryTheory.IsHomLift.eqToHom_codomain_lift_id {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] {p : CategoryTheory.Functor 𝒳 𝒮} {a : 𝒳} {b : 𝒳} (hab : a = b) {S : 𝒮} (hS : p.obj b = S) :

p.IsHomLift (CategoryTheory.CategoryStruct.id S) (CategoryTheory.eqToHom hab)

theorem CategoryTheory.IsHomLift.id_lift_eqToHom_domain {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] {p : CategoryTheory.Functor 𝒳 𝒮} {R : 𝒮} {S : 𝒮} (hRS : R = S) {a : 𝒳} (ha : p.obj a = R) :

p.IsHomLift (CategoryTheory.eqToHom hRS) (CategoryTheory.CategoryStruct.id a)

theorem CategoryTheory.IsHomLift.id_lift_eqToHom_codomain {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] {p : CategoryTheory.Functor 𝒳 𝒮} {R : 𝒮} {S : 𝒮} (hRS : R = S) {b : 𝒳} (hb : p.obj b = S) :

p.IsHomLift (CategoryTheory.eqToHom hRS) (CategoryTheory.CategoryStruct.id b)

instance CategoryTheory.IsHomLift.comp_eqToHom_lift {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a' : 𝒳} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : a' = a) [p.IsHomLift f φ] :

p.IsHomLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) φ)

Equations

⋯ = ⋯

instance CategoryTheory.IsHomLift.eqToHom_comp_lift {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} {b' : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : b = b') [p.IsHomLift f φ] :

p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.eqToHom h))

Equations

⋯ = ⋯

instance CategoryTheory.IsHomLift.lift_eqToHom_comp {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R' : 𝒮} {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : R' = R) [p.IsHomLift f φ] :

p.IsHomLift (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) φ

Equations

⋯ = ⋯

instance CategoryTheory.IsHomLift.lift_comp_eqToHom {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {S' : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : S = S') [p.IsHomLift f φ] :

p.IsHomLift (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) φ

Equations

⋯ = ⋯

@[simp]

theorem CategoryTheory.IsHomLift.comp_eqToHom_lift_iff {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a' : 𝒳} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : a' = a) :

p.IsHomLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) φ) ↔ p.IsHomLift f φ

@[simp]

theorem CategoryTheory.IsHomLift.eqToHom_comp_lift_iff {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} {b' : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : b = b') :

p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.eqToHom h)) ↔ p.IsHomLift f φ

@[simp]

theorem CategoryTheory.IsHomLift.lift_eqToHom_comp_iff {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R' : 𝒮} {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : R' = R) :

p.IsHomLift (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) φ ↔ p.IsHomLift f φ

@[simp]

theorem CategoryTheory.IsHomLift.lift_comp_eqToHom_iff {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {S' : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : S = S') :

p.IsHomLift (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) φ ↔ p.IsHomLift f φ

@[simp]

theorem CategoryTheory.IsHomLift.isoOfIsoLift_hom {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom] :

(CategoryTheory.IsHomLift.isoOfIsoLift p f φ).hom = f

def CategoryTheory.IsHomLift.isoOfIsoLift {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom] :

R ≅ S

Given a morphism f : R ⟶ S, and an isomorphism φ : a ≅ b lifting f, isoOfIsoLift f φ is the isomorphism Φ : R ≅ S with Φ.hom = f induced from φ

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem CategoryTheory.IsHomLift.isoOfIsoLift_inv_hom_id {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.IsHomLift.isoOfIsoLift p f φ).inv f = CategoryTheory.CategoryStruct.id S

@[simp]

theorem CategoryTheory.IsHomLift.isoOfIsoLift_hom_inv_id {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom] :

CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsHomLift.isoOfIsoLift p f φ).inv = CategoryTheory.CategoryStruct.id R

theorem CategoryTheory.IsHomLift.isIso_of_lift_isIso {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] [CategoryTheory.IsIso φ] :

CategoryTheory.IsIso f

If φ : a ⟶ b lifts f : R ⟶ S and φ is an isomorphism, then so is f.

instance CategoryTheory.IsHomLift.inv_lift_inv {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ≅ S) (φ : a ≅ b) [p.IsHomLift f.hom φ.hom] :

p.IsHomLift f.inv φ.inv

Given φ : a ≅ b and f : R ≅ S, such that φ.hom lifts f.hom, then φ.inv lifts f.inv.

Equations

⋯ = ⋯

instance CategoryTheory.IsHomLift.inv_lift {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom] :

p.IsHomLift (CategoryTheory.IsHomLift.isoOfIsoLift p f φ).inv φ.inv

Given φ : a ≅ b and f : R ⟶ S, such that φ.hom lifts f, then φ.inv lifts the inverse of f given by isoOfIsoLift.

Equations

⋯ = ⋯

instance CategoryTheory.IsHomLift.inv {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [CategoryTheory.IsIso f] [CategoryTheory.IsIso φ] [p.IsHomLift f φ] :

p.IsHomLift (CategoryTheory.inv f) (CategoryTheory.inv φ)

If φ : a ⟶ b lifts f : R ⟶ S and both are isomorphisms, then φ⁻¹ lifts f⁻¹.

Equations

⋯ = ⋯

instance CategoryTheory.IsHomLift.lift_id_inv {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) (S : 𝒮) {a : 𝒳} {b : 𝒳} (φ : a ≅ b) [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ.hom] :

p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ.inv

If φ : a ≅ b is an isomorphism lifting 𝟙 S for some S : 𝒮, then φ⁻¹ also lifts 𝟙 S.

Equations

⋯ = ⋯

instance CategoryTheory.IsHomLift.lift_id_inv_isIso {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₂} 𝒳] [CategoryTheory.Category.{v₂, u₁} 𝒮] (p : CategoryTheory.Functor 𝒳 𝒮) (S : 𝒮) {a : 𝒳} {b : 𝒳} (φ : a ⟶ b) [CategoryTheory.IsIso φ] [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ] :

p.IsHomLift (CategoryTheory.CategoryStruct.id S) (CategoryTheory.inv φ)

Equations

⋯ = ⋯