Widget test for fibred category theory #
def
CategoryTheory.eqToHomMap
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{I : C}
{I' : C}
{J : C}
{J' : C}
(w : I = I')
(w' : J = J')
(f : I ⟶ J)
:
I' ⟶ J'
Transporting a morphism f : I ⟶ J along equalities w : I = I' and w' : J = J'.
Note: It might be a good idea to add this to eqToHom file.
Equations
- CategoryTheory.eqToHomMap w w' f = w' ▸ w ▸ f
Instances For
@[simp]
theorem
CategoryTheory.eqToHomMap_naturality'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{I : C}
{I' : C}
{J : C}
{J' : C}
{w : I = I'}
{w' : J = J'}
(f : I ⟶ J)
:
The diagram below commutes:
I --eqToHom w --> J
| |
f | | eqToHomMap w w' f
v v
I' --eqToHom w'-> J'
def
CategoryTheory.eqToHomMap'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{I : C}
{I' : C}
{J : C}
{J' : C}
(w : I = I')
(w' : J = J')
(f : I ⟶ J)
:
I' ⟶ J'
Transporting a morphism f : I ⟶ J along equalities w : I = I' and w' : J = J'.
Note: It might be a good idea to add this to eqToHom file.
Equations
- CategoryTheory.eqToHomMap' w w' f = let a := CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f; let b := CategoryTheory.CategoryStruct.comp a (CategoryTheory.eqToHom w'); b
Instances For
class
CategoryTheory.DisplayStruct
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
(F : C → Type u_2)
:
Type (max (max (max u_1 u_2) (u_3 + 1)) u_4)
The type of morphisms indexed over morphisms of
C.- id_over : {I : C} → (X : F I) → X ⟶[CategoryTheory.CategoryStruct.id I] X
The identity morphism overlying the identity morphism of
C. - comp_over : {I J K : C} → {f₁ : I ⟶ J} → {f₂ : J ⟶ K} → {X : F I} → {Y : F J} → {Z : F K} → (X ⟶[f₁] Y) → (Y ⟶[f₂] Z) → X ⟶[CategoryTheory.CategoryStruct.comp f₁ f₂] Z
Composition of morphisms overlying composition of morphisms of
C.
Instances
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.«term𝟙ₗ» = Lean.ParserDescr.node `CategoryTheory.term𝟙ₗ 1024 (Lean.ParserDescr.symbol " 𝟙ₗ ")
Instances For
Equations
- CategoryTheory.«term_≫ₗ_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_≫ₗ_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ₗ ") (Lean.ParserDescr.cat `term 80))
Instances For
class
CategoryTheory.Display
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(F : C → Type u_2)
extends
CategoryTheory.DisplayStruct
:
Type (max (max (max u_1 u_2) u_3) (u_4 + 1))
- id_over : {I : C} → (X : F I) → X ⟶[CategoryTheory.CategoryStruct.id I] X
- assoc_cast : ∀ {I J K L : C} {f₁ : I ⟶ J} {f₂ : J ⟶ K} {f₃ : K ⟶ L} {X : F I} {Y : F J} {Z : F K} {W : F L} (g₁ : X ⟶[f₁] Y) (g₂ : Y ⟶[f₂] Z) (g₃ : Z ⟶[f₃] W), CategoryTheory.DisplayStruct.comp_over (CategoryTheory.DisplayStruct.comp_over g₁ g₂) g₃ = ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g₁ (CategoryTheory.DisplayStruct.comp_over g₂ g₃)
Instances
@[simp]
theorem
CategoryTheory.Display.id_comp_cast
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{F : C → Type u_2}
[self : CategoryTheory.Display F]
{I : C}
{J : C}
{f : I ⟶ J}
{X : F I}
{Y : F J}
(g : X ⟶[f] Y)
:
CategoryTheory.DisplayStruct.comp_over ( 𝟙ₗ X) g = ⋯ ▸ g
@[simp]
theorem
CategoryTheory.Display.comp_id_cast
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{F : C → Type u_2}
[self : CategoryTheory.Display F]
{I : C}
{J : C}
{f : I ⟶ J}
{X : F I}
{Y : F J}
(g : X ⟶[f] Y)
:
CategoryTheory.DisplayStruct.comp_over g ( 𝟙ₗ Y) = ⋯ ▸ g
@[simp]
theorem
CategoryTheory.Display.assoc_cast
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{F : C → Type u_2}
[self : CategoryTheory.Display F]
{I : C}
{J : C}
{K : C}
{L : C}
{f₁ : I ⟶ J}
{f₂ : J ⟶ K}
{f₃ : K ⟶ L}
{X : F I}
{Y : F J}
{Z : F K}
{W : F L}
(g₁ : X ⟶[f₁] Y)
(g₂ : Y ⟶[f₂] Z)
(g₃ : Z ⟶[f₃] W)
:
structure
CategoryTheory.BasedLift
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
(f : I ⟶ J)
(X : P ⁻¹ I)
(Y : P ⁻¹ J)
:
Type u_5
The type of lifts of a given morphism in the base with fixed source and target in the Fibres of the domain and codomain respectively.
- hom : ↑X ⟶ ↑Y
- over_eq : CategoryTheory.CategoryStruct.comp (P.map self.hom) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f
Instances For
theorem
CategoryTheory.BasedLift.over_eq
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
{f : I ⟶ J}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
(self : CategoryTheory.BasedLift f X Y)
:
CategoryTheory.CategoryStruct.comp (P.map self.hom) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f
structure
CategoryTheory.EBasedLift
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
(f : I ⟶ J)
(X : P ⁻¹ᵉ I)
(Y : P ⁻¹ᵉ J)
:
Type u_5
The structure of based-lifts up to an isomorphism of the domain objects in the base.
X --------------------> Y
_ -
| | |
| | |
v v v
P.obj X ---------> I ---------> J
≅ f
- hom : X.obj ⟶ Y.obj
- iso_over_eq : CategoryTheory.CategoryStruct.comp (P.map self.hom) Y.iso.hom = CategoryTheory.CategoryStruct.comp X.iso.hom f
Instances For
theorem
CategoryTheory.EBasedLift.iso_over_eq
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
{f : I ⟶ J}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
(self : CategoryTheory.EBasedLift f X Y)
:
CategoryTheory.CategoryStruct.comp (P.map self.hom) Y.iso.hom = CategoryTheory.CategoryStruct.comp X.iso.hom f
theorem
CategoryTheory.EBasedLift.iso_over_eq_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
{f : I ⟶ J}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
(self : CategoryTheory.EBasedLift f X Y)
{Z : C}
(h : J ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (P.map self.hom) (CategoryTheory.CategoryStruct.comp Y.iso.hom h) = CategoryTheory.CategoryStruct.comp X.iso.hom (CategoryTheory.CategoryStruct.comp f h)
@[simp]
theorem
CategoryTheory.BasedLift.over_base
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{E : Type u_4}
[CategoryTheory.Category.{u_6, u_4} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
{f : I ⟶ J}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
(g : CategoryTheory.BasedLift f X Y)
:
@[simp]
theorem
CategoryTheory.BasedLift.id_hom
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{E : Type u_4}
[CategoryTheory.Category.{u_6, u_4} E]
{P : CategoryTheory.Functor E C}
{I : C}
(X : P ⁻¹ I)
:
def
CategoryTheory.BasedLift.id
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{E : Type u_4}
[CategoryTheory.Category.{u_6, u_4} E]
{P : CategoryTheory.Functor E C}
{I : C}
(X : P ⁻¹ I)
:
The identity based-lift.
Equations
- CategoryTheory.BasedLift.id X = { hom := CategoryTheory.CategoryStruct.id ↑X, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.BasedLift.comp_hom
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{E : Type u_4}
[CategoryTheory.Category.{u_6, u_4} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
{K : C}
{f₁ : I ⟶ J}
{f₂ : J ⟶ K}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
{Z : P ⁻¹ K}
(g₁ : CategoryTheory.BasedLift f₁ X Y)
(g₂ : CategoryTheory.BasedLift f₂ Y Z)
:
(g₁.comp g₂).hom = CategoryTheory.CategoryStruct.comp g₁.hom g₂.hom
def
CategoryTheory.BasedLift.comp
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{E : Type u_4}
[CategoryTheory.Category.{u_6, u_4} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
{K : C}
{f₁ : I ⟶ J}
{f₂ : J ⟶ K}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
{Z : P ⁻¹ K}
(g₁ : CategoryTheory.BasedLift f₁ X Y)
(g₂ : CategoryTheory.BasedLift f₂ Y Z)
:
The composition of based-lifts
Equations
- g₁.comp g₂ = { hom := CategoryTheory.CategoryStruct.comp g₁.hom g₂.hom, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.BasedLift.cast_hom
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{E : Type u_4}
[CategoryTheory.Category.{u_6, u_4} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
{f : I ⟶ J}
{f' : I ⟶ J}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
(w : f = f')
(g : CategoryTheory.BasedLift f X Y)
:
(CategoryTheory.BasedLift.cast w g).hom = g.hom
def
CategoryTheory.BasedLift.cast
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{E : Type u_4}
[CategoryTheory.Category.{u_6, u_4} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
{f : I ⟶ J}
{f' : I ⟶ J}
{X : P ⁻¹ I}
{Y : P ⁻¹ J}
(w : f = f')
(g : CategoryTheory.BasedLift f X Y)
:
CategoryTheory.BasedLift f' X Y
Equations
- CategoryTheory.BasedLift.cast w g = { hom := g.hom, over_eq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.EBasedLift.iso_over_eq'
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
{f : I ⟶ J}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
(g : CategoryTheory.EBasedLift f X Y)
:
P.map g.hom = CategoryTheory.CategoryStruct.comp X.iso.hom (CategoryTheory.CategoryStruct.comp f Y.iso.inv)
def
CategoryTheory.EBasedLift.id
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
{P : CategoryTheory.Functor E C}
{I : C}
(X : P ⁻¹ᵉ I)
:
Equations
- CategoryTheory.EBasedLift.id X = { hom := CategoryTheory.CategoryStruct.id X.obj, iso_over_eq := ⋯ }
Instances For
def
CategoryTheory.EBasedLift.comp
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
{P : CategoryTheory.Functor E C}
{I : C}
{J : C}
{K : C}
{f₁ : I ⟶ J}
{f₂ : J ⟶ K}
{X : P ⁻¹ᵉ I}
{Y : P ⁻¹ᵉ J}
{Z : P ⁻¹ᵉ K}
(g₁ : CategoryTheory.EBasedLift f₁ X Y)
(g₂ : CategoryTheory.EBasedLift f₂ Y Z)
:
Equations
- g₁.comp g₂ = { hom := CategoryTheory.CategoryStruct.comp g₁.hom g₂.hom, iso_over_eq := ⋯ }