The category Grpd of groupoids

Need at least the following, some of which is already in MathLib:

• the category of small groupoids and their homomorphisms
• (discrete and split) fibrations of groupoids
• pullbacks of (discrete and split) fibrations exist in Grpd and are again (such) fibrations
• set- and groupoid-valued presheaves on groupoids
• the Grothendieck construction relating the previous two
• the equivalence between (split) fibrations and presheaves of groupoids
• Σ and Π-types for (split) fibrations
• path groupoids
• the universe of (small) discrete groupoids (aka sets)
• polynomial functors of groupoids
• maybe some W-types
• eventually we will want some groupoid quotients as well

@[simp]

theorem CategoryTheory.toCat_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Functor C CategoryTheory.Grpd) : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.toCat G).map f = CategoryTheory.Grpd.forgetToCat.map (G.map f)

@[simp]

theorem CategoryTheory.toCat_obj_str {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Functor C CategoryTheory.Grpd) (X : C) : ((CategoryTheory.toCat G).obj X).str = CategoryTheory.Groupoid.toCategory

@[simp]

theorem CategoryTheory.toCat_obj_α {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Functor C CategoryTheory.Grpd) (X : C) : ↑((CategoryTheory.toCat G).obj X) = ↑(G.obj X)

def CategoryTheory.toCat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Functor C CategoryTheory.Grpd) : CategoryTheory.Functor C CategoryTheory.Cat

Equations

• CategoryTheory.toCat G = G.comp CategoryTheory.Grpd.forgetToCat

def CategoryTheory.Grothendieck.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Functor C CategoryTheory.Cat} {X : CategoryTheory.Grothendieck G} {Y : CategoryTheory.Grothendieck G} (s : X.base ≅ Y.base) (t : (G.map s.hom).obj X.fiber ≅ Y.fiber) : X ≅ Y

A morphism in the Grothendieck construction is an isomorphism if the morphism in the base is an isomorphism and the fiber morphism is an isomorphism.

Equations

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

def CategoryTheory.GroupoidalGrothendieck {C : Type u₁} [CategoryTheory.Groupoid C] (F : CategoryTheory.Functor C CategoryTheory.Grpd) : Type (max u₁ u₂)

In Mathlib.CategoryTheory.Grothendieck we find the Grothendieck construction for the functors F : C ⥤ Cat. Given a functor F : G ⥤ Grpd, we show that the Grothendieck construction of the composite F ⋙ Grpd.forgetToCat, where forgetToCat : Grpd ⥤ Cat is the embedding of groupoids into categories, is a groupoid.

Equations

• CategoryTheory.GroupoidalGrothendieck F = CategoryTheory.Grothendieck (CategoryTheory.toCat F)

instance CategoryTheory.GroupoidalGrothendieck.instCategory {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} : CategoryTheory.Category.{max v₁ v₂, max u₂ u₁} (CategoryTheory.GroupoidalGrothendieck F)

Equations

• CategoryTheory.GroupoidalGrothendieck.instCategory = inferInstanceAs (CategoryTheory.Category.{max v₂ v₁, max u₂ u₁} (CategoryTheory.Grothendieck (CategoryTheory.toCat F)))

instance CategoryTheory.GroupoidalGrothendieck.instGroupoidαCategoryObjCatToCat {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} (X : C) : CategoryTheory.Groupoid ↑((CategoryTheory.toCat F).obj X)

Equations

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

def CategoryTheory.GroupoidalGrothendieck.isoMk {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} {X : CategoryTheory.GroupoidalGrothendieck F} {Y : CategoryTheory.GroupoidalGrothendieck F} (f : X ⟶ Y) : X ≅ Y

Equations

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

def CategoryTheory.GroupoidalGrothendieck.inv {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} {X : CategoryTheory.GroupoidalGrothendieck F} {Y : CategoryTheory.GroupoidalGrothendieck F} (f : X ⟶ Y) : Y ⟶ X

Equations

• CategoryTheory.GroupoidalGrothendieck.inv f = (CategoryTheory.GroupoidalGrothendieck.isoMk f).inv

instance CategoryTheory.GroupoidalGrothendieck.groupoid {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} : CategoryTheory.Groupoid (CategoryTheory.GroupoidalGrothendieck F)

Equations

• CategoryTheory.GroupoidalGrothendieck.groupoid = CategoryTheory.Groupoid.mk (fun {X Y : CategoryTheory.GroupoidalGrothendieck F} (f : X ⟶ Y) => CategoryTheory.GroupoidalGrothendieck.inv f) ⋯ ⋯

def CategoryTheory.GroupoidalGrothendieck.forget {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} : CategoryTheory.Functor (CategoryTheory.GroupoidalGrothendieck F) C

Equations

• CategoryTheory.GroupoidalGrothendieck.forget = CategoryTheory.Grothendieck.forget (F.comp CategoryTheory.Grpd.forgetToCat)

def CategoryTheory.GroupoidalGrothendieck.ToGrpd {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} : CategoryTheory.Functor (CategoryTheory.GroupoidalGrothendieck F) CategoryTheory.Grpd

Equations

• CategoryTheory.GroupoidalGrothendieck.ToGrpd = CategoryTheory.GroupoidalGrothendieck.forget.comp F

def CategoryTheory.GroupoidalGrothendieck.functorial {C : CategoryTheory.Grpd} {D : CategoryTheory.Grpd} (F : C ⟶ D) (G : CategoryTheory.Functor (↑D) CategoryTheory.Grpd) : CategoryTheory.Functor (CategoryTheory.Grothendieck (CategoryTheory.toCat (CategoryTheory.Functor.comp F G))) (CategoryTheory.Grothendieck (CategoryTheory.toCat G))

Equations

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

class CategoryTheory.PointedCategory (C : Type z) extends CategoryTheory.Category : Type (max (w + 1) z)

The class of pointed pointed categorys.

• Hom : C → C → Type w
• id : (X : C) → X ⟶ X
• comp : {X Y Z : C} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
• id_comp : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
• comp_id : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
• assoc : ∀ {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
• pt : C

def CategoryTheory.PointedCategory.of (C : Type u_1) (pt : C) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.PointedCategory C

A constructor that makes a pointed categorys from a category and a point.

Equations

• CategoryTheory.PointedCategory.of C pt = CategoryTheory.PointedCategory.mk pt

structure CategoryTheory.PointedFunctor (C : Type u_1) (D : Type u_2) [cp : CategoryTheory.PointedCategory C] [dp : CategoryTheory.PointedCategory D] extends CategoryTheory.Functor : Type (max (max (max u_1 u_2) u_3) u_4)

The structure of a functor from C to D along with a morphism from the image of the point of C to the point of D

• obj : C → D
• map : {X Y : C} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• map_id : ∀ (X : C), self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
• map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
• point : self.obj CategoryTheory.PointedCategory.pt ⟶ CategoryTheory.PointedCategory.pt

@[simp]

theorem CategoryTheory.PointedFunctor.id_map (C : Type u_1) [CategoryTheory.PointedCategory C] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.PointedFunctor.id C).map f = f

@[simp]

theorem CategoryTheory.PointedFunctor.id_obj (C : Type u_1) [CategoryTheory.PointedCategory C] (X : C) : (CategoryTheory.PointedFunctor.id C).obj X = X

@[simp]

theorem CategoryTheory.PointedFunctor.id_point (C : Type u_1) [CategoryTheory.PointedCategory C] : (CategoryTheory.PointedFunctor.id C).point = CategoryTheory.CategoryStruct.id CategoryTheory.PointedCategory.pt

def CategoryTheory.PointedFunctor.id (C : Type u_1) [CategoryTheory.PointedCategory C] : CategoryTheory.PointedFunctor C C

The identity PointedFunctor whose underlying functor is the identity functor

Equations

• CategoryTheory.PointedFunctor.id C = { toFunctor := CategoryTheory.Functor.id C, point := CategoryTheory.CategoryStruct.id CategoryTheory.PointedCategory.pt }

@[simp]

theorem CategoryTheory.PointedFunctor.comp_map {C : Type u_1} [CategoryTheory.PointedCategory C] {D : Type u_2} [CategoryTheory.PointedCategory D] {E : Type u_3} [CategoryTheory.PointedCategory E] (F : CategoryTheory.PointedFunctor C D) (G : CategoryTheory.PointedFunctor D E) : ∀ {X Y : C} (f : X ⟶ Y), (F.comp G).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.PointedFunctor.comp_point {C : Type u_1} [CategoryTheory.PointedCategory C] {D : Type u_2} [CategoryTheory.PointedCategory D] {E : Type u_3} [CategoryTheory.PointedCategory E] (F : CategoryTheory.PointedFunctor C D) (G : CategoryTheory.PointedFunctor D E) : (F.comp G).point = CategoryTheory.CategoryStruct.comp (G.map F.point) G.point

@[simp]

theorem CategoryTheory.PointedFunctor.comp_obj {C : Type u_1} [CategoryTheory.PointedCategory C] {D : Type u_2} [CategoryTheory.PointedCategory D] {E : Type u_3} [CategoryTheory.PointedCategory E] (F : CategoryTheory.PointedFunctor C D) (G : CategoryTheory.PointedFunctor D E) (X : C) : (F.comp G).obj X = G.obj (F.obj X)

def CategoryTheory.PointedFunctor.comp {C : Type u_1} [CategoryTheory.PointedCategory C] {D : Type u_2} [CategoryTheory.PointedCategory D] {E : Type u_3} [CategoryTheory.PointedCategory E] (F : CategoryTheory.PointedFunctor C D) (G : CategoryTheory.PointedFunctor D E) : CategoryTheory.PointedFunctor C E

Composition of PointedFunctor that composes there underling functors and shows that the point is preserved

Equations

• F.comp G = { toFunctor := F.comp G.toFunctor, point := CategoryTheory.CategoryStruct.comp (G.map F.point) G.point }

theorem CategoryTheory.PointedFunctor.congr_func {C : Type u_1} [CategoryTheory.PointedCategory C] {D : Type u_2} [CategoryTheory.PointedCategory D] {F : CategoryTheory.PointedFunctor C D} {G : CategoryTheory.PointedFunctor C D} (eq : F = G) : F.toFunctor = G.toFunctor

theorem CategoryTheory.PointedFunctor.congr_point {C : Type u_1} [pc : CategoryTheory.PointedCategory C] {D : Type u_2} [CategoryTheory.PointedCategory D] {F : CategoryTheory.PointedFunctor C D} {G : CategoryTheory.PointedFunctor C D} (eq : F = G) : F.point = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) G.point

theorem CategoryTheory.PointedFunctor.ext {C : Type u_1} [pc : CategoryTheory.PointedCategory C] {D : Type u_2} [CategoryTheory.PointedCategory D] (F : CategoryTheory.PointedFunctor C D) (G : CategoryTheory.PointedFunctor C D) (h_func : F.toFunctor = G.toFunctor) (h_point : F.point = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) G.point) : F = G

def CategoryTheory.PCat : Type (max (z + 1) (w + 1) z)

The category of pointed categorys and pointed functors

Equations

• CategoryTheory.PCat = CategoryTheory.Bundled CategoryTheory.PointedCategory

instance CategoryTheory.PCat.instCoeSortType : CoeSort CategoryTheory.PCat (Type u)

Equations

• CategoryTheory.PCat.instCoeSortType = { coe := CategoryTheory.Bundled.α }

instance CategoryTheory.PCat.str (C : CategoryTheory.PCat) : CategoryTheory.PointedCategory ↑C

Equations

• C.str = C.str

def CategoryTheory.PCat.of (C : Type u) [CategoryTheory.PointedCategory C] : CategoryTheory.PCat

Construct a bundled PCat from the underlying type and the typeclass.

Equations

• CategoryTheory.PCat.of C = CategoryTheory.Bundled.of C

instance CategoryTheory.PCat.category : CategoryTheory.LargeCategory CategoryTheory.PCat

Equations

• CategoryTheory.PCat.category = CategoryTheory.Category.mk @CategoryTheory.PCat.category.proof_1 @CategoryTheory.PCat.category.proof_2 @CategoryTheory.PCat.category.proof_3

def CategoryTheory.PCat.forgetPoint : CategoryTheory.Functor CategoryTheory.PCat CategoryTheory.Cat

The functor that takes PCat to Cat by forgetting the points

Equations

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

class CategoryTheory.PointedGroupoid (C : Type z) extends CategoryTheory.Groupoid : Type (max (w + 1) z)

The class of pointed pointed groupoids.

• Hom : C → C → Type w
• id : (X : C) → X ⟶ X
• comp : {X Y Z : C} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
• id_comp : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
• comp_id : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
• assoc : ∀ {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
• inv : {X Y : C} → (X ⟶ Y) → (Y ⟶ X)
• inv_comp : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f) f = CategoryTheory.CategoryStruct.id Y
• comp_inv : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Groupoid.inv f) = CategoryTheory.CategoryStruct.id X
• pt : C

def CategoryTheory.PointedGroupoid.of (C : Type u_1) (pt : C) [CategoryTheory.Groupoid C] : CategoryTheory.PointedGroupoid C

A constructor that makes a pointed groupoid from a groupoid and a point.

Equations

• CategoryTheory.PointedGroupoid.of C pt = CategoryTheory.PointedGroupoid.mk pt

def CategoryTheory.PGrpd : Type (max (z + 1) (w + 1) z)

The category of pointed groupoids and pointed functors

Equations

• CategoryTheory.PGrpd = CategoryTheory.Bundled CategoryTheory.PointedGroupoid

instance CategoryTheory.PGrpd.instCoeSortType : CoeSort CategoryTheory.PGrpd (Type u)

Equations

• CategoryTheory.PGrpd.instCoeSortType = { coe := CategoryTheory.Bundled.α }

instance CategoryTheory.PGrpd.str (C : CategoryTheory.PGrpd) : CategoryTheory.PointedGroupoid ↑C

Equations

• C.str = C.str

def CategoryTheory.PGrpd.of (C : Type u) [CategoryTheory.PointedGroupoid C] : CategoryTheory.PGrpd

Construct a bundled PGrpd from the underlying type and the typeclass.

Equations

• CategoryTheory.PGrpd.of C = CategoryTheory.Bundled.of C

def CategoryTheory.PGrpd.fromGrpd (G : CategoryTheory.Grpd) (g : ↑G) : CategoryTheory.PGrpd

Construct a bundled PGrpd from a Grpd and a point

Equations

• CategoryTheory.PGrpd.fromGrpd G g = let_fun pg := CategoryTheory.PointedGroupoid.of (↑G) g; CategoryTheory.PGrpd.of ↑G

instance CategoryTheory.PGrpd.category : CategoryTheory.LargeCategory CategoryTheory.PGrpd

Equations

• CategoryTheory.PGrpd.category = CategoryTheory.Category.mk @CategoryTheory.PGrpd.category.proof_1 @CategoryTheory.PGrpd.category.proof_2 @CategoryTheory.PGrpd.category.proof_3

def CategoryTheory.PGrpd.forgetPoint : CategoryTheory.Functor CategoryTheory.PGrpd CategoryTheory.Grpd

The functor that takes PGrpd to Grpd by forgetting the points

Equations

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

def CategoryTheory.PGrpd.forgetToCat : CategoryTheory.Functor CategoryTheory.PGrpd CategoryTheory.PCat

This takes PGrpd to PCat

Equations

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

theorem CategoryTheory.PointedFunctor.eqToHom_toFunctor {P1 : CategoryTheory.PCat} {P2 : CategoryTheory.PCat} (eq : P1 = P2) : (CategoryTheory.eqToHom eq).toFunctor = CategoryTheory.eqToHom ⋯

theorem PointedCategory.ext {P1 P2 : PCat.{u,u}} (eq_cat : P1.α = P2.α): P1 = P2 := by sorry

theorem CategoryTheory.PointedFunctor.eqToHom_point_help {P1 : CategoryTheory.PCat} {P2 : CategoryTheory.PCat} (eq : P1 = P2) : (CategoryTheory.eqToHom eq).obj CategoryTheory.PointedCategory.pt = CategoryTheory.PointedCategory.pt

This is the proof of equality used in the eqToHom in PointedFunctor.eqToHom_point

theorem CategoryTheory.PointedFunctor.eqToHom_point {P1 : CategoryTheory.PCat} {P2 : CategoryTheory.PCat} (eq : P1 = P2) : (CategoryTheory.eqToHom eq).point = CategoryTheory.eqToHom ⋯

This shows that the point of an eqToHom in PCat is an eqToHom

theorem CategoryTheory.Cat.eqToHom_obj (C1 : CategoryTheory.Cat) (C2 : CategoryTheory.Cat) (x : ↑C1) (eq : C1 = C2) : (CategoryTheory.eqToHom eq).obj x = cast ⋯ x

This is the turns the object part of eqToHom functors into a cast

theorem CategoryTheory.Cat.eqToHom_hom_help {C1 : CategoryTheory.Cat} {C2 : CategoryTheory.Cat} (x : ↑C1) (y : ↑C1) (eq : C1 = C2) : (x ⟶ y) = ((CategoryTheory.eqToHom eq).obj x ⟶ (CategoryTheory.eqToHom eq).obj y)

This is the proof of equality used in the eqToHom in Cat.eqToHom_hom

theorem CategoryTheory.Cat.eqToHom_hom {C1 : CategoryTheory.Cat} {C2 : CategoryTheory.Cat} {x : ↑C1} {y : ↑C1} (f : x ⟶ y) (eq : C1 = C2) : (CategoryTheory.eqToHom eq).map f = cast ⋯ f

This is the turns the hom part of eqToHom functors into a cast

theorem CategoryTheory.PCat.eqToHom_hom_help {C1 : CategoryTheory.PCat} {C2 : CategoryTheory.PCat} (x : ↑C1) (y : ↑C1) (eq : C1 = C2) : (x ⟶ y) = ((CategoryTheory.eqToHom eq).obj x ⟶ (CategoryTheory.eqToHom eq).obj y)

This is the proof of equality used in the eqToHom in PCat.eqToHom_hom

theorem CategoryTheory.PCat.eqToHom_hom {C1 : CategoryTheory.PCat} {C2 : CategoryTheory.PCat} {x : ↑C1} {y : ↑C1} (f : x ⟶ y) (eq : C1 = C2) : (CategoryTheory.eqToHom eq).map f = cast ⋯ f

This is the turns the hom part of eqToHom pointed functors into a cast

theorem CategoryTheory.Grothendieck.ext' {Γ : CategoryTheory.Cat} {A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat} (g1 : CategoryTheory.Grothendieck A) (g2 : CategoryTheory.Grothendieck A) (eq_base : g1.base = g2.base) (eq_fiber : g1.fiber = (A.map (CategoryTheory.eqToHom ⋯)).obj g2.fiber) : g1 = g2

This shows that two objects are equal in Grothendieck A if they have equal bases and fibers that are equal after being cast

theorem CategoryTheory.Grothendieck.eqToHom_base {Γ : CategoryTheory.Cat} {A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat} (g1 : CategoryTheory.Grothendieck A) (g2 : CategoryTheory.Grothendieck A) (eq : g1 = g2) : (CategoryTheory.eqToHom eq).base = CategoryTheory.eqToHom ⋯

This proves that base of an eqToHom morphism in the category Grothendieck A is an eqToHom morphism

theorem CategoryTheory.Grothendieck.eqToHom_fiber_help {Γ : CategoryTheory.Cat} {A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat} {g1 : CategoryTheory.Grothendieck A} {g2 : CategoryTheory.Grothendieck A} (eq : g1 = g2) : (A.map (CategoryTheory.eqToHom eq).base).obj g1.fiber = g2.fiber

This is the proof of equality used in the eqToHom in Grothendieck.eqToHom_fiber

theorem CategoryTheory.Grothendieck.eqToHom_fiber {Γ : CategoryTheory.Cat} {A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat} {g1 : CategoryTheory.Grothendieck A} {g2 : CategoryTheory.Grothendieck A} (eq : g1 = g2) : (CategoryTheory.eqToHom eq).fiber = CategoryTheory.eqToHom ⋯

This proves that fiber of an eqToHom morphism in the category Grothendieck A is an eqToHom morphism

theorem CategoryTheory.RightSidedEqToHom {C : Type v} [CategoryTheory.Category.{u_1, v} C] {x : C} {y : C} {z : C} (eq : y = z) {f : x ⟶ y} {g : x ⟶ z} (heq : HEq f g) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom eq) = g

This eliminates an eqToHom on the right side of an equality

theorem CategoryTheory.CastEqToHomSolve {C : Type v} [CategoryTheory.Category.{u_1, v} C] {x : C} {x1 : C} {x2 : C} {y : C} {y1 : C} {y2 : C} (eqx1 : x = x1) (eqx2 : x = x2) (eqy1 : y1 = y) (eqy2 : y2 = y) {f : x1 ⟶ y1} {g : x2 ⟶ y2} (heq : HEq f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom eqx1) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom eqy1)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom eqx2) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom eqy2))

This theorem is used to eliminate eqToHom form both sides of an equation

def CategoryTheory.CastFunc {C : CategoryTheory.Cat} {F1 : CategoryTheory.Functor (↑C) CategoryTheory.Cat} {F2 : CategoryTheory.Functor (↑C) CategoryTheory.Cat} (Comm : F1 = F2) (x : ↑C) : ↑(F1.obj x) ≌ ↑(F2.obj x)

Equations

• CategoryTheory.CastFunc Comm x = CategoryTheory.Cat.equivOfIso (CategoryTheory.eqToIso ⋯)

theorem CategoryTheory.CastFuncIsEqToHom {C : CategoryTheory.Cat} {F1 : CategoryTheory.Functor (↑C) CategoryTheory.Cat} {F2 : CategoryTheory.Functor (↑C) CategoryTheory.Cat} (Comm : F1 = F2) (x : ↑C) : (CategoryTheory.CastFunc Comm x).functor = CategoryTheory.eqToHom ⋯

def CategoryTheory.Up_uni (Δ : Type u) [CategoryTheory.Category.{u, u} Δ] : CategoryTheory.Functor Δ (ULift.{u + 1, u} Δ)

Equations

• CategoryTheory.Up_uni Δ = { obj := fun (x : Δ) => { down := x }, map := fun {X Y : Δ} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }

def CategoryTheory.Down_uni (Δ : Type u) [CategoryTheory.Category.{u, u} Δ] : CategoryTheory.Functor (ULift.{u + 1, u} Δ) Δ

Equations

• CategoryTheory.Down_uni Δ = { obj := fun (x : ULift.{u + 1, u} Δ) => x.down, map := fun {X Y : ULift.{u + 1, u} Δ} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }

theorem CategoryTheory.Up_Down {C : Type (u + 1)} [CategoryTheory.Category.{u, u + 1} C] {Δ : Type u} [CategoryTheory.Category.{u, u} Δ] (F : CategoryTheory.Functor C Δ) (G : CategoryTheory.Functor C (ULift.{u + 1, u} Δ)) : F.comp (CategoryTheory.Up_uni Δ) = G ↔ F = G.comp (CategoryTheory.Down_uni Δ)

def CategoryTheory.CatVar' (Γ : CategoryTheory.Cat) (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat) : CategoryTheory.Functor (CategoryTheory.Grothendieck A) CategoryTheory.PCat

Equations

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

theorem CategoryTheory.Comm {Γ : CategoryTheory.Cat} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat) : ((CategoryTheory.Down_uni (CategoryTheory.Grothendieck A)).comp (CategoryTheory.CatVar' Γ A)).comp CategoryTheory.PCat.forgetPoint = ((CategoryTheory.Down_uni (CategoryTheory.Grothendieck A)).comp ((CategoryTheory.Grothendieck.forget A).comp (CategoryTheory.Up_uni ↑Γ))).comp ((CategoryTheory.Down_uni ↑Γ).comp A)

def CategoryTheory.ForgetPointFunctor (P : CategoryTheory.PCat) : CategoryTheory.Functor ↑P ↑(CategoryTheory.PCat.forgetPoint.obj P)

Equations

• CategoryTheory.ForgetPointFunctor P = id (CategoryTheory.Functor.id ↑P)

def CategoryTheory.Grothendieck.UnivesalMap {Γ : CategoryTheory.Cat} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat) (C : CategoryTheory.Cat) (F1 : CategoryTheory.Functor (↑C) CategoryTheory.PCat) (F2 : CategoryTheory.Functor ↑C ↑Γ) (Comm : F1.comp CategoryTheory.PCat.forgetPoint = F2.comp A) : CategoryTheory.Functor (↑C) (CategoryTheory.Grothendieck A)

Equations

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

theorem CategoryTheory.Grothendieck.UnivesalMap_CatVar'_Comm {Γ : CategoryTheory.Cat} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat) (C : CategoryTheory.Cat) (F1 : CategoryTheory.Functor (↑C) CategoryTheory.PCat) (F2 : CategoryTheory.Functor ↑C ↑Γ) (Comm : F1.comp CategoryTheory.PCat.forgetPoint = F2.comp A) : (CategoryTheory.Grothendieck.UnivesalMap A C F1 F2 Comm).comp (CategoryTheory.CatVar' Γ A) = F1

theorem CategoryTheory.Grothendieck.UnivesalMap_Uniq {Γ : CategoryTheory.Cat} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat) (C : CategoryTheory.Cat) (F1 : CategoryTheory.Functor (↑C) CategoryTheory.PCat) (F2 : CategoryTheory.Functor ↑C ↑Γ) (Comm : F1.comp CategoryTheory.PCat.forgetPoint = F2.comp A) (F : CategoryTheory.Functor (↑C) (CategoryTheory.Grothendieck A)) (F1comm : F.comp (CategoryTheory.CatVar' Γ A) = F1) (F2comm : F.comp (CategoryTheory.Grothendieck.forget A) = F2) : F = CategoryTheory.Grothendieck.UnivesalMap A C F1 F2 Comm

@[reducible, inline]

abbrev CategoryTheory.GrothendieckCones {Γ : CategoryTheory.Cat} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat) : Type (u + 2)

Equations

• CategoryTheory.GrothendieckCones A = CategoryTheory.Limits.PullbackCone CategoryTheory.PCat.forgetPoint ((CategoryTheory.Down_uni ↑Γ).comp A)

@[reducible, inline]

abbrev CategoryTheory.GrothendieckLim {Γ : CategoryTheory.Cat} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat) : CategoryTheory.GrothendieckCones A

Equations

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

def CategoryTheory.GrothendieckLimisLim {Γ : CategoryTheory.Cat} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat) : CategoryTheory.Limits.IsLimit (CategoryTheory.GrothendieckLim A)

Equations

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

theorem CategoryTheory.GrothendieckLimisPullBack {Γ : CategoryTheory.Cat} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat) : CategoryTheory.IsPullback ((CategoryTheory.Down_uni (CategoryTheory.Grothendieck A)).comp (CategoryTheory.CatVar' Γ A)) ((CategoryTheory.Down_uni (CategoryTheory.Grothendieck A)).comp ((CategoryTheory.Grothendieck.forget A).comp (CategoryTheory.Up_uni ↑Γ))) CategoryTheory.PCat.forgetPoint ((CategoryTheory.Down_uni ↑Γ).comp A)

theorem CategoryTheory.PComm : CategoryTheory.PGrpd.forgetToCat.comp CategoryTheory.PCat.forgetPoint = CategoryTheory.PGrpd.forgetPoint.comp CategoryTheory.Grpd.forgetToCat

@[reducible, inline]

abbrev CategoryTheory.PointedCones : Type (u + 2)

Equations

• CategoryTheory.PointedCones = CategoryTheory.Limits.PullbackCone CategoryTheory.PCat.forgetPoint CategoryTheory.Grpd.forgetToCat

@[reducible, inline]

abbrev CategoryTheory.PointedLim : CategoryTheory.PointedCones

Equations

• CategoryTheory.PointedLim = CategoryTheory.Limits.PullbackCone.mk CategoryTheory.PGrpd.forgetToCat CategoryTheory.PGrpd.forgetPoint CategoryTheory.PComm

def CategoryTheory.Pointed.UnivesalMap (C : CategoryTheory.Cat) (F1 : CategoryTheory.Functor (↑C) CategoryTheory.PCat) (F2 : CategoryTheory.Functor (↑C) CategoryTheory.Grpd) (Comm : F1.comp CategoryTheory.PCat.forgetPoint = F2.comp CategoryTheory.Grpd.forgetToCat) : CategoryTheory.Functor (↑C) CategoryTheory.PGrpd

This is the construction of the universal map for the limit

Equations

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

def CategoryTheory.Pointed.UnivesalMap_Uniq (s : CategoryTheory.PointedCones) : s ⟶ CategoryTheory.PointedLim

Equations

• CategoryTheory.Pointed.UnivesalMap_Uniq s = { hom := sorryAx (s.pt ⟶ CategoryTheory.PointedLim.pt), w := ⋯ }

def CategoryTheory.PointedLimisLim : CategoryTheory.Limits.IsLimit CategoryTheory.PointedLim

Equations

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

def CategoryTheory.Ty_functor : CategoryTheory.Functor CategoryTheory.Grpdᵒᵖ (Type (u + 1))

Equations

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

def CategoryTheory.Tm_functor : CategoryTheory.Functor CategoryTheory.Grpdᵒᵖ (Type (u + 1))

Equations

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

def CategoryTheory.tp_NatTrans : CategoryTheory.NatTrans CategoryTheory.Tm_functor CategoryTheory.Ty_functor

Equations

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

def CategoryTheory.var' (Γ : CategoryTheory.Grpd) (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) : CategoryTheory.Functor (CategoryTheory.GroupoidalGrothendieck A) CategoryTheory.PGrpd

Equations

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

def CategoryTheory.sGrpd : Type (u + 1)

Equations

• CategoryTheory.sGrpd = CategoryTheory.ULiftHom CategoryTheory.Grpd

def CategoryTheory.sGrpd.of (C : Type u) [CategoryTheory.Groupoid C] : CategoryTheory.sGrpd

Equations

• CategoryTheory.sGrpd.of C = CategoryTheory.Grpd.of C

def CategoryTheory.SmallGrpd.forget : CategoryTheory.Functor CategoryTheory.sGrpd CategoryTheory.Grpd

Equations

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

instance CategoryTheory.GroupoidNM : CategoryTheory.NaturalModel.NaturalModelBase CategoryTheory.sGrpd

Equations

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

instance CategoryTheory.groupoidULift {α : Type u} [CategoryTheory.Groupoid α] : CategoryTheory.Groupoid (ULift.{u', u} α)

Equations

• CategoryTheory.groupoidULift = CategoryTheory.Groupoid.mk (fun {X Y : ULift.{u', u} α} (f : X ⟶ Y) => CategoryTheory.Groupoid.inv f) ⋯ ⋯

instance CategoryTheory.groupoidULiftHom {α : Type u} [CategoryTheory.Groupoid α] : CategoryTheory.Groupoid (CategoryTheory.ULiftHom α)

Equations

• CategoryTheory.groupoidULiftHom = CategoryTheory.Groupoid.mk (fun {X Y : CategoryTheory.ULiftHom α} (f : X ⟶ Y) => { down := CategoryTheory.Groupoid.inv f.down }) ⋯ ⋯

inductive CategoryTheory.Groupoid2 : Type (u + 2)

• small: CategoryTheory.sGrpd → CategoryTheory.Groupoid2
• large: CategoryTheory.sGrpd → CategoryTheory.Groupoid2

def CategoryTheory.Groupoid2.toLarge : CategoryTheory.Groupoid2 → CategoryTheory.sGrpd

Equations

• x.toLarge = match x with | CategoryTheory.Groupoid2.small A => { α := CategoryTheory.ULiftHom (ULift.{u + 1, u} ↑A), str := inferInstance } | CategoryTheory.Groupoid2.large A => A

def CategoryTheory.Grpd2 : Type (u + 2)

A model of Grpd with an internal universe, with the property that the small universe injects into the large one.

Equations

• CategoryTheory.Grpd2 = CategoryTheory.InducedCategory CategoryTheory.sGrpd CategoryTheory.Groupoid2.toLarge