theorem CategoryTheory.ObjectProperty.ι_mono {T C : Type u} [Category.{v, u} C] [Category.{v, u} T] {Z : C → Prop} (f g : Functor T (FullSubcategory Z)) (e : f.comp (ι Z) = g.comp (ι Z)) : f = g

def GroupoidModel.FunctorOperation.conjugating {Γ : Type u} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor Γ CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) : CategoryTheory.Functor (CategoryTheory.Functor ↑(A.obj x) ↑(B.obj x)) (CategoryTheory.Functor ↑(A.obj y) ↑(B.obj y))

The functor that, on objects G : A.obj x ⥤ B.obj x acts by creating the map on the right, by taking the inverse of f : x ⟶ y in the groupoid A f A x --------> A y | . | | | . G | | conjugating A B f G | . V V B x --------> B y B f

Equations

• GroupoidModel.FunctorOperation.conjugating A B f = CategoryTheory.Functor.whiskeringLeftObjWhiskeringRightObj (A.map (CategoryTheory.Groupoid.inv f)) (B.map f)

@[simp]

theorem GroupoidModel.FunctorOperation.conjugating_obj {Γ : Type u} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor Γ CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) (s : CategoryTheory.Functor ↑(A.obj x) ↑(B.obj x)) : (conjugating A B f).obj s = CategoryTheory.Functor.comp (CategoryTheory.inv (A.map f)) (s.comp (B.map f))

@[simp]

theorem GroupoidModel.FunctorOperation.conjugating_id {Γ : Type u} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor Γ CategoryTheory.Grpd) (x : Γ) : conjugating A B (CategoryTheory.CategoryStruct.id x) = CategoryTheory.Functor.id (CategoryTheory.Functor ↑(A.obj x) ↑(B.obj x))

@[simp]

theorem GroupoidModel.FunctorOperation.conjugating_comp {Γ : Type u} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor Γ CategoryTheory.Grpd) (x y z : Γ) (f : x ⟶ y) (g : y ⟶ z) : conjugating A B (CategoryTheory.CategoryStruct.comp f g) = (conjugating A B f).comp (conjugating A B g)

def GroupoidModel.FunctorOperation.IsSection {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor B A) (s : CategoryTheory.Functor A B) : Prop

Equations

• GroupoidModel.FunctorOperation.IsSection F s = (s.comp F = CategoryTheory.Functor.id A)

@[reducible, inline]

abbrev GroupoidModel.FunctorOperation.Section {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor B A) : Type (max (max (max u_4 u_3) u_2) u_1)

Equations

• GroupoidModel.FunctorOperation.Section F = CategoryTheory.ObjectProperty.FullSubcategory (GroupoidModel.FunctorOperation.IsSection F)

instance GroupoidModel.FunctorOperation.Section.category {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor B A) : CategoryTheory.Category.{max u_1 u_4, max (max (max u_4 u_3) u_2) u_1} (Section F)

Equations

• GroupoidModel.FunctorOperation.Section.category F = CategoryTheory.ObjectProperty.FullSubcategory.category (GroupoidModel.FunctorOperation.IsSection F)

@[reducible, inline]

abbrev GroupoidModel.FunctorOperation.Section.ι {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor B A) : CategoryTheory.Functor (Section F) (CategoryTheory.Functor A B)

Equations

• GroupoidModel.FunctorOperation.Section.ι F = CategoryTheory.ObjectProperty.ι (GroupoidModel.FunctorOperation.IsSection F)

instance GroupoidModel.FunctorOperation.Section.groupoid {A : Type u_1} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_3} [CategoryTheory.Groupoid B] (F : CategoryTheory.Functor B A) : CategoryTheory.Groupoid (Section F)

Equations

• GroupoidModel.FunctorOperation.Section.groupoid F = CategoryTheory.InducedCategory.groupoid (CategoryTheory.Functor A B) fun (f : GroupoidModel.FunctorOperation.Section F) => f.obj

@[reducible, inline]

abbrev GroupoidModel.FunctorOperation.sigma.fstAuxObj {Γ : Type u_1} [CategoryTheory.Category.{u_2, u_1} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (x : Γ) : CategoryTheory.Functor (sigmaObj B x) ↑(A.obj x)

Equations

• GroupoidModel.FunctorOperation.sigma.fstAuxObj B x = CategoryTheory.Grothendieck.Groupoidal.forget

def GroupoidModel.FunctorOperation.piObj {Γ : Type u_1} [CategoryTheory.Category.{u_2, u_1} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (x : Γ) : Type (max v₁ u₁)

Equations

• GroupoidModel.FunctorOperation.piObj B x = GroupoidModel.FunctorOperation.Section (GroupoidModel.FunctorOperation.sigma.fstAuxObj B x)

instance GroupoidModel.FunctorOperation.piObj.groupoid {Γ : Type u_1} [CategoryTheory.Category.{u_2, u_1} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (x : Γ) : CategoryTheory.Groupoid (piObj B x)

Equations

• GroupoidModel.FunctorOperation.piObj.groupoid B x = inferInstanceAs (CategoryTheory.Groupoid (GroupoidModel.FunctorOperation.Section (GroupoidModel.FunctorOperation.sigma.fstAuxObj B x)))

theorem GroupoidModel.FunctorOperation.isSection_conjugating_isSection {Γ : CategoryTheory.Grpd} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : ↑Γ} (f : x ⟶ y) (s : piObj B x) : IsSection (sigma.fstAuxObj B y) (((Section.ι (sigma.fstAuxObj B x)).comp (conjugating A (sigma A B) f)).obj s)

If s : piObj B x then the underlying functor is of the form s : A x ⥤ sigma A B x and it is a section of the forgetful functor sigma A B x ⥤ A x. This theorem states that conjugating A f⁻¹ ⋙ s ⋙ sigma A B f⁻¹ : A y ⥤ sigma A B y using some f : x ⟶ y produces a section of the forgetful functor sigma A B y ⥤ A y.

def GroupoidModel.FunctorOperation.piMap {Γ : CategoryTheory.Grpd} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : ↑Γ} (f : x ⟶ y) : CategoryTheory.Functor (piObj B x) (piObj B y)

The functorial action of pi on a morphism f : x ⟶ y in Γ is given by "conjugation". Since piObj B x is a full subcategory of sigma A B x ⥤ A x, we obtain the action piMap : piObj B x ⥤ piObj B y as the induced map in the following diagram the inclusion Section.ι piObj B x ⥤ (A x ⥤ sigma A B x) ⋮ || ⋮ || conjugating A (sigma A B) f VV VV piObj B y ⥤ (A y ⥤ sigma A B y)

Equations

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

theorem GroupoidModel.FunctorOperation.piMap.obj {Γ : CategoryTheory.Grpd} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : ↑Γ} (f : x ⟶ y) (s : piObj B x) : ((piMap A B f).obj s).obj = (conjugating A (sigma A B) f).obj s.obj

theorem GroupoidModel.FunctorOperation.piMap.map {Γ : CategoryTheory.Grpd} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : ↑Γ} (f : x ⟶ y) (s1 s2 : piObj B x) (η : s1 ⟶ s2) : (Section.ι (sigma.fstAuxObj B y)).map ((piMap A B f).map η) = (conjugating A (sigma A B) f).map η

theorem GroupoidModel.FunctorOperation.piMap_ι {Γ : CategoryTheory.Grpd} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : ↑Γ} (f : x ⟶ y) : (piMap A B f).comp (Section.ι (sigma.fstAuxObj B y)) = (Section.ι (sigma.fstAuxObj B x)).comp (conjugating A (sigma A B) f)

The square commutes

piObj B x ⥤ (A x ⥤ sigma A B x) ⋮ || piMap⋮ || conjugating A (sigma A B) f VV VV piObj B y ⥤ (A y ⥤ sigma A B y)

@[simp]

theorem GroupoidModel.FunctorOperation.piMap_id {Γ : CategoryTheory.Grpd} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (x : ↑Γ) : piMap A B (CategoryTheory.CategoryStruct.id x) = CategoryTheory.Functor.id (piObj B x)

theorem GroupoidModel.FunctorOperation.piMap_comp {Γ : CategoryTheory.Grpd} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y z : ↑Γ} (f : x ⟶ y) (g : y ⟶ z) : piMap A B (CategoryTheory.CategoryStruct.comp f g) = (piMap A B f).comp (piMap A B g)

def GroupoidModel.FunctorOperation.pi {Γ : CategoryTheory.Grpd} {A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd

The formation rule for Σ-types for the ambient natural model base unfolded into operations between functors

Equations

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

def GroupoidModel.FunctorOperation.smallUPi_app {Γ : Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj smallU.Ty) : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ty

Equations

• GroupoidModel.FunctorOperation.smallUPi_app AB = GroupoidModel.yonedaCategoryEquiv.symm (GroupoidModel.FunctorOperation.pi (GroupoidModel.smallU.PtpEquiv.snd AB))

def GroupoidModel.FunctorOperation.smallUPi.Pi : smallU.Ptp.obj smallU.Ty ⟶ smallU.Ty

The formation rule for Π-types for the natural model smallU

Equations

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

def GroupoidModel.FunctorOperation.smallUPi.lam : smallU.Ptp.obj smallU.Tm ⟶ smallU.Tm

The introduction rule for Π-types for the natural model smallU

Equations

• GroupoidModel.FunctorOperation.smallUPi.lam = CategoryTheory.NatTrans.yonedaMk (fun {X : GroupoidModel.Ctx} => sorry) @GroupoidModel.FunctorOperation.smallUPi.lam._proof_1

def GroupoidModel.FunctorOperation.smallUPi : smallU.NaturalModelPi

Equations

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

def GroupoidModel.FunctorOperation.uHomSeqPis' (i : ℕ) (ilen : i < 4) : (uHomSeqObjs i ilen).NaturalModelPi

Equations

• GroupoidModel.FunctorOperation.uHomSeqPis' 0 ilen_2 = GroupoidModel.FunctorOperation.smallUPi
• GroupoidModel.FunctorOperation.uHomSeqPis' 1 ilen_2 = GroupoidModel.FunctorOperation.smallUPi
• GroupoidModel.FunctorOperation.uHomSeqPis' 2 ilen_2 = GroupoidModel.FunctorOperation.smallUPi
• GroupoidModel.FunctorOperation.uHomSeqPis' 3 ilen_2 = GroupoidModel.FunctorOperation.smallUPi
• GroupoidModel.FunctorOperation.uHomSeqPis' n.succ.succ.succ.succ ilen_2 = ⋯.elim

def GroupoidModel.FunctorOperation.uHomSeqPis : NaturalModelBase.UHomSeqPiSigma Ctx

Equations

• GroupoidModel.FunctorOperation.uHomSeqPis = { toUHomSeq := GroupoidModel.uHomSeq, nmPi := GroupoidModel.FunctorOperation.uHomSeqPis', nmSigma := GroupoidModel.uHomSeqSigmas' }