Vertical Lifts #
We call a lift v : x ⟶[𝟙 c] y of the identity morphism a vertical lift/morphism.
Question: Can we use extension types to define VertHom so that the proofs of
vertHomOfBasedLift and basedLiftOfVertHom are more concise/automated?
@[reducible, inline]
abbrev
CategoryTheory.Vert
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
(P : CategoryTheory.Functor E C)
:
Type (max u_1 u_2)
Equations
- CategoryTheory.Vert P = ((c : C) × P ⁻¹ c)
Instances For
instance
CategoryTheory.instCategoryVert
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
:
Equations
- CategoryTheory.instCategoryVert = inferInstance
def
CategoryTheory.vertHomOfBasedLift
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{X : CategoryTheory.Vert P}
{Y : CategoryTheory.Vert P}
(h : X.fst = Y.fst)
(f : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id X.fst) X.snd (Fiber.cast Y.snd ⋯))
:
X ⟶ Y
A based-lift of the identity generates a morphism in `Vert P.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.base_eq_of_vert_hom
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{X : CategoryTheory.Vert P}
{Y : CategoryTheory.Vert P}
(f : X ⟶ Y)
:
X.fst = Y.fst
def
CategoryTheory.basedLiftOfVertHomAux
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{X : CategoryTheory.Vert P}
{Y : CategoryTheory.Vert P}
(f : X ⟶ Y)
:
↑X.snd ⟶ ↑Y.snd
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.basedLiftOfVertHomAux_over
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{X : CategoryTheory.Vert P}
{Y : CategoryTheory.Vert P}
{f : X ⟶ Y}
:
let_fun this := ⋯;
CategoryTheory.CategoryStruct.comp (P.map (CategoryTheory.basedLiftOfVertHomAux f)) (CategoryTheory.eqToHom this) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.id X.fst)
def
CategoryTheory.basedLiftOfVertHom
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{X : CategoryTheory.Vert P}
{Y : CategoryTheory.Vert P}
(f : X ⟶ Y)
:
let_fun this := ⋯;
CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id X.fst) X.snd (Fiber.cast Y.snd ⋯)
Equations
- CategoryTheory.basedLiftOfVertHom f = { hom := CategoryTheory.basedLiftOfVertHomAux f, over := ⋯ }
Instances For
def
CategoryTheory.basedLiftOfFiberHom
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{x : P ⁻¹ c}
{y : P ⁻¹ c}
(f : x ⟶ y)
:
Equations
- CategoryTheory.basedLiftOfFiberHom f = { hom := ↑f, over := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.instCoeFiberHom_coe_coe
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{x : P ⁻¹ c}
{y : P ⁻¹ c}
(f : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x y)
:
instance
CategoryTheory.instCoeFiberHom
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{x : P ⁻¹ c}
{y : P ⁻¹ c}
:
Coe (CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x y) (x ⟶ y)
Coercing a based-lift x ⟶[𝟙 c] y of the identity morphism 𝟙 c
to a morphism x ⟶ y in the fiber P⁻¹ c.
Equations
- CategoryTheory.instCoeFiberHom = { coe := fun (f : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x y) => ⟨f.hom, ⋯⟩ }
@[simp]
theorem
CategoryTheory.equivFiberHomBasedLift_apply_hom
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{x : P ⁻¹ c}
{y : P ⁻¹ c}
(g : x ⟶ y)
:
(CategoryTheory.equivFiberHomBasedLift g).hom = ↑g
@[simp]
theorem
CategoryTheory.equivFiberHomBasedLift_symm_apply_coe
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{x : P ⁻¹ c}
{y : P ⁻¹ c}
(g : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x y)
:
↑(CategoryTheory.equivFiberHomBasedLift.symm g) = g.hom
def
CategoryTheory.equivFiberHomBasedLift
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{x : P ⁻¹ c}
{y : P ⁻¹ c}
:
(x ⟶ y) ≃ CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x y
The bijection between the hom-type of the fiber P⁻¹ c and the based-lifts of the identity morphism of c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.equivVertHomBasedLift_apply_hom
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{x : P ⁻¹ c}
{y : P ⁻¹ c}
(g : ⟨c, x⟩ ⟶ ⟨c, y⟩)
:
(CategoryTheory.equivVertHomBasedLift g).hom = CategoryTheory.Sigma.SigmaHom.rec (motive :=
fun (a a_1 : (i : C) × P ⁻¹ i) (x_1 : CategoryTheory.Sigma.SigmaHom a a_1) =>
⟨c, x⟩ = a → ⟨c, y⟩ = a_1 → HEq g x_1 → (↑x ⟶ ↑y))
(fun {i : C} {X Y : P ⁻¹ i} (a : X ⟶ Y) (h : ⟨c, x⟩ = ⟨i, X⟩) =>
Eq.rec (motive := fun (x : CategoryTheory.Vert P) (x_1 : ⟨i, X⟩ = x) =>
(f : x ⟶ ⟨c, y⟩) → ⟨c, y⟩ = ⟨i, Y⟩ → HEq f (CategoryTheory.Sigma.SigmaHom.mk a) → (↑x.snd ⟶ ↑y))
(fun (f : ⟨i, X⟩ ⟶ ⟨c, y⟩) (h : ⟨c, y⟩ = ⟨i, Y⟩) =>
Eq.rec (motive := fun (x : CategoryTheory.Vert P) (x_1 : ⟨i, Y⟩ = x) =>
(f : ⟨i, X⟩ ⟶ x) → HEq f (CategoryTheory.Sigma.SigmaHom.mk a) → (↑X ⟶ ↑x.snd))
(fun (f : ⟨i, X⟩ ⟶ ⟨i, Y⟩) (h : HEq f (CategoryTheory.Sigma.SigmaHom.mk a)) => ↑a) ⋯ f)
⋯ g)
g ⋯ ⋯ ⋯
@[simp]
theorem
CategoryTheory.equivVertHomBasedLift_symm_apply
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{x : P ⁻¹ c}
{y : P ⁻¹ c}
(g : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x y)
:
CategoryTheory.equivVertHomBasedLift.symm g = CategoryTheory.vertHomOfBasedLift ⋯ g
def
CategoryTheory.equivVertHomBasedLift
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{x : P ⁻¹ c}
{y : P ⁻¹ c}
:
(⟨c, x⟩ ⟶ ⟨c, y⟩) ≃ CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x y
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.isoVertBasedLiftEquiv
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{x : P ⁻¹ c}
{y : P ⁻¹ c}
:
(x ≅ y) ≃ CategoryTheory.IsoBasedLift (CategoryTheory.CategoryStruct.id c) x y
The bijection between the type of the isomorphisms in the fiber P⁻¹ c and the iso-based-lifts of the identity morphism of c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.vertCartIso_hom
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{e : P ⁻¹ c}
{e' : P ⁻¹ c}
(g : e ⟶ e')
[(CategoryTheory.basedLiftOfFiberHom g).Cartesian]
:
(CategoryTheory.vertCartIso g).hom = g
@[simp]
theorem
CategoryTheory.vertCartIso_inv
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{e : P ⁻¹ c}
{e' : P ⁻¹ c}
(g : e ⟶ e')
[(CategoryTheory.basedLiftOfFiberHom g).Cartesian]
:
(CategoryTheory.vertCartIso g).inv = sorryAx (e' ⟶ e)
def
CategoryTheory.vertCartIso
{C : Type u_1}
{E : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} E]
{P : CategoryTheory.Functor E C}
{c : C}
{e : P ⁻¹ c}
{e' : P ⁻¹ c}
(g : e ⟶ e')
[(CategoryTheory.basedLiftOfFiberHom g).Cartesian]
:
e ≅ e'
Vertical cartesian morphisms are isomorphism.
Equations
- CategoryTheory.vertCartIso g = { hom := g, inv := sorryAx (e' ⟶ e), hom_inv_id := ⋯, inv_hom_id := ⋯ }