GroupoidModel.ForMathlib

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

source

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

source

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) ⋯)

source

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✝

source

@[simp]

theorem Part.assert_dom {α : Type u_1} (P : Prop) (x : P → Part α) :

(assert P x).Dom ↔ ∃ (h : P), (x h).Dom

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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)

Instances For

source

def CategoryTheory.Cat.uLiftFunctor :

Functor Cat Cat

Equations

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

Instances For

source

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

source

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

source

theorem CategoryTheory.Grothendieck.cast_eq {Γ : Type u_1} [Category.{u_2, u_1} Γ] {F G : Functor Γ Cat} (h : F = G) (p : Grothendieck F) :

cast ⋯ p = { base := p.base, fiber := cast ⋯ p.fiber }

source

theorem CategoryTheory.Grothendieck.obj_hext {Γ : Type u_1} [Category.{u_2, u_1} Γ] {A : Functor Γ Cat} {x y : Grothendieck A} (hbase : x.base = y.base) (hfiber : x.fiber ≍ y.fiber) :

x = y

source

theorem CategoryTheory.Grothendieck.obj_hext_iff {Γ : Type u_1} [Category.{u_2, u_1} Γ] {A : Functor Γ Cat} {x y : Grothendieck A} :

x.base = y.base ∧ x.fiber ≍ y.fiber ↔ x = y

source

theorem CategoryTheory.Grothendieck.obj_hext' {Γ : Type u_1} [Category.{u_2, u_1} Γ] {A A' : Functor Γ Cat} (h : A = A') {x : Grothendieck A} {y : Grothendieck A'} (hbase : x.base ≍ y.base) (hfiber : x.fiber ≍ y.fiber) :

x ≍ y

source

theorem CategoryTheory.Grothendieck.hext' {Γ : Type u_1} [Category.{u_2, u_1} Γ] {A A' : Functor Γ Cat} (h : A = A') {X Y : Grothendieck A} {X' Y' : Grothendieck A'} (f : X.Hom Y) (g : X'.Hom Y') (hX : X ≍ X') (hY : Y ≍ Y') (w_base : f.base ≍ g.base) (w_fiber : f.fiber ≍ g.fiber) :

f ≍ g

source

theorem CategoryTheory.Grothendieck.eqToHom_base {Γ : Type u_1} [Category.{u_3, u_1} Γ] {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

source

theorem CategoryTheory.Grothendieck.eqToHom_fiber_aux {Γ : Type u} [Category.{v, u} Γ] {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

source

theorem CategoryTheory.Grothendieck.eqToHom_fiber {Γ : Type u} [Category.{v, u} Γ] {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

source

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

x = y

source

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

A.obj G1.base = A.obj G2.base

source

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

A.map (eqToHom eq).base = eqToHom ⋯

source

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

((map (eqToHom h)).obj x).base = x.base

source

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

(map α).comp (forget G) = forget F

source

def CategoryTheory.Grothendieck.mkIso {C : Type u_2} [Category.{u_3, u_2} 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.

Instances For

source

theorem CategoryTheory.Grothendieck.Functor.hext {Γ : Type u_1} [Category.{u_4, u_1} Γ] {A : Functor Γ Cat} {C : Type u_2} [Category.{u_3, u_2} C] (F G : Functor C (Grothendieck A)) (hbase : F.comp (forget A) = G.comp (forget A)) (hfiber_obj : ∀ (x : C), (F.obj x).fiber ≍ (G.obj x).fiber) (hfiber_map : ∀ {x y : C} (f : x ⟶ y), (F.map f).fiber ≍ (G.map f).fiber) :

F = G

source

theorem CategoryTheory.Grothendieck.hext_iff {Γ : Type u_1} [Category.{u_3, u_1} Γ] {A : Functor Γ Cat} (x y : Grothendieck A) (f g : x ⟶ y) :

f.base = g.base ∧ f.fiber ≍ g.fiber ↔ f = g

source

@[simp]

theorem CategoryTheory.Grothendieck.preNatIso_hom_app_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) {G H : Functor D C} (α : G ≅ H) (x : Grothendieck (G.comp F)) :

((preNatIso F α).hom.app x).base = α.hom.app x.base

source

@[simp]

theorem CategoryTheory.Grothendieck.preNatIso_hom_app_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) {G H : Functor D C} (α : G ≅ H) (x : Grothendieck (G.comp F)) :

((preNatIso F α).hom.app x).fiber = CategoryStruct.id ((F.map ((preNatIso F α).hom.app x).base).obj ((pre F G).obj x).fiber)

source

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

source

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

source

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

source

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

source

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

source

@[simp]

theorem CategoryTheory.AsSmall.up_comp_down {C : Type u₁} [Category.{v₁, u₁} C] :

up.comp down = Functor.id C

source

@[simp]

theorem CategoryTheory.AsSmall.down_comp_up {C : Type u₁} [Category.{v₁, u₁} C] :

down.comp up = Functor.id (AsSmall C)

source

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

up.IsEquivalence

source

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

Groupoid (AsSmall Γ)

Equations

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

source

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

Instances For

source

theorem CategoryTheory.Grpd.homOf_id {A : Type u} [Groupoid A] :

homOf (Functor.id A) = CategoryStruct.id (of A)

source

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)

source

def CategoryTheory.Grpd.asSmallFunctor :

Functor Grpd Grpd

Equations

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

Instances For

source

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

The chosen terminal object in D.

Equations

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

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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

ULift.downFunctor.ReflectsIsomorphisms

source

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

ULift.upFunctor.ReflectsIsomorphisms

source

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

AsSmall.down.ReflectsIsomorphisms

source

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

AsSmall.up.ReflectsIsomorphisms

source

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

source

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 ⋯))

source

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 ⋯

source

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 ⋯))

source

@[simp]

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

(ι (σ.comp A) x).comp (pre A σ) = ι A (σ.obj x)

source

theorem CategoryTheory.Grothendieck.preNatIso_congr {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) {G H : Functor D C} {α β : G ≅ H} (h : α = β) :

preNatIso F α = preNatIso F β ≪≫ eqToIso ⋯

source

@[simp]

theorem CategoryTheory.Grothendieck.preNatIso_eqToIso {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) {G H : Functor D C} {h : G = H} :

preNatIso F (eqToIso h) = eqToIso ⋯

source

theorem CategoryTheory.Grothendieck.preNatIso_comp {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) {G1 G2 G3 : Functor D C} (α : G1 ≅ G2) (β : G2 ≅ G3) :

preNatIso F (α ≪≫ β) = preNatIso F α ≪≫ (map (Functor.whiskerRight α.hom F)).isoWhiskerLeft (preNatIso F β) ≪≫ eqToIso ⋯

source

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

Functor (↑(F.obj c)) E

Equations

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

Instances For

source

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

asFunctorFrom_fib K c ⟶ Functor.comp (F.map f) (asFunctorFrom_fib K c')

Equations

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

Instances For

source

theorem CategoryTheory.Grothendieck.asFunctorFrom_hom_app {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_2, u_1} E] (K : Functor (Grothendieck F) E) {c c' : C} (f : c ⟶ c') (p : ↑(F.obj c)) :

(asFunctorFrom_hom K f).app p = K.map ((ιNatTrans f).app p)

source

theorem CategoryTheory.Grothendieck.asFunctorFrom_hom_id {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_2, u_1} E] (K : Functor (Grothendieck F) E) (c : C) :

asFunctorFrom_hom K (CategoryStruct.id c) = eqToHom ⋯

source

theorem CategoryTheory.Grothendieck.asFunctorFrom_hom_comp {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_2, u_1} E] (K : Functor (Grothendieck F) 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 (Functor.whiskerLeft (F.map f) (asFunctorFrom_hom K g)) (eqToHom ⋯))

source

theorem CategoryTheory.Grothendieck.asFunctorFrom {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_2, u_1} E] (K : Functor (Grothendieck F) E) :

functorFrom (asFunctorFrom_fib K) (fun {c c' : C} => asFunctorFrom_hom K) ⋯ ⋯ = K

source

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

Functor (↑(F.obj c)) D

Equations

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

Instances For

source

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

functorFrom_comp_fib fib G c ⟶ Functor.comp (F.map f) (functorFrom_comp_fib fib G c')

Equations

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

Instances For

source

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

functorFrom_comp_hom fib (fun {c c' : C} => hom) G (CategoryStruct.id c) = eqToHom ⋯

source

theorem CategoryTheory.Grothendieck.functorFrom_comp_hom_comp {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_4, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.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 (Functor.whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) {D : Type u_2} [Category.{u_3, u_2} 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 (Functor.whiskerLeft (F.map f) (functorFrom_comp_hom fib (fun {c c' : C} => hom) G g)) (eqToHom ⋯))

source

theorem CategoryTheory.Grothendieck.functorFrom_comp {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_4, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.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 (Functor.whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) {D : Type u_2} [Category.{u_3, u_2} 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) ⋯ ⋯

source

theorem CategoryTheory.Grothendieck.functorFrom_eq_of {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_3, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.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 (Functor.whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) (fib' : (c : C) → Functor (↑(F.obj c)) E) (hom' : {c c' : C} → (f : c ⟶ c') → fib' c ⟶ Functor.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 (Functor.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'

source

theorem CategoryTheory.Grothendieck.functorFrom_ext {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_3, u_1} E] {K K' : Functor (Grothendieck F) 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'

source

theorem CategoryTheory.Grothendieck.functorFrom_hext {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_3, u_1} E] {K K' : Functor (Grothendieck F) 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'

source

theorem CategoryTheory.Grothendieck.hext {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X Y : Grothendieck F} (f g : X.Hom Y) (w_base : f.base = g.base) (w_fiber : f.fiber ≍ g.fiber) :

f = g

source

theorem CategoryTheory.Grothendieck.functorTo_map_id_aux {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (x : D) :

((A.comp F).map (CategoryStruct.id x)).obj (fibObj x) = fibObj x

source

theorem CategoryTheory.Grothendieck.functorTo_map_comp_aux {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) {x y z : D} (f : x ⟶ y) (g : y ⟶ z) :

((A.comp F).map (CategoryStruct.comp f g)).obj (fibObj x) = (F.map (A.map g)).obj (((A.comp F).map f).obj (fibObj x))

source

def CategoryTheory.Grothendieck.functorTo {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))) :

Functor D (Grothendieck F)

To define a functor into Grothendieck F we can make use of an existing functor into the base.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Grothendieck.functorTo_obj_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))) (x : D) :

((functorTo A fibObj (fun {x y : D} => fibMap) map_id ⋯).obj x).base = A.obj x

source

@[simp]

theorem CategoryTheory.Grothendieck.functorTo_obj_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))) (x : D) :

((functorTo A fibObj (fun {x y : D} => fibMap) map_id ⋯).obj x).fiber = fibObj x

source

@[simp]

theorem CategoryTheory.Grothendieck.functorTo_map_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))) {x y : D} (f : x ⟶ y) :

((functorTo A fibObj (fun {x y : D} => fibMap) map_id ⋯).map f).base = A.map f

source

@[simp]

theorem CategoryTheory.Grothendieck.functorTo_map_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))) {x y : D} (f : x ⟶ y) :

((functorTo A fibObj (fun {x y : D} => fibMap) map_id ⋯).map f).fiber = fibMap f

source

@[simp]

theorem CategoryTheory.Grothendieck.functorTo_forget {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} {A : Functor D C} {fibObj : (x : D) → ↑((A.comp F).obj x)} {fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y} {map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯} {map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))} :

(functorTo A fibObj fibMap map_id ⋯).comp (forget F) = A

source

def CategoryTheory.Grothendieck.functorTo' {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) ≍ CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g)) :

Functor D (Grothendieck F)

To define a functor into Grothendieck F we can make use of an existing functor into the base.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Grothendieck.functorTo'_obj_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) ≍ CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g)) (x : D) :

((functorTo' A fibObj (fun {x y : D} => fibMap) map_id ⋯).obj x).base = A.obj x

source

@[simp]

theorem CategoryTheory.Grothendieck.functorTo'_obj_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) ≍ CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g)) (x : D) :

((functorTo' A fibObj (fun {x y : D} => fibMap) map_id ⋯).obj x).fiber = fibObj x

source

@[simp]

theorem CategoryTheory.Grothendieck.functorTo'_map_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) ≍ CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g)) {x y : D} (f : x ⟶ y) :

((functorTo' A fibObj (fun {x y : D} => fibMap) map_id ⋯).map f).base = A.map f

source

@[simp]

theorem CategoryTheory.Grothendieck.functorTo'_map_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) ≍ CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g)) {x y : D} (f : x ⟶ y) :

((functorTo' A fibObj (fun {x y : D} => fibMap) map_id ⋯).map f).fiber = fibMap f

source

@[simp]

theorem CategoryTheory.Grothendieck.functorTo'_forget {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} {A : Functor D C} {fibObj : (x : D) → ↑((A.comp F).obj x)} {fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y} {map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯} {map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) ≍ CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g)} :

(functorTo' A fibObj fibMap map_id ⋯).comp (forget F) = A

source

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

source

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

Instances For

source

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

source

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

⋯ = ⋯

Instances For

source

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.

Instances For

source

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

source

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) ⋯

Instances For

source

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

Instances For

source

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.

Instances For

source

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 α

source

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

source

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