This file contains declarations missing from mathlib, to be upstreamed.

@[simp]

theorem CategoryTheory.Limits.terminal.comp_from_assoc {C : Type u₁} [Category.{v₁, u₁} C] [HasTerminal C] {P Q : C} (f : P ⟶ Q) {Z : C} (h : ⊤_ C ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp («from» Q) h) = CategoryStruct.comp («from» P) h

@[simp]

theorem CategoryTheory.Limits.initial.to_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] [HasInitial C] {P Q : C} (f : P ⟶ Q) {Z : C} (h : Q ⟶ Z) : CategoryStruct.comp («to» P) (CategoryStruct.comp f h) = CategoryStruct.comp («to» Q) h

@[simp]

theorem CategoryTheory.Limits.IsTerminal.comp_from_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (t : IsTerminal Z) {X Y : C} (f : X ⟶ Y) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp f (CategoryStruct.comp (t.from Y) h) = CategoryStruct.comp (t.from X) h

@[simp]

theorem CategoryTheory.Limits.IsInitial.to_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (t : IsInitial X) {Y Z : C} (f : Y ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (t.to Y) (CategoryStruct.comp f h) = CategoryStruct.comp (t.to Z) h

theorem CategoryTheory.Limits.PullbackCone.IsLimit.comp_lift {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z W' W : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (σ : W' ⟶ W) (ht : IsLimit t) (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : CategoryStruct.comp σ (ht.lift (PullbackCone.mk h k w)) = ht.lift (PullbackCone.mk (CategoryStruct.comp σ h) (CategoryStruct.comp σ k) ⋯)

theorem CategoryTheory.Limits.PullbackCone.IsLimit.comp_lift_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z W' W : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (σ : W' ⟶ W) (ht : IsLimit t) (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : t.pt ⟶ Z✝) : CategoryStruct.comp σ (CategoryStruct.comp (ht.lift (PullbackCone.mk h k w)) h✝) = CategoryStruct.comp (ht.lift (PullbackCone.mk (CategoryStruct.comp σ h) (CategoryStruct.comp σ k) ⋯)) h✝

@[simp]

theorem Part.assert_dom {α : Type u_1} (P : Prop) (x : P → Part α) : (assert P x).Dom ↔ ∃ (h : P), (x h).Dom

theorem CategoryTheory.ULift.comp_downFunctor_inj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F G : Functor C (ULift.{u, u₂} D)) : F.comp downFunctor = G.comp downFunctor ↔ F = G

theorem CategoryTheory.ULift.comp_upFunctor_inj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F G : Functor C D) : F.comp upFunctor = G.comp upFunctor ↔ F = G

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

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

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

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

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

This turns the object part of eqToHom functors into casts

@[reducible, inline]

abbrev CategoryTheory.Cat.homOf {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] (F : Functor C D) : of C ⟶ of D

Equations

• CategoryTheory.Cat.homOf F = F

def CategoryTheory.Cat.ULift_lte_iso_self {C : Type (max u u₁)} [Category.{v, max u u₁} C] : of (ULift.{u, max u u₁} C) ≅ of C

Equations

• CategoryTheory.Cat.ULift_lte_iso_self = { hom := CategoryTheory.ULift.downFunctor, inv := CategoryTheory.ULift.upFunctor, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Cat.ULift_lte_iso_self_inv {C : Type (max u u₁)} [Category.{v, max u u₁} C] : ULift_lte_iso_self.inv = ULift.upFunctor

@[simp]

theorem CategoryTheory.Cat.ULift_lte_iso_self_hom {C : Type (max u u₁)} [Category.{v, max u u₁} C] : ULift_lte_iso_self.hom = ULift.downFunctor

def CategoryTheory.Cat.ULift_succ_iso_self {C : Type (u + 1)} [Category.{v, u + 1} C] : of (ULift.{u, u + 1} C) ≅ of C

Equations

• CategoryTheory.Cat.ULift_succ_iso_self = CategoryTheory.Cat.ULift_lte_iso_self

def CategoryTheory.Cat.ULift_iso_self {C : Type u} [Category.{v, u} C] : of (ULift.{u, u} C) ≅ of C

Equations

• CategoryTheory.Cat.ULift_iso_self = CategoryTheory.Cat.ULift_lte_iso_self

def CategoryTheory.Cat.ofULift (C : Type u) [Category.{v, u} C] : Cat

Equations

• CategoryTheory.Cat.ofULift C = CategoryTheory.Cat.of (ULift.{?u.19, ?u.17} C)

def CategoryTheory.Cat.uLiftFunctor : Functor Cat Cat

Equations

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

theorem CategoryTheory.Grothendieck.obj_ext_hEq {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {x y : Grothendieck A} (hbase : x.base = y.base) (hfiber : HEq x.fiber y.fiber) : x = y

theorem CategoryTheory.Grothendieck.eqToHom_base {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {x y : Grothendieck A} (eq : x = y) : (eqToHom eq).base = eqToHom ⋯

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

theorem CategoryTheory.Grothendieck.eqToHom_fiber_aux {Γ : Cat} {A : Functor (↑Γ) Cat} {g1 g2 : Grothendieck A} (eq : g1 = g2) : (A.map (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 {Γ : Cat} {A : Functor (↑Γ) Cat} {g1 g2 : Grothendieck A} (eq : g1 = g2) : (eqToHom eq).fiber = eqToHom ⋯

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

theorem CategoryTheory.Grothendieck.obj_ext_cast {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {x y : Grothendieck A} (hbase : x.base = y.base) (hfiber : cast ⋯ x.fiber = y.fiber) : x = y

theorem CategoryTheory.Grothendieck.map_eqToHom_base_pf {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {G1 G2 : Grothendieck A} (eq : G1 = G2) : A.obj G1.base = A.obj G2.base

theorem CategoryTheory.Grothendieck.map_eqToHom_base {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {G1 G2 : Grothendieck A} (eq : G1 = G2) : A.map (eqToHom eq).base = eqToHom ⋯

def CategoryTheory.Grothendieck.mkIso {C : Type u₁} [Category.{v₁, u₁} C] {G : Functor C Cat} {X Y : 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.

theorem CategoryTheory.IsPullback.of_iso_isPullback {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) {Q : C} (i : Q ≅ P) : IsPullback (CategoryStruct.comp i.hom fst) (CategoryStruct.comp i.hom snd) f g

@[reducible, inline]

abbrev CategoryTheory.Grpd.chosenTerminal : Grpd

The chosen terminal object in Grpd.

Equations

• CategoryTheory.Grpd.chosenTerminal = CategoryTheory.Grpd.of (CategoryTheory.Discrete PUnit.{?u.3 + 1})

def CategoryTheory.Grpd.chosenTerminalIsTerminal : Limits.IsTerminal chosenTerminal

The chosen terminal object in Grpd is terminal.

Equations

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

def CategoryTheory.Grpd.prodCone (C D : Grpd) : Limits.BinaryFan C D

The chosen product of categories C × D yields a product cone in Grpd.

Equations

• C.prodCone D = CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Prod.fst ↑C ↑D) (CategoryTheory.Prod.snd ↑C ↑D)

def CategoryTheory.Grpd.isLimitProdCone (X Y : Grpd) : Limits.IsLimit (X.prodCone Y)

The product cone in Grpd is indeed a product.

Equations

• X.isLimitProdCone Y = CategoryTheory.Limits.BinaryFan.isLimitMk (fun (S : CategoryTheory.Limits.BinaryFan X Y) => CategoryTheory.Functor.prod' S.fst S.snd) ⋯ ⋯ ⋯

instance CategoryTheory.Grpd.instChosenFiniteProducts_groupoidModel : ChosenFiniteProducts Grpd

Equations

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

theorem CategoryTheory.Grpd.id_eq_id (X : Grpd) : CategoryStruct.id X = Functor.id ↑X

The identity in the category of groupoids equals the identity functor.

theorem CategoryTheory.Grpd.comp_eq_comp {X Y Z : Grpd} (F : X ⟶ Y) (G : Y ⟶ Z) : CategoryStruct.comp F G = Functor.comp F G

Composition in the category of groupoids equals functor composition.

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

@[simp]

theorem CategoryTheory.AsSmall.up_map_down_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : down.map (up.map f) = f

@[simp]

theorem CategoryTheory.AsSmall.down_map_up_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : AsSmall C} (f : X ⟶ Y) : up.map (down.map f) = f

theorem CategoryTheory.AsSmall.comp_up_inj {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F G : Functor C D} (h : F.comp up = G.comp up) : F = G

theorem CategoryTheory.AsSmall.comp_down_inj {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F G : Functor C (AsSmall D)} (h : F.comp down = G.comp down) : F = G

@[simp]

theorem CategoryTheory.AsSmall.up_comp_down {C : Type u₁} [Category.{v₁, u₁} C] : up.comp down = Functor.id C

@[simp]

theorem CategoryTheory.AsSmall.down_comp_up {C : Type u₁} [Category.{v₁, u₁} C] : down.comp up = Functor.id (AsSmall C)

instance CategoryTheory.AsSmall.instIsEquivalenceUp_groupoidModel {C : Type u} [Category.{v, u} C] : up.IsEquivalence

instance CategoryTheory.Groupoid.asSmallGroupoid (Γ : Type u) [Groupoid Γ] : Groupoid (AsSmall Γ)

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Grpd.homOf {C D : Type u} [Groupoid C] [Groupoid D] (F : Functor C D) : of C ⟶ of D

Equations

• CategoryTheory.Grpd.homOf F = F

def CategoryTheory.Grpd.asSmallFunctor : Functor Grpd Grpd

Equations

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

@[simp]

theorem CategoryTheory.Core.id_inv {C : Type u} [Category.{v, u} C] (X : C) : (CategoryStruct.id X).inv = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Core.comp_inv {C : Type u} [Category.{v, u} C] {X Y Z : Core C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).inv = CategoryStruct.comp g.inv f.inv

def CategoryTheory.Core.map' {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) : Functor (Core C) (Core D)

Equations

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

theorem CategoryTheory.Core.map'_comp_inclusion {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) : (map' F).comp (inclusion D) = (inclusion C).comp F

def CategoryTheory.Core.map : Functor Cat Grpd

Equations

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

def CategoryTheory.Core.functorToCoreEquiv {D : Type u₁} [Category.{v₁, u₁} D] {Γ : Type u} [Groupoid Γ] : Functor Γ D ≃ Functor Γ (Core D)

Equations

• CategoryTheory.Core.functorToCoreEquiv = { toFun := CategoryTheory.Core.functorToCore, invFun := CategoryTheory.Core.forgetFunctorToCore.obj, left_inv := ⋯, right_inv := ⋯ }

theorem CategoryTheory.Core.eqToIso_hom {C : Type u} [Category.{v, u} C] {a b : Core C} (h1 : a = b) (h2 : (inclusion C).obj a = (inclusion C).obj b) : (eqToHom h1).hom = eqToHom h2

theorem CategoryTheory.Core.functorToCore_naturality_left {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] {G' : Type u₃} [Groupoid G'] (H : Functor G C) (F : Functor G' G) : functorToCore (F.comp H) = F.comp (functorToCore H)

theorem CategoryTheory.Core.functorToCore_naturality_right {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] {C' : Type u₃} [Category.{v₃, u₃} C'] (H : Functor G C) (F : Functor C C') : functorToCore (H.comp F) = (functorToCore H).comp (map' F)

def CategoryTheory.Core.adjunction : Grpd.forgetToCat ⊣ map

Equations

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

theorem CategoryTheory.Core.inclusion_comp_functorToCore {G : Type u₂} [Groupoid G] : (inclusion G).comp (functorToCore (Functor.id G)) = Functor.id (Core G)

Mildly evil.

instance CategoryTheory.Core.instIsIsoGrpdHomOfInclusion {G : Type u₂} [Groupoid G] : IsIso (Grpd.homOf (inclusion G))

Mildly evil.

instance CategoryTheory.Core.instIsIsoGrpdHomOfFunctorToCoreId {G : Type u} [Groupoid G] : IsIso (Grpd.homOf (functorToCore (Functor.id G)))

Mildly evil.

instance CategoryTheory.Core.instIsLeftAdjointGrpdCatForgetToCat_groupoidModel : Grpd.forgetToCat.IsLeftAdjoint

instance CategoryTheory.Core.instIsRightAdjointGrpdCatMap : map.IsRightAdjoint

theorem CategoryTheory.Core.IsPullback.w' {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] (F : Functor C D) : CategoryStruct.comp (Cat.homOf (inclusion C)) (Cat.homOf F) = Functor.comp (Cat.homOf (map' F)) (Cat.homOf (inclusion D))

def CategoryTheory.Core.IsPullback.lift {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] {F : Functor C D} [F.ReflectsIsomorphisms] (s : Limits.PullbackCone (Cat.homOf F) (Cat.homOf (inclusion D))) : Functor (↑s.pt) (Core C)

Equations

• CategoryTheory.Core.IsPullback.lift s = { obj := s.fst.obj, map := fun {x y : ↑s.pt} (f : x ⟶ y) => CategoryTheory.asIso (s.fst.map f), map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Core.IsPullback.fac_left {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] {F : Functor C D} [F.ReflectsIsomorphisms] (s : Limits.PullbackCone (Cat.homOf F) (Cat.homOf (inclusion D))) : CategoryStruct.comp (lift s) (Cat.homOf (inclusion C)) = s.fst

@[simp]

theorem CategoryTheory.Core.IsPullback.fac_right {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] {F : Functor C D} [F.ReflectsIsomorphisms] (s : Limits.PullbackCone (Cat.homOf F) (Cat.homOf (inclusion D))) : CategoryStruct.comp (lift s) (Cat.homOf (map' F)) = s.snd

def CategoryTheory.Core.IsPullback.lift_uniq {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] {F : Functor C D} [F.ReflectsIsomorphisms] (s : Limits.PullbackCone (Cat.homOf F) (Cat.homOf (inclusion D))) (m : s.pt ⟶ Cat.of (Core C)) (fl : CategoryStruct.comp m (Cat.homOf (inclusion C)) = s.fst) : m = lift s

Equations

• ⋯ = ⋯

theorem CategoryTheory.Core.isPullback_map'_self {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] (F : Functor C D) [F.ReflectsIsomorphisms] : IsPullback (Cat.homOf (inclusion C)) (Cat.homOf (map' F)) (Cat.homOf F) (Cat.homOf (inclusion D))

In the category of categories, if functor F : C ⥤ D reflects isomorphisms then taking the Core is pullback stable along F

Core C ---- inclusion -----> C | | | | | | Core.map' F F | | | | V V Core D ---- inclusion -----> D

@[reducible, inline]

abbrev CategoryTheory.Equivalence.chosenTerminal {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [ChosenFiniteProducts C] (e : C ≌ D) : D

The chosen terminal object in D.

Equations

• e.chosenTerminal = e.functor.obj (𝟙_ C)

def CategoryTheory.Equivalence.chosenTerminalIsTerminal {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [ChosenFiniteProducts C] (e : C ≌ D) : Limits.IsTerminal e.chosenTerminal

The chosen terminal object in D is terminal.

Equations

• e.chosenTerminalIsTerminal = CategoryTheory.Limits.IsTerminal.isTerminalObj e.functor (𝟙_ C) (CategoryTheory.Limits.IsTerminal.ofUnique (𝟙_ C))

def CategoryTheory.Equivalence.prodCone {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [ChosenFiniteProducts C] (e : C ≌ D) (X Y : D) : Limits.BinaryFan X Y

Product cones in D are defined using chosen products in C

Equations

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

def CategoryTheory.Equivalence.isLimitProdCone {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [ChosenFiniteProducts C] (e : C ≌ D) (X Y : D) : Limits.IsLimit (e.prodCone X Y)

The chosen product cone in D is a limit.

Equations

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

def CategoryTheory.Equivalence.chosenFiniteProducts {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (e : C ≌ D) [ChosenFiniteProducts C] : ChosenFiniteProducts D

Equations

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

def CategoryTheory.ULift.Core.isoCoreULift {C : Type u} [Category.{v, u} C] : Cat.of (ULift.{w, u} (Core C)) ≅ Cat.of (Core (ULift.{w, u} C))

Equations

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

def CategoryTheory.functorToAsSmallEquiv {D : Type u₁} [Category.{v₁, u₁} D] {C : Type u} [Category.{v, u} C] : Functor D (AsSmall C) ≃ Functor D C

Equations

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

instance CategoryTheory.instReflectsIsomorphismsULiftDownFunctor_groupoidModel (C : Type u) [Category.{v, u} C] : ULift.downFunctor.ReflectsIsomorphisms

instance CategoryTheory.instReflectsIsomorphismsULiftUpFunctor_groupoidModel (C : Type u) [Category.{v, u} C] : ULift.upFunctor.ReflectsIsomorphisms

instance CategoryTheory.instReflectsIsomorphismsAsSmallDown_groupoidModel (C : Type u) [Category.{v, u} C] : AsSmall.down.ReflectsIsomorphisms

instance CategoryTheory.instReflectsIsomorphismsAsSmallUp_groupoidModel (C : Type u) [Category.{v, u} C] : AsSmall.up.ReflectsIsomorphisms

@[simp]

theorem CategoryTheory.Grpd.map_id_obj {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {x : Γ} {a : ↑(A.obj x)} : (A.map (CategoryStruct.id x)).obj a = a

theorem CategoryTheory.Grpd.map_id_map {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {x : Γ} {a b : ↑(A.obj x)} {f : a ⟶ b} : (A.map (CategoryStruct.id x)).map f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp f (eqToHom ⋯))

theorem CategoryTheory.Grpd.map_comp_obj {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {x y z : Γ} {f : x ⟶ y} {g : y ⟶ z} {a : ↑(A.obj x)} : (A.map (CategoryStruct.comp f g)).obj a = (A.map g).obj ((A.map f).obj a)

theorem CategoryTheory.Grpd.map_comp_map {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {x y z : Γ} {f : x ⟶ y} {g : y ⟶ z} {a b : ↑(A.obj x)} {φ : a ⟶ b} : (A.map (CategoryStruct.comp f g)).map φ = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((A.map g).map ((A.map f).map φ)) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Cat.map_id_obj {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Cat} {x : Γ} {a : ↑(A.obj x)} : (A.map (CategoryStruct.id x)).obj a = a

theorem CategoryTheory.Cat.map_id_map {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Cat} {x : Γ} {a b : ↑(A.obj x)} {f : a ⟶ b} : (A.map (CategoryStruct.id x)).map f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp f (eqToHom ⋯))

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

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

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

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

theorem CategoryTheory.Grothendieck.ιNatTrans_id_app {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X : C} {a : ↑(F.obj X)} : (ιNatTrans (CategoryStruct.id X)).app a = eqToHom ⋯

theorem CategoryTheory.Grothendieck.ιNatTrans_comp_app {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {a : ↑(F.obj X)} : (ιNatTrans (CategoryStruct.comp f g)).app a = CategoryStruct.comp ((ιNatTrans f).app a) (CategoryStruct.comp ((ιNatTrans g).app ((F.map f).obj a)) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Grothendieck.ιCompPre {Γ : Type u₂} [Category.{v₂, u₂} Γ] {Δ : Type u₃} [Category.{v₃, u₃} Δ] (σ : Functor Δ Γ) (A : Functor Γ Cat) (x : Δ) : (ι (σ.comp A) x).comp (pre A σ) = ι A (σ.obj x)

def Equiv.psigmaCongrProp {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : α₁ → Prop} {β₂ : α₂ → Prop} (f : α₁ ≃ α₂) (F : ∀ (a : α₁), β₁ a ↔ β₂ (f a)) : PSigma β₁ ≃ PSigma β₂

Equations

• f.psigmaCongrProp F = { toFun := fun (x : PSigma β₁) => ⟨f x.fst, ⋯⟩, invFun := fun (x : PSigma β₂) => ⟨f.symm x.fst, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

noncomputable def CategoryTheory.Limits.pullbackHomEquiv {𝒞 : Type u} [Category.{v, u} 𝒞] [HasPullbacks 𝒞] {A B C Γ : 𝒞} {f : A ⟶ C} {g : B ⟶ C} : (Γ ⟶ pullback f g) ≃ (fst : Γ ⟶ A) × (snd : Γ ⟶ B) ×' CategoryStruct.comp fst f = CategoryStruct.comp snd g

Equations

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