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

@[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.12, ?u.10} C)

def CategoryTheory.Cat.uLiftFunctor : Functor Cat Cat

Equations

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

@[simp]

theorem CategoryTheory.prod.eqToHom_fst (C : Type u_1) [Category.{u_3, u_1} C] (D : Type u_2) [Category.{u_4, u_2} D] (x y : C × D) (h : x = y) : (eqToHom h).1 = eqToHom ⋯

@[simp]

theorem CategoryTheory.prod.eqToHom_snd (C : Type u_1) [Category.{u_4, u_1} C] (D : Type u_2) [Category.{u_3, u_2} D] (x y : C × D) (h : x = y) : (eqToHom h).2 = eqToHom ⋯

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

@[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

theorem CategoryTheory.Grpd.homOf_id {A : Type u} [Groupoid A] : homOf (Functor.id A) = CategoryStruct.id (of A)

theorem CategoryTheory.Grpd.homOf_comp {A B C : Type u} [Groupoid A] [Groupoid B] [Groupoid C] (F : Functor A B) (G : Functor B C) : homOf (F.comp G) = CategoryStruct.comp (homOf F) (homOf G)

def CategoryTheory.Grpd.asSmallFunctor : Functor Grpd Grpd

Equations

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

@[reducible, inline]

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

The chosen terminal object in D.

Equations

• e.chosenTerminal = e.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

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

The chosen terminal object in D is terminal.

Equations

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

def CategoryTheory.Equivalence.prodCone {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [CartesianMonoidalCategory 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] [CartesianMonoidalCategory 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) [CartesianMonoidalCategory C] : CartesianMonoidalCategory D

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.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.Functor.Grothendieck.cast_eq {Γ : Type u_1} [Category.{u_2, u_1} Γ] {F G : Functor Γ Cat} (h : F = G) (p : F.Grothendieck) : cast ⋯ p = { base := p.base, fiber := cast ⋯ p.fiber }

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

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

theorem CategoryTheory.Functor.Grothendieck.map_eqToHom_obj_base {Γ : Type u_1} [Category.{u_2, u_1} Γ] {F G : Functor Γ Cat} (h : F = G) (x : F.Grothendieck) : ((map (eqToHom h)).obj x).base = x.base

theorem CategoryTheory.Functor.Grothendieck.map_forget {Γ : Type u_1} [Category.{u_2, u_1} Γ] {F G : Functor Γ Cat} (α : F ⟶ G) : (map α).comp (forget G) = forget F

def CategoryTheory.Functor.Grothendieck.asFunctorFrom_fib {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_3, u_2} E] (K : Functor F.Grothendieck E) (c : C) : Functor (↑(F.obj c)) E

Equations

• CategoryTheory.Functor.Grothendieck.asFunctorFrom_fib K c = (CategoryTheory.Functor.Grothendieck.ι F c).comp K

def CategoryTheory.Functor.Grothendieck.asFunctorFrom_hom {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_3, u_2} E] (K : Functor F.Grothendieck E) {c c' : C} (f : c ⟶ c') : asFunctorFrom_fib K c ⟶ comp (F.map f) (asFunctorFrom_fib K c')

Equations

• CategoryTheory.Functor.Grothendieck.asFunctorFrom_hom K f = CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.Grothendieck.ιNatTrans f) K

theorem CategoryTheory.Functor.Grothendieck.asFunctorFrom_hom_app {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_3, u_2} E] (K : Functor F.Grothendieck E) {c c' : C} (f : c ⟶ c') (p : ↑(F.obj c)) : (asFunctorFrom_hom K f).app p = K.map ((ιNatTrans f).app p)

theorem CategoryTheory.Functor.Grothendieck.asFunctorFrom_hom_id {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_3, u_2} E] (K : Functor F.Grothendieck E) (c : C) : asFunctorFrom_hom K (CategoryStruct.id c) = eqToHom ⋯

theorem CategoryTheory.Functor.Grothendieck.asFunctorFrom_hom_comp {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_3, u_2} E] (K : Functor F.Grothendieck E) (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃) : asFunctorFrom_hom K (CategoryStruct.comp f g) = CategoryStruct.comp (asFunctorFrom_hom K f) (CategoryStruct.comp (whiskerLeft (F.map f) (asFunctorFrom_hom K g)) (eqToHom ⋯))

theorem CategoryTheory.Functor.Grothendieck.asFunctorFrom {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_3, u_2} E] (K : Functor F.Grothendieck E) : functorFrom (asFunctorFrom_fib K) (fun {c c' : C} => asFunctorFrom_hom K) ⋯ ⋯ = K

def CategoryTheory.Functor.Grothendieck.functorFrom_comp_fib {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_4, u_2} E] (fib : (c : C) → Functor (↑(F.obj c)) E) {D : Type u_3} [Category.{u_5, u_3} D] (G : Functor E D) (c : C) : Functor (↑(F.obj c)) D

Equations

• CategoryTheory.Functor.Grothendieck.functorFrom_comp_fib fib G c = (fib c).comp G

def CategoryTheory.Functor.Grothendieck.functorFrom_comp_hom {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_4, u_2} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ comp (F.map f) (fib c')) {D : Type u_3} [Category.{u_5, u_3} D] (G : Functor E D) {c c' : C} (f : c ⟶ c') : functorFrom_comp_fib fib G c ⟶ comp (F.map f) (functorFrom_comp_fib fib G c')

Equations

• CategoryTheory.Functor.Grothendieck.functorFrom_comp_hom fib hom G f = CategoryTheory.Functor.whiskerRight (hom f) G

theorem CategoryTheory.Functor.Grothendieck.functorFrom_comp_hom_id {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_5, u_2} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) {D : Type u_3} [Category.{u_4, u_3} D] (G : Functor E D) (c : C) : functorFrom_comp_hom fib (fun {c c' : C} => hom) G (CategoryStruct.id c) = eqToHom ⋯

theorem CategoryTheory.Functor.Grothendieck.functorFrom_comp_hom_comp {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_5, u_2} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ comp (F.map f) (fib c')) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) {D : Type u_3} [Category.{u_4, u_3} D] (G : Functor E D) (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃) : functorFrom_comp_hom fib (fun {c c' : C} => hom) G (CategoryStruct.comp f g) = CategoryStruct.comp (functorFrom_comp_hom fib (fun {c c' : C} => hom) G f) (CategoryStruct.comp (whiskerLeft (F.map f) (functorFrom_comp_hom fib (fun {c c' : C} => hom) G g)) (eqToHom ⋯))

theorem CategoryTheory.Functor.Grothendieck.functorFrom_comp {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_5, u_2} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) {D : Type u_3} [Category.{u_4, u_3} D] (G : Functor E D) : (functorFrom fib (fun {c c' : C} => hom) hom_id hom_comp).comp G = functorFrom (functorFrom_comp_fib fib G) (fun {c c' : C} => functorFrom_comp_hom fib (fun {c c' : C} => hom) G) ⋯ ⋯

theorem CategoryTheory.Functor.Grothendieck.functorFrom_eq_of {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_4, u_2} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) (fib' : (c : C) → Functor (↑(F.obj c)) E) (hom' : {c c' : C} → (f : c ⟶ c') → fib' c ⟶ comp (F.map f) (fib' c')) (hom_id' : ∀ (c : C), hom' (CategoryStruct.id c) = eqToHom ⋯) (hom_comp' : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom' (CategoryStruct.comp f g) = CategoryStruct.comp (hom' f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom' g)) (eqToHom ⋯))) (ef : fib = fib') (hhom : ∀ {c c' : C} (f : c ⟶ c'), CategoryStruct.comp (hom f) (eqToHom ⋯) = CategoryStruct.comp (eqToHom ⋯) (hom' f)) : functorFrom fib (fun {c c' : C} => hom) hom_id hom_comp = functorFrom fib' (fun {c c' : C} => hom') hom_id' hom_comp'

theorem CategoryTheory.Functor.Grothendieck.functorFrom_ext {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_4, u_2} E] {K K' : Functor F.Grothendieck E} (hfib : asFunctorFrom_fib K = asFunctorFrom_fib K') (hhom : ∀ {c c' : C} (f : c ⟶ c'), CategoryStruct.comp (asFunctorFrom_hom K f) (eqToHom ⋯) = CategoryStruct.comp (eqToHom ⋯) (asFunctorFrom_hom K' f)) : K = K'

theorem CategoryTheory.Functor.Grothendieck.functorFrom_hext {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_2} [Category.{u_4, u_2} E] {K K' : Functor F.Grothendieck E} (hfib : asFunctorFrom_fib K = asFunctorFrom_fib K') (hhom : ∀ {c c' : C} (f : c ⟶ c'), asFunctorFrom_hom K f ≍ asFunctorFrom_hom K' f) : K = K'

@[simp]

theorem CategoryTheory.isoWhiskerLeft_eqToIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) {G H : Functor D E} (η : G = H) : F.isoWhiskerLeft (eqToIso η) = eqToIso ⋯

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 := ⋯ }

@[simp]

theorem Equiv.sigmaCongr_apply_fst {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁ → Type u_3} {β₂ : α₂ → Type u_4} (f : α₁ ≃ α₂) (F : (a : α₁) → β₁ a ≃ β₂ (f a)) (x : Sigma β₁) : ((f.sigmaCongr F) x).fst = f x.fst

@[simp]

def Equiv.sigmaCongr_apply_snd {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁ → Type u_3} {β₂ : α₂ → Type u_4} (f : α₁ ≃ α₂) (F : (a : α₁) → β₁ a ≃ β₂ (f a)) (x : Sigma β₁) : ((f.sigmaCongr F) x).snd = (F x.fst) x.snd

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Limits.pullbackHomEquiv {𝒞 : Type u} [Category.{v, u} 𝒞] {A B C Γ : 𝒞} {f : A ⟶ C} {g : B ⟶ C} [HasPullback f g] : (Γ ⟶ 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.

@[simp]

theorem CategoryTheory.IsPullback.lift_fst_snd {C : Type u_1} [Category.{u_2, u_1} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (pb : IsPullback fst snd f g) (w : CategoryStruct.comp fst f = CategoryStruct.comp snd g) : pb.lift fst snd w = CategoryStruct.id P

def CategoryTheory.yonedaIso {C : Type u₁} [SmallCategory C] (F : Functor Cᵒᵖ (Type u₁)) : yoneda.op.comp (yoneda.obj F) ≅ F

A presheaf F on a small category C is isomorphic to the hom-presheaf Hom(y(•),F).

Equations

• CategoryTheory.yonedaIso F = CategoryTheory.NatIso.ofComponents (fun (x : Cᵒᵖ) => CategoryTheory.yonedaEquiv.toIso) ⋯

def CategoryTheory.yonedaIsoMap {C : Type u₁} [SmallCategory C] {F G : Functor Cᵒᵖ (Type u₁)} (app : {X : C} → (yoneda.obj X ⟶ F) → (yoneda.obj X ⟶ G)) (naturality : ∀ {X Y : C} (f : X ⟶ Y) (α : yoneda.obj Y ⟶ F), app (CategoryStruct.comp (yoneda.map f) α) = CategoryStruct.comp (yoneda.map f) (app α)) : yoneda.op.comp (yoneda.obj F) ⟶ yoneda.op.comp (yoneda.obj G)

Equations

• CategoryTheory.yonedaIsoMap app naturality = { app := fun (x : Cᵒᵖ) => app, naturality := ⋯ }

def CategoryTheory.NatTrans.yonedaMk {C : Type u₁} [SmallCategory C] {F G : Functor Cᵒᵖ (Type u₁)} (app : {X : C} → (yoneda.obj X ⟶ F) → (yoneda.obj X ⟶ G)) (naturality : ∀ {X Y : C} (f : X ⟶ Y) (α : yoneda.obj Y ⟶ F), app (CategoryStruct.comp (yoneda.map f) α) = CategoryStruct.comp (yoneda.map f) (app α)) : F ⟶ G

Build natural transformations between presheaves on a small category by defining their action when precomposing by a morphism with representable domain

Equations

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

theorem CategoryTheory.NatTrans.yonedaMk_app {C : Type u₁} [SmallCategory C] {F G : Functor Cᵒᵖ (Type u₁)} (app : {X : C} → (yoneda.obj X ⟶ F) → (yoneda.obj X ⟶ G)) (naturality : ∀ {X Y : C} (f : X ⟶ Y) (α : yoneda.obj Y ⟶ F), app (CategoryStruct.comp (yoneda.map f) α) = CategoryStruct.comp (yoneda.map f) (app α)) {X : C} (α : yoneda.obj X ⟶ F) : CategoryStruct.comp α (yonedaMk (fun {X : C} => app) ⋯) = app α

theorem CategoryTheory.Functor.precomp_heq_of_heq_id {A B : Type u} {C : Type u_1} [Category.{v, u} A] [Category.{v, u} B] [Category.{u_2, u_1} C] (hAB : A = B) (h0 : inferInstance ≍ inferInstance) {F : Functor A B} (h : F ≍ Functor.id B) (G : Functor B C) : F.comp G ≍ G

theorem CategoryTheory.Functor.comp_heq_of_heq_id {A B : Type u} {C : Type u_1} [Category.{v, u} A] [Category.{v, u} B] [Category.{u_2, u_1} C] (hAB : A = B) (h0 : inferInstance ≍ inferInstance) {F : Functor B A} (h : F ≍ Functor.id B) (G : Functor C B) : G.comp F ≍ G