English
Let Φ be a LocalizerMorphism with HasRightResolutions. For any isomorphism e: Φ.functor ⋙ L₂ ≅ L₁ ⋙ F, Φ.IsRightDerivabilityStructure holds if and only if the TwoSquare GuitartExact e.hom holds.
Русский
Пусть Φ — локализирующий морфизм с свойством HasRightResolutions. Пусть e: Φ.functor ⋙ L₂ ≅ L₁ ⋙ F. Тогда Φ.IsRightDerivabilityStructure эквивалентно тому, что TwoSquare.GuitartExact e.hom выполняется.
LaTeX
$$$\Phi.HasRightResolutions \; \Rightarrow \Big(\Phi.IsRightDerivabilityStructure \iff TwoSquare.GuitartExact(e.g)\Big)$$$
Lean4
theorem isRightDerivabilityStructure_iff [Φ.HasRightResolutions] (e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F) :
Φ.IsRightDerivabilityStructure ↔ TwoSquare.GuitartExact e.hom :=
by
have : Φ.IsRightDerivabilityStructure ↔ TwoSquare.GuitartExact ((Φ.catCommSq W₁.Q W₂.Q).iso).hom :=
⟨fun h => h.guitartExact', fun h => ⟨inferInstance, h⟩⟩
rw [this]
let e' := (Φ.catCommSq W₁.Q W₂.Q).iso
let E₁ := Localization.uniq W₁.Q L₁ W₁
let E₂ := Localization.uniq W₂.Q L₂ W₂
let e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
let e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
let e'' : (Φ.functor ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
associator _ _ _ ≪≫ isoWhiskerLeft _ e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
let e''' : Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F := liftNatIso W₁.Q W₁ _ _ _ _ e''
have : TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom :=
by
ext X₁
rw [TwoSquare.vComp'_app, liftNatIso_hom, liftNatTrans_app]
simp only [Functor.comp_obj, Iso.trans_hom, isoWhiskerLeft_hom, isoWhiskerRight_hom, Iso.symm_hom,
NatTrans.comp_app, Functor.associator_hom_app, whiskerLeft_app, whiskerRight_app, id_comp, assoc, e'']
dsimp [Lifting.iso]
rw [F.map_id, id_comp, ← F.map_comp, Iso.inv_hom_id_app, F.map_id, comp_id, ← Functor.map_comp_assoc]
erw [show (CatCommSq.iso Φ.functor W₁.Q W₂.Q (localizedFunctor Φ W₁.Q W₂.Q)).hom = (Lifting.iso W₁.Q W₁ _ _).inv by
rfl,
Iso.inv_hom_id_app]
simp
rw [← TwoSquare.GuitartExact.vComp'_iff_of_equivalences e'.hom E₁ E₂ e''' e₁ e₂, this]
