theorem
CategoryTheory.UvPoly.η_naturality
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
{E B E' B' : C}
{P : UvPoly E B}
{P' : UvPoly E' B'}
(e : E ⟶ E')
(b : B ⟶ B')
(hp : IsPullback P.p e b P'.p)
:
CategoryStruct.comp ((Over.pullback P.p).whiskerLeft (Over.mapPullbackAdj e).unit)
(CategoryStruct.comp (Functor.whiskerRight (pullbackMapIsoSquare ⋯).hom (Over.pullback e))
((Over.map b).whiskerLeft (((Over.pullbackComp P.p b).symm ≪≫ eqToIso ⋯) ≪≫ Over.pullbackComp e P'.p).inv)) = Functor.whiskerRight (Over.mapPullbackAdj b).unit (Over.pullback P.p)
theorem
CategoryTheory.UvPoly.η_naturality'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
{E B E' B' : C}
{P : UvPoly E B}
{P' : UvPoly E' B'}
(e : E ⟶ E')
(b : B ⟶ B')
(hp : IsPullback P.p e b P'.p)
:
let bmap := Over.map b;
let emap := Over.map e;
let pbk := Over.pullback P.p;
let ebk := Over.pullback e;
let bbk := Over.pullback b;
let p'bk := Over.pullback P'.p;
have α := pullbackMapIsoSquare ⋯;
have bb := ((Over.pullbackComp P.p b).symm ≪≫ eqToIso ⋯) ≪≫ Over.pullbackComp e P'.p;
CategoryStruct.comp (pbk.whiskerLeft (Over.mapPullbackAdj e).unit)
(CategoryStruct.comp (Functor.whiskerRight α.hom ebk) (bmap.whiskerLeft bb.inv)) = Functor.whiskerRight (Over.mapPullbackAdj b).unit pbk
theorem
CategoryTheory.UvPoly.pushforwardPullbackIsoSquare_eq
{C : Type u_1}
[Category.{u_2, u_1} C]
[Limits.HasPullbacks C]
{X Y Z W : C}
{h : X ⟶ Z}
{f : X ⟶ Y}
{g : Z ⟶ W}
{k : Y ⟶ W}
(pb : IsPullback h f g k)
[ExponentiableMorphism f]
[ExponentiableMorphism g]
:
pushforwardPullbackIsoSquare pb = (conjugateIsoEquiv ((Over.mapPullbackAdj k).comp (ExponentiableMorphism.adj g))
((ExponentiableMorphism.adj f).comp (Over.mapPullbackAdj h)))
(asIso (Over.pullbackMapTwoSquare h f g k ⋯))
theorem
CategoryTheory.UvPoly.ev_naturality
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
{E B E' B' : C}
{P : UvPoly E B}
{P' : UvPoly E' B'}
(e : E ⟶ E')
(b : B ⟶ B')
(hp : IsPullback P.p e b P'.p)
:
let pfwd := ExponentiableMorphism.pushforward P.p;
let p'fwd := ExponentiableMorphism.pushforward P'.p;
let pbk := Over.pullback P.p;
let ebk := Over.pullback e;
let bbk := Over.pullback b;
let p'bk := Over.pullback P'.p;
have β := (pushforwardPullbackIsoSquare ⋯).inv;
have bb := ((Over.pullbackComp P.p b).symm ≪≫ eqToIso ⋯) ≪≫ Over.pullbackComp e P'.p;
CategoryStruct.comp (Functor.whiskerRight β pbk)
(CategoryStruct.comp (p'fwd.whiskerLeft bb.hom) (Functor.whiskerRight (ExponentiableMorphism.ev P'.p) ebk)) = ebk.whiskerLeft (ExponentiableMorphism.ev P.p)
theorem
CategoryTheory.UvPoly.associator_eq_id
{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')
:
theorem
CategoryTheory.UvPoly.whiskerRight_left'
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
{B : 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} B]
(F : Functor B C)
{G H : Functor C D}
(α : G ⟶ H)
(K : Functor D E)
:
theorem
CategoryTheory.UvPoly.id_whiskerLeft'
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
{G H : Functor C D}
(α : G ⟶ H)
:
theorem
CategoryTheory.UvPoly.whiskerLeft_twice'
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
{B : 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} B]
(F : Functor B C)
(G : Functor C D)
{H K : Functor D E}
(α : H ⟶ K)
:
theorem
CategoryTheory.UvPoly.whiskerRight_twice'
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
{B : 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} B]
{H K : Functor B C}
(F : Functor C D)
(G : Functor D E)
(α : H ⟶ K)
:
@[simp]
theorem
CategoryTheory.UvPoly.cartesianNatTrans_fstProj
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B E' B' : C}
(P : UvPoly E B)
(P' : UvPoly E' B')
(e : E ⟶ E')
(b : B ⟶ B')
(pb : IsPullback P.p e b P'.p)
(X : C)
:
CategoryStruct.comp ((P.cartesianNatTrans P' b e pb).app X) (P'.fstProj X) = CategoryStruct.comp (P.fstProj X) b
theorem
CategoryTheory.UvPoly.fan_snd_map'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B E' B' : C}
{P : UvPoly E B}
{P' : UvPoly E' B'}
(e : E ⟶ E')
(b : B ⟶ B')
(A : C)
(hp : IsPullback P.p e b P'.p)
:
CategoryStruct.comp
(Limits.pullback.map (P.fstProj A) P.p (P'.fstProj A) P'.p ((P.cartesianNatTrans P' b e hp).app A) e b ⋯ ⋯)
(PartialProduct.fan P' A).snd = (PartialProduct.fan P A).snd
theorem
CategoryTheory.UvPoly.fan_snd_map
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B A E' B' A' : C}
{P : UvPoly E B}
{P' : UvPoly E' B'}
(e : E ⟶ E')
(b : B ⟶ B')
(a : A ⟶ A')
(hp : IsPullback P.p e b P'.p)
:
CategoryStruct.comp
(Limits.pullback.map (P.fstProj A) P.p (P'.fstProj A') P'.p
(CategoryStruct.comp ((P.cartesianNatTrans P' b e hp).app A) (P'.functor.map a)) e b ⋯ ⋯)
(PartialProduct.fan P' A').snd = CategoryStruct.comp (PartialProduct.fan P A).snd a
theorem
CategoryTheory.UvPoly.ε_map
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B A E' B' A' : C}
{P : UvPoly E B}
{P' : UvPoly E' B'}
(e : E ⟶ E')
(b : B ⟶ B')
(a : A ⟶ A')
(hp : IsPullback P.p e b P'.p)
:
CategoryStruct.comp
(Limits.pullback.map (P.fstProj A) P.p (P'.fstProj A') P'.p
(CategoryStruct.comp ((P.cartesianNatTrans P' b e hp).app A) (P'.functor.map a)) e b ⋯ ⋯)
(PartialProduct.ε P' A') = CategoryStruct.comp (PartialProduct.ε P A) (Limits.prod.map e a)
def
CategoryTheory.UvPoly.Equiv.fst
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
:
Equations
- CategoryTheory.UvPoly.Equiv.fst P X pair = ((CategoryTheory.UvPoly.PartialProduct.fan P X).extend pair).fst
Instances For
theorem
CategoryTheory.UvPoly.Equiv.fst_eq
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
:
def
CategoryTheory.UvPoly.Equiv.snd
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
:
Equations
- CategoryTheory.UvPoly.Equiv.snd P X pair = ((CategoryTheory.UvPoly.PartialProduct.fan P X).extend pair).snd
Instances For
def
CategoryTheory.UvPoly.Equiv.snd'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g (fst P X pair) P.p)
:
Equations
- CategoryTheory.UvPoly.Equiv.snd' P X pair H = CategoryTheory.CategoryStruct.comp H.isoPullback.hom (CategoryTheory.UvPoly.Equiv.snd P X pair)
Instances For
theorem
CategoryTheory.UvPoly.Equiv.snd_eq_snd'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
:
def
CategoryTheory.UvPoly.Equiv.mk
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
(x : Limits.pullback b P.p ⟶ X)
:
Equations
- CategoryTheory.UvPoly.Equiv.mk P X b x = P.lift b x
Instances For
def
CategoryTheory.UvPoly.Equiv.mk'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g b P.p)
(x : R ⟶ X)
:
Equations
Instances For
theorem
CategoryTheory.UvPoly.Equiv.mk_eq_mk'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
(x : Limits.pullback b P.p ⟶ X)
:
@[simp]
theorem
CategoryTheory.UvPoly.Equiv.fst_mk
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
(x : Limits.pullback b P.p ⟶ X)
:
@[simp]
theorem
CategoryTheory.UvPoly.Equiv.fst_mk'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g b P.p)
(x : R ⟶ X)
:
@[simp]
theorem
CategoryTheory.UvPoly.Equiv.mk'_comp_fstProj
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g b P.p)
(x : R ⟶ X)
:
theorem
CategoryTheory.UvPoly.Equiv.fst_comp_left
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
{Δ : C}
(f : Δ ⟶ Γ)
:
theorem
CategoryTheory.UvPoly.Equiv.fst_comp_right
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X Y : C)
(f : X ⟶ Y)
(pair : Γ ⟶ P @ X)
:
theorem
CategoryTheory.UvPoly.Equiv.snd'_eq
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g (fst P X pair) P.p)
:
snd' P X pair H = CategoryStruct.comp (Limits.pullback.lift (CategoryStruct.comp f pair) g ⋯) (PartialProduct.fan P X).snd
theorem
CategoryTheory.UvPoly.Equiv.snd'_eq_snd'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g (fst P X pair) P.p)
{R' : C}
{f' : R' ⟶ Γ}
{g' : R' ⟶ E}
(H' : IsPullback f' g' (fst P X pair) P.p)
:
Switch the selected pullback R used in UvPoly.Equiv.snd' with a different pullback R'.
@[simp]
theorem
CategoryTheory.UvPoly.Equiv.snd'_mk'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g b P.p)
(x : R ⟶ X)
:
theorem
CategoryTheory.UvPoly.Equiv.snd_mk_heq
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
(x : Limits.pullback b P.p ⟶ X)
:
theorem
CategoryTheory.UvPoly.Equiv.snd_mk
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
(x : Limits.pullback b P.p ⟶ X)
:
theorem
CategoryTheory.UvPoly.Equiv.snd'_comp_left
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g (fst P X pair) P.p)
{Δ : C}
(σ : Δ ⟶ Γ)
{R' : C}
{f' : R' ⟶ Δ}
{g' : R' ⟶ E}
(H' : IsPullback f' g' (CategoryStruct.comp σ (fst P X pair)) P.p)
:
snd' P X (CategoryStruct.comp σ pair) ⋯ = CategoryStruct.comp (H.lift (CategoryStruct.comp f' σ) g' ⋯) (snd' P X pair H)
theorem
CategoryTheory.UvPoly.Equiv.snd'_comp_right
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X Y : C)
(f : X ⟶ Y)
(pair : Γ ⟶ P @ X)
{R : C}
{f1 : R ⟶ Γ}
{f2 : R ⟶ E}
(H : IsPullback f1 f2 (fst P X pair) P.p)
:
theorem
CategoryTheory.UvPoly.Equiv.snd_comp_right
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X Y : C)
(f : X ⟶ Y)
(pair : Γ ⟶ P @ X)
:
snd P Y (CategoryStruct.comp pair (P.functor.map f)) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (snd P X pair) f)
theorem
CategoryTheory.UvPoly.Equiv.ext'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
{pair₁ pair₂ : Γ ⟶ P @ X}
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g (fst P X pair₁) P.p)
(h1 : fst P X pair₁ = fst P X pair₂)
(h2 : snd' P X pair₁ H = snd' P X pair₂ ⋯)
:
theorem
CategoryTheory.UvPoly.Equiv.mk'_eq_mk'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g b P.p)
(x : R ⟶ X)
{R' : C}
{f' : R' ⟶ Γ}
{g' : R' ⟶ E}
(H' : IsPullback f' g' b P.p)
:
Switch the selected pullback R used in UvPoly.Equiv.mk' with a different pullback R'.
@[simp]
theorem
CategoryTheory.UvPoly.Equiv.eta'
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
{R : C}
{f1 : R ⟶ Γ}
{f2 : R ⟶ E}
(H : IsPullback f1 f2 (fst P X pair) P.p)
:
@[simp]
theorem
CategoryTheory.UvPoly.Equiv.eta
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
(pair : Γ ⟶ P @ X)
:
theorem
CategoryTheory.UvPoly.Equiv.mk'_comp_right
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X Y : C)
(f : X ⟶ Y)
(b : Γ ⟶ B)
{R : C}
{f1 : R ⟶ Γ}
{f2 : R ⟶ E}
(H : IsPullback f1 f2 b P.p)
(x : R ⟶ X)
:
theorem
CategoryTheory.UvPoly.Equiv.mk_comp_right
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X Y : C)
(f : X ⟶ Y)
(b : Γ ⟶ B)
(x : Limits.pullback b P.p ⟶ X)
:
theorem
CategoryTheory.UvPoly.Equiv.mk'_comp_left
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
{Δ : C}
(b : Γ ⟶ B)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ E}
(H : IsPullback f g b P.p)
(x : R ⟶ X)
(σ : Δ ⟶ Γ)
(σb : Δ ⟶ B)
(eq : CategoryStruct.comp σ b = σb)
{R' : C}
{f' : R' ⟶ Δ}
{g' : R' ⟶ E}
(H' : IsPullback f' g' σb P.p)
:
CategoryStruct.comp σ (mk' P X b H x) = mk' P X σb H' (CategoryStruct.comp (H.lift (CategoryStruct.comp f' σ) g' ⋯) x)
theorem
CategoryTheory.UvPoly.Equiv.mk_comp_left
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{Γ : C}
(X : C)
{Δ : C}
(b : Γ ⟶ B)
(x : Limits.pullback b P.p ⟶ X)
(σ : Δ ⟶ Γ)
:
CategoryStruct.comp σ (mk P X b x) = mk P X (CategoryStruct.comp σ b)
(CategoryStruct.comp
(Limits.pullback.map (CategoryStruct.comp σ b) P.p b P.p σ (CategoryStruct.id E) (CategoryStruct.id B) ⋯ ⋯) x)
theorem
CategoryTheory.UvPoly.Equiv.mk'_comp_cartesianNatTrans_app
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
(P : UvPoly E B)
{E' B' Γ X : C}
{P' : UvPoly E' B'}
(y : Γ ⟶ B)
(R : C)
(f : R ⟶ Γ)
(g : R ⟶ E)
(H : IsPullback f g y P.p)
(x : R ⟶ X)
(e : E ⟶ E')
(b : B ⟶ B')
(hp : IsPullback P.p e b P'.p)
:
CategoryStruct.comp (mk' P X y H x) ((P.cartesianNatTrans P' b e hp).app X) = mk' P' X (CategoryStruct.comp y b) ⋯ x
def
CategoryTheory.UvPoly.compDomEquiv
{𝒞 : Type u_1}
[Category.{u_2, u_1} 𝒞]
[Limits.HasTerminal 𝒞]
[Limits.HasPullbacks 𝒞]
{Γ E B D A : 𝒞}
{P : UvPoly E B}
{Q : UvPoly D A}
:
(Γ ⟶ P.compDom Q) ≃ (AB : Γ ⟶ P @ A) ×
(α : Γ ⟶ E) ×
(β : Γ ⟶ D) ×'
(w : CategoryStruct.comp AB (P.fstProj A) = CategoryStruct.comp α P.p) ×'
CategoryStruct.comp β Q.p = CategoryStruct.comp (Limits.pullback.lift AB α w) (PartialProduct.fan P A).snd
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.UvPoly.compP
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B D A : C}
(P : UvPoly E B)
(Q : UvPoly D A)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.UvPoly.compDomEquiv_symm_compP
{𝒞 : Type u_1}
[Category.{u_2, u_1} 𝒞]
[Limits.HasTerminal 𝒞]
[Limits.HasPullbacks 𝒞]
{Γ E B D A : 𝒞}
{P : UvPoly E B}
{Q : UvPoly D A}
(AB : Γ ⟶ P @ A)
(α : Γ ⟶ E)
(β : Γ ⟶ D)
(w : CategoryStruct.comp AB (P.fstProj A) = CategoryStruct.comp α P.p)
(h : CategoryStruct.comp β Q.p = CategoryStruct.comp (Limits.pullback.lift AB α w) (PartialProduct.fan P A).snd)
:
def
CategoryTheory.UvPoly.compDomMap
{𝒞 : Type u_1}
[Category.{u_2, u_1} 𝒞]
[Limits.HasTerminal 𝒞]
[Limits.HasPullbacks 𝒞]
{E B D A E' B' D' A' : 𝒞}
{P : UvPoly E B}
{Q : UvPoly D A}
{P' : UvPoly E' B'}
{Q' : UvPoly D' A'}
(e : E ⟶ E')
(d : D ⟶ D')
(b : B ⟶ B')
(a : A ⟶ A')
(hp : IsPullback P.p e b P'.p)
(hq : IsPullback Q.p d a Q'.p)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.UvPoly.compDomMap_isPullback
{𝒞 : Type u_1}
[Category.{u_2, u_1} 𝒞]
[Limits.HasTerminal 𝒞]
[Limits.HasPullbacks 𝒞]
{E B D A E' B' D' A' : 𝒞}
{P : UvPoly E B}
{Q : UvPoly D A}
{P' : UvPoly E' B'}
{Q' : UvPoly D' A'}
(e : E ⟶ E')
(d : D ⟶ D')
(b : B ⟶ B')
(a : A ⟶ A')
(hp : IsPullback P.p e b P'.p)
(hq : IsPullback Q.p d a Q'.p)
:
IsPullback (compDomMap e d b a hp hq) (P.compP Q) (P'.compP Q')
(CategoryStruct.comp ((P.cartesianNatTrans P' b e hp).app A) (P'.functor.map a))
theorem
CategoryTheory.UvPoly.fst_verticalNatTrans_app
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B F : C}
(P : UvPoly E B)
(Q : UvPoly F B)
(ρ : E ⟶ F)
(h : P.p = CategoryStruct.comp ρ Q.p)
{Γ : C}
(X : C)
(pair : Γ ⟶ Q @ X)
:
theorem
CategoryTheory.UvPoly.snd'_verticalNatTrans_app
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B F : C}
(P : UvPoly E B)
(Q : UvPoly F B)
(ρ : E ⟶ F)
(h : P.p = CategoryStruct.comp ρ Q.p)
{Γ : C}
(X : C)
(pair : Γ ⟶ Q @ X)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ F}
(H : IsPullback f g (Equiv.fst Q X pair) Q.p)
{R' : C}
{f' : R' ⟶ Γ}
{g' : R' ⟶ E}
(H' : IsPullback f' g' (Equiv.fst Q X pair) P.p)
:
Equiv.snd' P X (CategoryStruct.comp pair ((P.verticalNatTrans Q ρ h).app X)) ⋯ = CategoryStruct.comp (H.lift f' (CategoryStruct.comp g' ρ) ⋯) (Equiv.snd' Q X pair H)
theorem
CategoryTheory.UvPoly.mk'_comp_verticalNatTrans_app
{C : Type u}
[Category.{v, u} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B F : C}
(P : UvPoly E B)
(Q : UvPoly F B)
(ρ : E ⟶ F)
(h : P.p = CategoryStruct.comp ρ Q.p)
{Γ : C}
(X : C)
(b : Γ ⟶ B)
{R : C}
{f : R ⟶ Γ}
{g : R ⟶ F}
(H : IsPullback f g b Q.p)
(x : R ⟶ X)
{R' : C}
{f' : R' ⟶ Γ}
{g' : R' ⟶ E}
(H' : IsPullback f' g' b P.p)
:
CategoryStruct.comp (Equiv.mk' Q X b H x) ((P.verticalNatTrans Q ρ h).app X) = Equiv.mk' P X b H' (CategoryStruct.comp (H.lift f' (CategoryStruct.comp g' ρ) ⋯) x)
instance
CategoryTheory.UvPoly.preservesConnectedLimitsOfShape_of_hasLimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasPullbacks C]
[Limits.HasTerminal C]
{E B : C}
{J : Type v₁}
[SmallCategory J]
[IsConnected J]
[Limits.HasLimitsOfShape J C]
(P : UvPoly E B)
: