GroupoidModel.Groupoids.PullBackProofs

Here we show some lemmas about pullbacks

theorem CategoryTheory.PointedFunctor.eqToHom_toFunctor {P1 : CategoryTheory.PCat} {P2 : CategoryTheory.PCat} (eq : P1 = P2) :

(CategoryTheory.eqToHom eq).toFunctor = CategoryTheory.eqToHom ⋯

theorem PointedCategory.ext {P1 P2 : PCat.{u,u}} (eq_cat : P1.α = P2.α): P1 = P2 := by sorry

source

theorem CategoryTheory.PointedFunctor.eqToHom_point_help {P1 : CategoryTheory.PCat} {P2 : CategoryTheory.PCat} (eq : P1 = P2) :

(CategoryTheory.eqToHom eq).obj CategoryTheory.PointedCategory.pt = CategoryTheory.PointedCategory.pt

This is the proof of equality used in the eqToHom in PointedFunctor.eqToHom_point

source

theorem CategoryTheory.PointedFunctor.eqToHom_point {P1 : CategoryTheory.PCat} {P2 : CategoryTheory.PCat} (eq : P1 = P2) :

(CategoryTheory.eqToHom eq).point = CategoryTheory.eqToHom ⋯

This shows that the point of an eqToHom in PCat is an eqToHom

source

theorem CategoryTheory.Cat.eqToHom_obj (C1 : CategoryTheory.Cat) (C2 : CategoryTheory.Cat) (x : ↑C1) (eq : C1 = C2) :

(CategoryTheory.eqToHom eq).obj x = cast ⋯ x

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

source

theorem CategoryTheory.Cat.eqToHom_hom_help {C1 : CategoryTheory.Cat} {C2 : CategoryTheory.Cat} (x : ↑C1) (y : ↑C1) (eq : C1 = C2) :

(x ⟶ y) = ((CategoryTheory.eqToHom eq).obj x ⟶ (CategoryTheory.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 : CategoryTheory.Cat} {C2 : CategoryTheory.Cat} {x : ↑C1} {y : ↑C1} (f : x ⟶ y) (eq : C1 = C2) :

(CategoryTheory.eqToHom eq).map f = cast ⋯ f

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

source

theorem CategoryTheory.PCat.eqToHom_hom_help {C1 : CategoryTheory.PCat} {C2 : CategoryTheory.PCat} (x : ↑C1) (y : ↑C1) (eq : C1 = C2) :

(x ⟶ y) = ((CategoryTheory.eqToHom eq).obj x ⟶ (CategoryTheory.eqToHom eq).obj y)

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

source

theorem CategoryTheory.PCat.eqToHom_hom {C1 : CategoryTheory.PCat} {C2 : CategoryTheory.PCat} {x : ↑C1} {y : ↑C1} (f : x ⟶ y) (eq : C1 = C2) :

(CategoryTheory.eqToHom eq).map f = cast ⋯ f

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

source

theorem CategoryTheory.Grothendieck.ext' {Γ : CategoryTheory.Cat} {A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat} (g1 : CategoryTheory.Grothendieck A) (g2 : CategoryTheory.Grothendieck A) (eq_base : g1.base = g2.base) (eq_fiber : g1.fiber = (A.map (CategoryTheory.eqToHom ⋯)).obj g2.fiber) :

g1 = g2

This shows that two objects are equal in Grothendieck A if they have equal bases and fibers that are equal after being cast

source

theorem CategoryTheory.Grothendieck.eqToHom_base {Γ : CategoryTheory.Cat} {A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat} (g1 : CategoryTheory.Grothendieck A) (g2 : CategoryTheory.Grothendieck A) (eq : g1 = g2) :

(CategoryTheory.eqToHom eq).base = CategoryTheory.eqToHom ⋯

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

source

theorem CategoryTheory.Grothendieck.eqToHom_fiber_help {Γ : CategoryTheory.Cat} {A : CategoryTheory.Functor (↑Γ) CategoryTheory.Cat} {g1 : CategoryTheory.Grothendieck A} {g2 : CategoryTheory.Grothendieck A} (eq : g1 = g2) :

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

(CategoryTheory.eqToHom eq).fiber = CategoryTheory.eqToHom ⋯

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

source

theorem CategoryTheory.RightSidedEqToHom {C : Type v} [CategoryTheory.Category.{u_1, v} C] {x : C} {y : C} {z : C} (eq : y = z) {f : x ⟶ y} {g : x ⟶ z} (heq : HEq f g) :

CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom eq) = g

This eliminates an eqToHom on the right side of an equality

source

theorem CategoryTheory.CastEqToHomSolve {C : Type v} [CategoryTheory.Category.{u_1, v} C] {x : C} {x1 : C} {x2 : C} {y : C} {y1 : C} {y2 : C} (eqx1 : x = x1) (eqx2 : x = x2) (eqy1 : y1 = y) (eqy2 : y2 = y) {f : x1 ⟶ y1} {g : x2 ⟶ y2} (heq : HEq f g) :