CategoryTheory.MorphismProperty.Under.congrPushoutIso
Pushout in relative under categories commutes with a compatible change of objects by isomorphisms.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u
open CategoryTheory Limits
namespace CategoryTheory.MorphismProperty
variable {A : Type*} [Category A]
{B : Type*} [Category B] {T : Type*} [Category T] {L L₁ L₂ L₃ : A ⥤ T} {P : MorphismProperty T}
{Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative]
{R R₁ R₂ R₃ : B ⥤ T}
variable (L)
variable {L} (R)
variable {C : Type*} [Category C] (P Q : MorphismProperty C) [Q.IsMultiplicative]Lean source · full declaration
def Under.congrPushoutIso [HasPushouts C] [P.IsStableUnderCobaseChange]
[Q.IsStableUnderCobaseChange] [Q.RespectsIso]
{X X' Y Y' : C} (f : X ⟶ Y) (f' : X' ⟶ Y') (eX : X ≅ X') (eY : Y ≅ Y')
(h : f ≫ eY.hom = eX.hom ≫ f') :
(Comma.mapLeftIso _ (Discrete.natIso fun _ ↦ eX)).functor ⋙ Under.pushout P Q f' ≅
Under.pushout P Q f ⋙
(Comma.mapLeftIso _ (Discrete.natIso fun _ ↦ eY)).functor :=
have h_inv : f' ≫ eY.inv = eX.inv ≫ f := by
rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp]
exact h.symm
have h_id (A : P.Under Q X) :
(eX.inv ≫ A.hom) ≫ (Iso.refl ((𝟭 C).obj A.right)).hom =
eX.inv ≫ A.hom := by
simp only [Iso.refl_hom, Category.comp_id]
NatIso.ofComponents
(fun A ↦
haveI : IsIso (Iso.refl ((𝟭 C).obj A.right)).hom := inferInstance
haveI : IsIso eY.inv := inferInstance
haveI : IsIso eX.inv := inferInstance
let k := pushout.map (eX.inv ≫ A.hom) f' A.hom f
(Iso.refl ((𝟭 C).obj A.right)).hom eY.inv eX.inv (h_id A) h_inv
have hk : IsIso k := by
dsimp only [k]
exact CategoryTheory.Limits.pushout.map_isIso (eX.inv ≫ A.hom) f' A.hom f
(Iso.refl ((𝟭 C).obj A.right)).hom eY.inv eX.inv (h_id A) h_inv
Under.isoMk
(@asIso C _ _ _ k hk)
(by
change pushout.inr (eX.inv ≫ A.hom) f' ≫ k =
eY.inv ≫ pushout.inr A.hom f
dsimp only [k, pushout.map]
apply pushout.inr_desc)) <|
fun {A B} g ↦ by
ext
let a : X ⟶ A.right := A.hom
let b : X ⟶ B.right := B.hom
let gr : A.right ⟶ B.right := g.right
have hgr : a ≫ gr = b := by
change A.hom ≫ g.right = B.hom
exact Under.w g
have ha_id :
(eX.inv ≫ a) ≫ (Iso.refl ((𝟭 C).obj A.right)).hom =
eX.inv ≫ a := by
change
(eX.inv ≫ A.hom) ≫ (Iso.refl ((𝟭 C).obj A.right)).hom =
eX.inv ≫ A.hom
exact h_id A
have hb_id :
(eX.inv ≫ b) ≫ (Iso.refl ((𝟭 C).obj B.right)).hom =
eX.inv ≫ b := by
change
(eX.inv ≫ B.hom) ≫ (Iso.refl ((𝟭 C).obj B.right)).hom =
eX.inv ≫ B.hom
exact h_id B
let s : Limits.pushout (eX.inv ≫ a) f' ⟶
Limits.pushout (eX.inv ≫ b) f' :=
pushout.desc
(gr ≫ pushout.inl (eX.inv ≫ b) f')
(pushout.inr (eX.inv ≫ b) f') (by
calc
(eX.inv ≫ a) ≫
(gr ≫ pushout.inl (eX.inv ≫ b) f') =
(eX.inv ≫ (a ≫ gr)) ≫
pushout.inl (eX.inv ≫ b) f' := by
simp only [Category.assoc]
_ = (eX.inv ≫ b) ≫
pushout.inl (eX.inv ≫ b) f' := by
rw [hgr]
_ = f' ≫ pushout.inr (eX.inv ≫ b) f' :=
pushout.condition)
let t : Limits.pushout a f ⟶ Limits.pushout b f :=
pushout.desc
(gr ≫ pushout.inl b f)
(pushout.inr b f) (by
calc
a ≫ (gr ≫ pushout.inl b f) =
(a ≫ gr) ≫ pushout.inl b f := by
simp only [Category.assoc]
_ = b ≫ pushout.inl b f := by rw [hgr]
_ = f ≫ pushout.inr b f := pushout.condition)
let kA : Limits.pushout (eX.inv ≫ a) f' ⟶ Limits.pushout a f :=
pushout.map (eX.inv ≫ a) f' a f
(Iso.refl ((𝟭 C).obj A.right)).hom eY.inv eX.inv
ha_id h_inv
let kB : Limits.pushout (eX.inv ≫ b) f' ⟶ Limits.pushout b f :=
pushout.map (eX.inv ≫ b) f' b f
(Iso.refl ((𝟭 C).obj B.right)).hom eY.inv eX.inv
hb_id h_inv
change s ≫ kB = kA ≫ t
have hs_inl :
pushout.inl (eX.inv ≫ a) f' ≫ s =
gr ≫ pushout.inl (eX.inv ≫ b) f' := by
exact pushout.inl_desc _ _ _
have hs_inr :
pushout.inr (eX.inv ≫ a) f' ≫ s =
pushout.inr (eX.inv ≫ b) f' := by
exact pushout.inr_desc _ _ _
have ht_inl :
pushout.inl a f ≫ t =
gr ≫ pushout.inl b f := by
exact pushout.inl_desc _ _ _
have ht_inr :
pushout.inr a f ≫ t =
pushout.inr b f := by
exact pushout.inr_desc _ _ _
have hkA_inl :
pushout.inl (eX.inv ≫ a) f' ≫ kA =
(Iso.refl ((𝟭 C).obj A.right)).hom ≫
pushout.inl a f := by
exact pushout.inl_desc _ _ _
have hkA_inr :
pushout.inr (eX.inv ≫ a) f' ≫ kA =
eY.inv ≫ pushout.inr a f := by
exact pushout.inr_desc _ _ _
have hkB_inl :
pushout.inl (eX.inv ≫ b) f' ≫ kB =
(Iso.refl ((𝟭 C).obj B.right)).hom ≫
pushout.inl b f := by
exact pushout.inl_desc _ _ _
have hkB_inr :
pushout.inr (eX.inv ≫ b) f' ≫ kB =
eY.inv ≫ pushout.inr b f := by
exact pushout.inr_desc _ _ _
have hkA_inl' :
pushout.inl (eX.inv ≫ a) f' ≫ kA =
pushout.inl a f := by
simpa only [Iso.refl_hom, Category.id_comp] using hkA_inl
have hkB_inl' :
pushout.inl (eX.inv ≫ b) f' ≫ kB =
pushout.inl b f := by
simpa only [Iso.refl_hom, Category.id_comp] using hkB_inl
apply pushout.hom_ext
· calc
pushout.inl (eX.inv ≫ a) f' ≫ (s ≫ kB) =
(pushout.inl (eX.inv ≫ a) f' ≫ s) ≫ kB :=
(Category.assoc _ _ _).symm
_ = (gr ≫ pushout.inl (eX.inv ≫ b) f') ≫ kB := by
rw [hs_inl]
_ = gr ≫
(pushout.inl (eX.inv ≫ b) f' ≫ kB) :=
Category.assoc _ _ _
_ = gr ≫ pushout.inl b f := by rw [hkB_inl']
_ = pushout.inl a f ≫ t := ht_inl.symm
_ = (pushout.inl (eX.inv ≫ a) f' ≫ kA) ≫ t := by
rw [hkA_inl']
_ = pushout.inl (eX.inv ≫ a) f' ≫ (kA ≫ t) :=
Category.assoc _ _ _
· calc
pushout.inr (eX.inv ≫ a) f' ≫ (s ≫ kB) =
(pushout.inr (eX.inv ≫ a) f' ≫ s) ≫ kB :=
(Category.assoc _ _ _).symm
_ = pushout.inr (eX.inv ≫ b) f' ≫ kB := by
rw [hs_inr]
_ = eY.inv ≫ pushout.inr b f := hkB_inr
_ = eY.inv ≫ (pushout.inr a f ≫ t) := by
rw [ht_inr]
_ = (eY.inv ≫ pushout.inr a f) ≫ t :=
(Category.assoc _ _ _).symm
_ = (pushout.inr (eX.inv ≫ a) f' ≫ kA) ≫ t := by
rw [hkA_inr]
_ = pushout.inr (eX.inv ≫ a) f' ≫ (kA ≫ t) :=
Category.assoc _ _ _