Here we construct the natural model for groupoids.

TODO: This file needs to eventually be ported to GroupoidRussellNaturalModel but currently we don't have a Russell style sigma type.

def sGrpd : Type (u + 1)

Equations

• sGrpd = CategoryTheory.ULiftHom CategoryTheory.Grpd

instance instsGrpdSmallCategory : CategoryTheory.SmallCategory sGrpd

Equations

• instsGrpdSmallCategory = CategoryTheory.ULiftHom.category

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

Equations

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

def CatLift : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Cat

Equations

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

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

Equations

• sGrpd.forget = CategoryTheory.ULiftHom.down

def sGrpd.remember : CategoryTheory.Functor CategoryTheory.Grpd sGrpd

Equations

• sGrpd.remember = CategoryTheory.ULiftHom.up

def ι : CategoryTheory.Functor CategoryTheory.Grpd CategoryTheory.Cat

Equations

• ι = CategoryTheory.Grpd.forgetToCat.comp CatLift

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

Equations

• PshGrpdOfCat = CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringLeft CategoryTheory.Grpdᵒᵖ CategoryTheory.Catᵒᵖ (Type (?u.11 + 1))).obj ι.op)

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

Equations

• PshsGrpdOfPshGrpd = (CategoryTheory.whiskeringLeft sGrpdᵒᵖ CategoryTheory.Grpdᵒᵖ (Type (?u.15 + 1))).obj sGrpd.forget.op

@[reducible, inline]

abbrev yonedaCat : CategoryTheory.Functor CategoryTheory.Cat (CategoryTheory.Psh sGrpd)

Equations

• yonedaCat = PshGrpdOfCat.comp PshsGrpdOfPshGrpd

def yonedaCatEquiv {Γ : sGrpd} {C : Type (u + 1)} [CategoryTheory.Category.{u, u + 1} C] : (CategoryTheory.yoneda.obj Γ ⟶ yonedaCat.obj (CategoryTheory.Cat.of C)) ≃ CategoryTheory.Functor (↑(sGrpd.forget.obj Γ)) C

Equations

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

theorem yonedaCatEquiv_naturality {Γ Δ : sGrpd} {C : Type (u + 1)} [CategoryTheory.Category.{u, u + 1} C] (A : CategoryTheory.yoneda.obj Γ ⟶ yonedaCat.obj (CategoryTheory.Cat.of C)) (σ : Δ ⟶ Γ) : CategoryTheory.Functor.comp (sGrpd.forget.map σ) (yonedaCatEquiv A) = yonedaCatEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A)

theorem yonedaCatEquiv_comp {Γ : sGrpd} {C D : Type (u + 1)} [CategoryTheory.Category.{u, u + 1} C] [CategoryTheory.Category.{u, u + 1} D] (A : CategoryTheory.yoneda.obj Γ ⟶ yonedaCat.obj (CategoryTheory.Cat.of D)) (U : CategoryTheory.Functor D C) : yonedaCatEquiv (CategoryTheory.CategoryStruct.comp A (yonedaCat.map U)) = (yonedaCatEquiv A).comp U

@[reducible, inline]

abbrev Ty : CategoryTheory.Psh sGrpd

Equations

• Ty = yonedaCat.obj (CategoryTheory.Cat.of CategoryTheory.Grpd)

@[reducible, inline]

abbrev Tm : CategoryTheory.Psh sGrpd

Equations

• Tm = yonedaCat.obj (CategoryTheory.Cat.of CategoryTheory.PGrpd)

@[reducible, inline]

abbrev tp : Tm ⟶ Ty

Equations

• tp = yonedaCat.map CategoryTheory.PGrpd.forgetToGrpd

@[reducible, inline]

abbrev ext {Γ : sGrpd} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : CategoryTheory.Grpd

Equations

• ext A = CategoryTheory.Grpd.of (CategoryTheory.Grothendieck.Groupoidal (yonedaCatEquiv A))

@[reducible, inline]

abbrev downDisp {Γ : sGrpd} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : ext A ⟶ Γ

Equations

• downDisp A = CategoryTheory.Grothendieck.forget (CategoryTheory.Groupoid.compForgetToCat (yonedaCatEquiv A))

@[reducible, inline]

abbrev disp {Γ : sGrpd} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : ext A ⟶ Γ

Equations

• disp A = { down := downDisp A }

@[reducible, inline]

abbrev var {Γ : sGrpd} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : CategoryTheory.yoneda.obj (ext A) ⟶ Tm

Equations

• var A = yonedaCatEquiv.invFun sorry

theorem disp_pullback {Γ : sGrpd} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : CategoryTheory.IsPullback (var A) (CategoryTheory.yoneda.map { down := downDisp A }) tp A

instance GroupoidNM : CategoryTheory.NaturalModel.NaturalModelBase sGrpd

Equations

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

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

Equations

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

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

Equations

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

inductive Groupoid2 : Type (u + 2)

• small : sGrpd → Groupoid2
• large : sGrpd → Groupoid2

def Groupoid2.toLarge : Groupoid2 → sGrpd

Equations

• (Groupoid2.small A).toLarge = { α := CategoryTheory.ULiftHom (ULift.{?u.154 + 1, ?u.154} ↑A), str := inferInstance }
• (Groupoid2.large A).toLarge = A

def 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

• Grpd2 = CategoryTheory.InducedCategory sGrpd Groupoid2.toLarge

instance instGrpd2SmallCategory : CategoryTheory.SmallCategory Grpd2

Equations

• instGrpd2SmallCategory = CategoryTheory.InducedCategory.category Groupoid2.toLarge

def PointToFiber {Γ : CategoryTheory.Grpd} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (x : ↑Γ) : CategoryTheory.Functor (↑(A.obj x)) (CategoryTheory.Grothendieck.Groupoidal A)

Equations

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

def PointToFiberNT {Γ : CategoryTheory.Grpd} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (X Y : ↑Γ) (f : X ⟶ Y) : PointToFiber A X ⟶ CategoryTheory.Functor.comp (A.map f) (PointToFiber A Y)

Equations

• PointToFiberNT A X Y f = { app := fun (x : ↑(A.obj X)) => { base := id f, fiber := id (CategoryTheory.CategoryStruct.id ((A.map f).obj x)) }, naturality := ⋯ }

def uv_tp : UvPoly Tm Ty

Equations

• uv_tp = { p := tp, exp := inferInstance }

def P : CategoryTheory.Functor (CategoryTheory.Psh sGrpd) (CategoryTheory.Psh sGrpd)

Equations

• P = uv_tp.functor

def GroupoidSigma (Γ : CategoryTheory.Grpd) (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal A) CategoryTheory.Grpd) : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd

Equations

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

def GroupoidSigmaMake {Γ : CategoryTheory.Grpd} {A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd} {B : CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal A) CategoryTheory.Grpd} {x : ↑Γ} (Ax : ↑(A.obj x)) (Bx : ↑(B.obj { base := x, fiber := Ax })) : ↑((GroupoidSigma Γ A B).obj x)

Equations

• GroupoidSigmaMake Ax Bx = { base := Ax, fiber := Bx }

def GroupoidSigmaBase (Γ : CategoryTheory.Grpd) (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal A) CategoryTheory.Grpd) : GroupoidSigma Γ A B ⟶ A

Equations

• GroupoidSigmaBase Γ A B = { app := id fun (x : ↑Γ) => id sorry, naturality := ⋯ }

theorem GroupoidSigmaBeckChevalley (Δ Γ : CategoryTheory.Grpd) (σ : CategoryTheory.Functor ↑Δ ↑Γ) (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal A) CategoryTheory.Grpd) : σ.comp (GroupoidSigma Γ A B) = GroupoidSigma Δ (σ.comp A) (CategoryTheory.Grothendieck.Groupoidal.Map Δ Γ σ A B)

instance instHasLimitsPshSGrpd : CategoryTheory.Limits.HasLimits (CategoryTheory.Psh sGrpd)

instance instHasLimitWalkingCospanFunctorOppositeSGrpdTypeCospanPPshUv_tp {Γ : sGrpd} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan A uv_tp.p)

def Limits_Sub {Γ : sGrpd} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : CategoryTheory.Limits.pullback A uv_tp.p ≅ CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A)

Equations

• Limits_Sub A = ⋯.isoPullback.symm

def GroupoidNMSigma : P.obj Ty ⟶ Ty

Equations

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

@[reducible, inline]

abbrev R : CategoryTheory.Psh sGrpd

Equations

• R = uv_tp.genPb Ty

def GroupoidPair {Γ : sGrpd} (baB : CategoryTheory.yoneda.obj Γ ⟶ uv_tp.compDom uv_tp) : CategoryTheory.yoneda.obj Γ ⟶ Tm

Equations

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

def GroupoidNMPair : uv_tp.compDom uv_tp ⟶ Tm

Equations

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

def SigmaPullBack : CategoryTheory.IsPullback GroupoidNMPair (uv_tp.comp uv_tp).p tp GroupoidNMSigma

Equations

• SigmaPullBack = ⋯

instance instCategorySubtype_groupoidModel (C : Type) [CategoryTheory.Category.{u_1, 0} C] (P : C → Prop) : CategoryTheory.Category.{u_1, 0} { x : C // P x }

Equations

• instCategorySubtype_groupoidModel C P = CategoryTheory.Category.mk ⋯ ⋯ ⋯

instance g (C : Type) [CategoryTheory.Groupoid C] (P : C → Prop) : CategoryTheory.Groupoid { x : C // P x }

Equations

• g C P = CategoryTheory.Groupoid.mk (fun {X Y : { x : C // P x }} (f : X ⟶ Y) => CategoryTheory.Groupoid.inv f) ⋯ ⋯

instance instGroupoidFunctor_groupoidModel (G1 G2 : Type) [CategoryTheory.Groupoid G1] [CategoryTheory.Groupoid G2] : CategoryTheory.Groupoid (CategoryTheory.Functor G1 G2)

Equations

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

def GroupoidPiMap (Γ : CategoryTheory.Grpd) (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal A) CategoryTheory.Grpd) : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd

Equations

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

def GroupoidPi (Γ : CategoryTheory.Grpd) (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal A) CategoryTheory.Grpd) : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd

Equations

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