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 auxiliary 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.

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
    
    Instances
      theorem CategoryTheory.Functor.IsHomLift.cond {๐’ฎ : Type uโ‚} {๐’ณ : Type uโ‚‚} :
      โˆ€ {inst : CategoryTheory.Category.{vโ‚, uโ‚‚} ๐’ณ} {inst_1 : CategoryTheory.Category.{vโ‚‚, uโ‚} ๐’ฎ} {p : CategoryTheory.Functor ๐’ณ ๐’ฎ} {R S : ๐’ฎ} {a b : ๐’ณ} {f : R โŸถ S} {ฯ† : a โŸถ b} [self : p.IsHomLift f ฯ†], CategoryTheory.IsHomLiftAux p f ฯ†

      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 : ๐’ณ) :
        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) :
        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 ฯ†] :
        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 ฯ†] :
        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 ฯ†] :
        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 ฯˆ] :
        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) ฯˆ] :

        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) :
        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) :
        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) :
        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) :
        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 ฯ†] :
        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 ฯ†] :
        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 ฯ†] :
        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 ฯ†] :
        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] :
        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] :

        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] :
          @[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] :
          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 ฯ†] :

          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) ฯ†] :
          Equations
          • โ‹ฏ = โ‹ฏ