GroupoidModel.Groupoids.Pi

source

theorem hcongr_fun {α α' : Type u} (hα : α ≍ α') (β : α → Type v) (β' : α' → Type v) (hβ : β ≍ β') (f : (x : α) → β x) (f' : (x : α') → β' x) (hf : f ≍ f') {x : α} {x' : α'} (hx : x ≍ x') :

f x ≍ f' x'

source

theorem CategoryTheory.Functor.Iso.whiskerLeft_inv_hom_heq {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Category.{v₂, u₂} E] (F : C ≅≅ D) (G H : Functor D E) (η : G ⟶ H) :

(F.inv.comp F.hom).whiskerLeft η ≍ η

source

theorem CategoryTheory.Functor.Iso.whiskerLeft_inv_hom {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Category.{v₂, u₂} E] (F : C ≅≅ D) (G H : Functor D E) (η : G ⟶ H) :

(F.inv.comp F.hom).whiskerLeft η = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp η (eqToHom ⋯))

source

theorem CategoryTheory.Functor.Iso.whiskerLeft_hom_inv_heq {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Category.{v₂, u₂} E] (F : D ≅≅ C) (G H : Functor D E) (η : G ⟶ H) :

(F.hom.comp F.inv).whiskerLeft η ≍ η

source

theorem CategoryTheory.Functor.Iso.whiskerLeft_hom_inv {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Category.{v₂, u₂} E] (F : D ≅≅ C) (G H : Functor D E) (η : G ⟶ H) :

(F.hom.comp F.inv).whiskerLeft η = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp η (eqToHom ⋯))

source

def CategoryTheory.Grpd.functorIsoOfIso {A B : Grpd} (F : A ≅ B) :

↑A ≅≅ ↑B

Equations

CategoryTheory.Grpd.functorIsoOfIso F = { hom := F.hom, inv := F.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Grpd.functorIsoOfIso_hom {A B : Grpd} (F : A ≅ B) :

(functorIsoOfIso F).hom = F.hom

source

@[simp]

theorem CategoryTheory.Grpd.functorIsoOfIso_inv {A B : Grpd} (F : A ≅ B) :

(functorIsoOfIso F).inv = F.inv

source

def CategoryTheory.Grpd.Functor.iso {Γ : Type u} [Groupoid Γ] (A : Functor Γ Grpd) {x y : Γ} (f : x ⟶ y) :

↑(A.obj x) ≅≅ ↑(A.obj y)

Equations

CategoryTheory.Grpd.Functor.iso A f = CategoryTheory.Grpd.functorIsoOfIso (A.mapIso (CategoryTheory.asIso f))

Instances For

source

def CategoryTheory.Grpd.Functor.iso_hom {Γ : Type u} [Groupoid Γ] (A : Functor Γ Grpd) {x y : Γ} (f : x ⟶ y) :

(iso A f).hom = A.map f

Equations

⋯ = ⋯

Instances For

source

def CategoryTheory.Grpd.Functor.iso_inv {Γ : Type u} [Groupoid Γ] (A : Functor Γ Grpd) {x y : Γ} (f : x ⟶ y) :

(iso A f).inv = A.map (inv f)

Equations

⋯ = ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Grpd.Functor.iso_id {Γ : Type u} [Groupoid Γ] (A : Functor Γ Grpd) (x : Γ) :

iso A (CategoryStruct.id x) = Functor.Iso.refl ↑(A.obj x)

source

@[simp]

theorem CategoryTheory.Grpd.Functor.iso_comp {Γ : Type u} [Groupoid Γ] (A : Functor Γ Grpd) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) :

iso A (CategoryStruct.comp f g) = iso A f ≪⋙ iso A g

source

@[simp]

theorem CategoryTheory.Grpd.Functor.iso_naturality {Γ : Type u} [Groupoid Γ] {Δ : Type u₁} [Groupoid Δ] (A : Functor Γ Grpd) (σ : Functor Δ Γ) {x y : Δ} (f : x ⟶ y) :

iso (σ.comp A) f = iso A (σ.map f)

source

theorem CategoryTheory.Grpd.Functor.hcongr_obj {C C' D D' : Grpd} (hC : C = C') (hD : D = D') {F : Functor ↑C ↑D} {F' : Functor ↑C' ↑D'} (hF : F ≍ F') {x : ↑C} {x' : ↑C'} (hx : x ≍ x') :

F.obj x ≍ F'.obj x'

source

theorem CategoryTheory.Grpd.whiskerLeft_hcongr_right {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {E E' : Grpd} (hE : E ≍ E') (F : Functor C D) {G H : Functor D ↑E} {G' H' : Functor D ↑E'} (hG : G ≍ G') (hH : H ≍ H') {α : G ⟶ H} {α' : G' ⟶ H'} (hα : α ≍ α') :

F.whiskerLeft α ≍ F.whiskerLeft α'

source

theorem CategoryTheory.Grpd.comp_hcongr {C C' D D' E E' : Grpd} (hC : C ≍ C') (hD : D ≍ D') (hE : E ≍ E') {F : Functor ↑C ↑D} {F' : Functor ↑C' ↑D'} {G : Functor ↑D ↑E} {G' : Functor ↑D' ↑E'} (hF : F ≍ F') (hG : G ≍ G') :

F.comp G ≍ F'.comp G'

source

theorem CategoryTheory.Grpd.NatTrans.hext {X X' Y Y' : Grpd} (hX : X = X') (hY : Y = Y') {F G : Functor ↑X ↑Y} {F' G' : Functor ↑X' ↑Y'} (hF : F ≍ F') (hG : G ≍ G') (α : F ⟶ G) (α' : F' ⟶ G') (happ : ∀ (x : ↑X), α.app x ≍ α'.app ((eqToHom hX).obj x)) :

α ≍ α'

source

theorem CategoryTheory.Functor.associator_eq {C : Type u_1} {D : Type u_2} {E : Type u_3} {E' : Type u_4} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} E] [Category.{u_8, u_4} E'] (F : Functor C D) (G : Functor D E) (H : Functor E E') :

F.associator G H = CategoryTheory.Iso.refl ((F.comp G).comp H)

source

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

Prop

Equations

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

Instances For

source

@[reducible, inline]

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

Type (max (max (max u_4 u_3) u_2) u_1)

Equations

CategoryTheory.Section F = CategoryTheory.ObjectProperty.FullSubcategory (CategoryTheory.IsSection F)

Instances For

source

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

Category.{max u_1 u_4, max (max (max u_4 u_3) u_2) u_1} (Section F)

Equations

CategoryTheory.Section.category F = CategoryTheory.ObjectProperty.FullSubcategory.category (CategoryTheory.IsSection F)

source

@[reducible, inline]

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

Functor (Section F) (Functor A B)

Equations

CategoryTheory.Section.ι F = CategoryTheory.ObjectProperty.ι (CategoryTheory.IsSection F)

Instances For

source

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

source

instance CategoryTheory.instGroupoidFullSubcategory_groupoidModel {C : Type u_1} [Groupoid C] (P : ObjectProperty C) :

Groupoid P.FullSubcategory

Equations

CategoryTheory.instGroupoidFullSubcategory_groupoidModel P = CategoryTheory.InducedCategory.groupoid C P.ι.obj

source

instance CategoryTheory.Grpd.ι_mono (G : Grpd) (P : ObjectProperty ↑G) :

Mono (homOf P.ι)

source

theorem CategoryTheory.Grpd.ObjectProperty.FullSubcategory.congr {A A' : Grpd} (hA : A ≍ A') (P : ObjectProperty ↑A) (P' : ObjectProperty ↑A') (hP : P ≍ P') (a : ↑A) (a' : ↑A') (ha : a ≍ a') (ha✝ : P a) (ha' : P' a') :

{ obj := a, property := ha✝ } ≍ { obj := a', property := ha' }

source

theorem CategoryTheory.Grpd.ObjectProperty.FullSubcategory.hext {A A' : Grpd} (hA : A ≍ A') (P : ObjectProperty ↑A) (P' : ObjectProperty ↑A') (hP : P ≍ P') (p : P.FullSubcategory) (p' : P'.FullSubcategory) (hp : p.obj ≍ p'.obj) :

p ≍ p'

source

theorem GroupoidModel.smallU.PtpEquiv.fst_app_comp_map_tp {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj smallU.Tm) :

fst (CategoryTheory.CategoryStruct.comp ab (smallU.Ptp.map smallU.tp)) = fst ab

source

theorem GroupoidModel.smallU.PtpEquiv.snd_app_comp_map_tp {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj smallU.Tm) :

snd (CategoryTheory.CategoryStruct.comp ab (smallU.Ptp.map smallU.tp)) ≍ (snd ab).comp CategoryTheory.PGrpd.forgetToGrpd

source

def GroupoidModel.FunctorOperation.conjugating' {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A 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.inv f)) (B.map f)

Instances For

source

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

CategoryTheory.Grpd.of (CategoryTheory.Functor ↑(A.obj x) ↑(B.obj x)) ⟶ CategoryTheory.Grpd.of (CategoryTheory.Functor ↑(A.obj y) ↑(B.obj y))

Equations

GroupoidModel.FunctorOperation.conjugating A B f = GroupoidModel.FunctorOperation.conjugating' A B f

Instances For

source

theorem GroupoidModel.FunctorOperation.conjugating_obj {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A 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 (A.map (CategoryTheory.inv f)) (s.comp (B.map f))

source

theorem GroupoidModel.FunctorOperation.conjugating_map {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A B : CategoryTheory.Functor Γ CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) {s1 s2 : CategoryTheory.Functor ↑(A.obj x) ↑(B.obj x)} (h : s1 ⟶ s2) :

(conjugating A B f).map h = CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.whiskerLeft (A.map (CategoryTheory.inv f)) h) (B.map f)

source

@[simp]

theorem GroupoidModel.FunctorOperation.conjugating_id {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A B : CategoryTheory.Functor Γ CategoryTheory.Grpd) (x : Γ) :

conjugating A B (CategoryTheory.CategoryStruct.id x) = CategoryTheory.Functor.id ↑(CategoryTheory.Grpd.of (CategoryTheory.Functor ↑(A.obj x) ↑(B.obj x)))

source

@[simp]

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

conjugating A B (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.Functor.comp (conjugating A B f) (conjugating A B g)

source

@[simp]

theorem GroupoidModel.FunctorOperation.conjugating_naturality_map {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A B : CategoryTheory.Functor Γ CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Groupoid Δ] (σ : CategoryTheory.Functor Δ Γ) {x y : Δ} (f : x ⟶ y) :

conjugating (σ.comp A) (σ.comp B) f = conjugating A B (σ.map f)

source

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

((CategoryTheory.Grpd.Functor.iso A f).inv.comp (S.comp (CategoryTheory.Grpd.Functor.iso B f).hom) ⟶ T) ≃ (S.comp (CategoryTheory.Grpd.Functor.iso B f).hom ⟶ (CategoryTheory.Grpd.Functor.iso A f).hom.comp T)

Equations

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

Instances For

source

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

(CategoryTheory.Functor.comp (A.map (CategoryTheory.inv f)) (S.comp (B.map f)) ⟶ T) ≃ (S.comp (B.map f) ⟶ CategoryTheory.Functor.comp (A.map f) T)

Equations

GroupoidModel.FunctorOperation.conjugatingObjNatTransEquiv A B f S T = GroupoidModel.FunctorOperation.conjugatingObjNatTransEquiv' A B f S T

Instances For

source

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

(CategoryTheory.Functor.comp (A.map (CategoryTheory.inv f)) (S.comp (B.map f)) ⟶ T) ≃ (S.comp (B.map f) ≅ CategoryTheory.Functor.comp (A.map f) T)

Equations

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

Instances For

source

@[reducible, inline]

abbrev GroupoidModel.FunctorOperation.sigma.fstAuxObj {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) (x : Γ) :

CategoryTheory.Functor ((CategoryTheory.Functor.Groupoidal.ι A x).comp B).Groupoidal ↑(A.obj x)

Equations

GroupoidModel.FunctorOperation.sigma.fstAuxObj B x = CategoryTheory.Functor.Groupoidal.forget

Instances For

source

def GroupoidModel.FunctorOperation.piObj {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) (x : Γ) :

CategoryTheory.Grpd

Equations

GroupoidModel.FunctorOperation.piObj B x = CategoryTheory.Grpd.of (CategoryTheory.Section (GroupoidModel.FunctorOperation.sigma.fstAuxObj B x))

Instances For

source

theorem GroupoidModel.FunctorOperation.piObj.hext {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A A' : CategoryTheory.Functor Γ CategoryTheory.Grpd} (hA : A ≍ A') {B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd} {B' : CategoryTheory.Functor A'.Groupoidal CategoryTheory.Grpd} (hB : B ≍ B') (x : Γ) (f : ↑(piObj B x)) (f' : ↑(piObj B' x)) (hf : f.obj ≍ f'.obj) :

f ≍ f'

source

theorem GroupoidModel.FunctorOperation.isSection_conjugating_isSection {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) (s : ↑(piObj B x)) :

CategoryTheory.IsSection (sigma.fstAuxObj B y) (((CategoryTheory.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.

source

def GroupoidModel.FunctorOperation.piMap {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal 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.

Instances For

source

theorem GroupoidModel.FunctorOperation.piMap_obj_obj {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal 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

source

theorem GroupoidModel.FunctorOperation.piMap_map {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) (s1 s2 : ↑(piObj B x)) (η : s1 ⟶ s2) :

(piMap A B f).map η = (conjugating A (sigma A B) f).map η

source

theorem GroupoidModel.FunctorOperation.piMap_ι {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) :

(piMap A B f).comp (CategoryTheory.Section.ι (sigma.fstAuxObj B y)) = (CategoryTheory.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)

source

@[simp]

theorem GroupoidModel.FunctorOperation.piMap_id {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) (x : Γ) :

piMap A B (CategoryTheory.CategoryStruct.id x) = CategoryTheory.Functor.id ↑(piObj B x)

source

theorem GroupoidModel.FunctorOperation.piMap_comp {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal 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)

source

def GroupoidModel.FunctorOperation.pi {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) :

CategoryTheory.Functor Γ CategoryTheory.Grpd

The formation rule for Π-types for the natural model smallU as operations between functors

Equations

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

Instances For

source

@[simp]

theorem GroupoidModel.FunctorOperation.pi_obj {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) (x : Γ) :

(pi A B).obj x = piObj B x

source

@[simp]

theorem GroupoidModel.FunctorOperation.pi_map {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {X✝ Y✝ : Γ} (f : X✝ ⟶ Y✝) :

(pi A B).map f = piMap A B f

source

theorem GroupoidModel.FunctorOperation.IsSection_eq {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Groupoid Δ] (σ : CategoryTheory.Functor Δ Γ) (x : Δ) :

sigma.fstAuxObj B (σ.obj x) ≍ sigma.fstAuxObj ((CategoryTheory.Functor.Groupoidal.pre A σ).comp B) x

source

theorem GroupoidModel.FunctorOperation.piObj_naturality {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Groupoid Δ] (σ : CategoryTheory.Functor Δ Γ) (x : Δ) :

piObj B (σ.obj x) = piObj ((CategoryTheory.Functor.Groupoidal.pre A σ).comp B) x

source

theorem GroupoidModel.FunctorOperation.eqToHom_ι_aux {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Groupoid Δ] (σ : CategoryTheory.Functor Δ Γ) (x : Δ) :

CategoryTheory.Grpd.of (CategoryTheory.Functor (↑(A.obj (σ.obj x))) ((CategoryTheory.Functor.Groupoidal.ι A (σ.obj x)).comp B).Groupoidal) = CategoryTheory.Grpd.of (CategoryTheory.Functor (↑(A.obj (σ.obj x))) ((CategoryTheory.Functor.Groupoidal.ι (σ.comp A) x).comp ((CategoryTheory.Functor.Groupoidal.pre A σ).comp B)).Groupoidal)

source

theorem GroupoidModel.FunctorOperation.ObjectProperty.eqToHom_comp_ι {C D : CategoryTheory.Grpd} (h : C = D) (P : CategoryTheory.ObjectProperty ↑C) (Q : CategoryTheory.ObjectProperty ↑D) (hP : P ≍ Q) :

have h' := ⋯; CategoryTheory.Functor.comp (CategoryTheory.eqToHom h') Q.ι = P.ι.comp (CategoryTheory.eqToHom h)

source

theorem GroupoidModel.FunctorOperation.eqToHom_ι' {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Groupoid Δ] (σ : CategoryTheory.Functor Δ Γ) (x : Δ) :

CategoryTheory.ObjectProperty.ι (CategoryTheory.IsSection (sigma.fstAuxObj ((CategoryTheory.Functor.Groupoidal.pre A σ).comp B) x)) ≍ CategoryTheory.ObjectProperty.ι (CategoryTheory.IsSection (sigma.fstAuxObj B (σ.obj x)))

source

theorem GroupoidModel.FunctorOperation.eqToHom_ι {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Groupoid Δ] (σ : CategoryTheory.Functor Δ Γ) (x : Δ) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Grpd.homOf (CategoryTheory.ObjectProperty.ι (CategoryTheory.IsSection (sigma.fstAuxObj ((CategoryTheory.Functor.Groupoidal.pre A σ).comp B) x)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Grpd.homOf (CategoryTheory.ObjectProperty.ι (CategoryTheory.IsSection (sigma.fstAuxObj B (σ.obj x))))) (CategoryTheory.eqToHom ⋯)

source

theorem GroupoidModel.FunctorOperation.FullSubcategory.lift_comp_inclusion_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) :

(P.lift F hF).comp P.ι = F

source

theorem GroupoidModel.FunctorOperation.conjugating_naturality_sigma {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Groupoid Δ] (σ : CategoryTheory.Functor Δ Γ) {x y : Δ} (f : x ⟶ y) :

conjugating (σ.comp A) (sigma (σ.comp A) ((CategoryTheory.Functor.Groupoidal.pre A σ).comp B)) f ≍ conjugating A (sigma A B) (σ.map f)

source

theorem GroupoidModel.FunctorOperation.eqToHom_conjugating {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Groupoid Δ] (σ : CategoryTheory.Functor Δ Γ) {x y : Δ} (f : x ⟶ y) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (conjugating (σ.comp A) (sigma (σ.comp A) ((CategoryTheory.Functor.Groupoidal.pre A σ).comp B)) f) = CategoryTheory.CategoryStruct.comp (conjugating A (sigma A B) (σ.map f)) (CategoryTheory.eqToHom ⋯)

source

CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h i

source

theorem GroupoidModel.FunctorOperation.pi_naturality_map {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Groupoid Δ] (σ : CategoryTheory.Functor Δ Γ) {x y : Δ} (f : x ⟶ y) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Grpd.homOf (piMap A B (σ.map f))) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Grpd.homOf (piMap (σ.comp A) ((CategoryTheory.Functor.Groupoidal.pre A σ).comp B) f))

source

theorem GroupoidModel.FunctorOperation.pi_naturality {Γ : Type u₂} [CategoryTheory.Groupoid Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Groupoid Δ] (σ : CategoryTheory.Functor Δ Γ) :

σ.comp (pi A B) = pi (σ.comp A) ((CategoryTheory.Functor.Groupoidal.pre A σ).comp B)

source

def GroupoidModel.FunctorOperation.pi.strongTrans.naturality {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) (s : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hs : s.comp CategoryTheory.PGrpd.forgetToGrpd = pi A B) {x y : Γ} (g : x ⟶ y) :

CategoryTheory.Functor.comp (A.map g) (CategoryTheory.PGrpd.objFiber' hs y).obj ≅ (CategoryTheory.PGrpd.objFiber' hs x).obj.comp (sigmaMap B g)

Equations

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

Instances For

source

def GroupoidModel.FunctorOperation.pi.strongTrans {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) (s : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hs : s.comp CategoryTheory.PGrpd.forgetToGrpd = pi A B) :

(A.comp CategoryTheory.Grpd.forgetToCat).toPseudoFunctor'.StrongTrans ((sigma A B).comp CategoryTheory.Grpd.forgetToCat).toPseudoFunctor'

Equations

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

Instances For

source

@[simp]

theorem GroupoidModel.FunctorOperation.pi.strongTrans_naturality {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) (s : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hs : s.comp CategoryTheory.PGrpd.forgetToGrpd = pi A B) {x y : CategoryTheory.LocallyDiscrete Γ} (g : x ⟶ y) :

(strongTrans B s hs).naturality g = strongTrans.naturality B s hs g.as

source

@[simp]

theorem GroupoidModel.FunctorOperation.pi.strongTrans_app {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) (s : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hs : s.comp CategoryTheory.PGrpd.forgetToGrpd = pi A B) (x : CategoryTheory.LocallyDiscrete Γ) :

(strongTrans B s hs).app x = (CategoryTheory.PGrpd.objFiber' hs x.as).obj

source

def GroupoidModel.FunctorOperation.pi.mapStrongTrans {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) (s : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hs : s.comp CategoryTheory.PGrpd.forgetToGrpd = pi A B) :

CategoryTheory.Functor A.Groupoidal (sigma A B).Groupoidal

Equations

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

Instances For

source

def GroupoidModel.FunctorOperation.pi.inversion {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor A.Groupoidal CategoryTheory.Grpd) (s : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hs : s.comp CategoryTheory.PGrpd.forgetToGrpd = pi A B) :

CategoryTheory.Functor A.Groupoidal CategoryTheory.PGrpd

Let Γ be a category. For any pair of functors A : Γ ⥤ Grpd and B : ∫(A) ⥤ Grpd, and any "term of pi", meaning a functor f : Γ ⥤ PGrpd satisfying f ⋙ forgetToGrpd = pi A B : Γ ⥤ Grpd, there is a "term of B" inversion : Γ ⥤ PGrpd such that inversion ⋙ forgetToGrpd = B.

Equations