Skip to content

Commit

Permalink
feat: forward port AlgebraicTopology.DoldKan.Compatibility (#6186)
Browse files Browse the repository at this point in the history 
This PR is a forward port of mathlib3 PR !3#17923



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
  • Loading branch information
@joelriou
joelriou and joelriou committed Jul 29, 2023
1 parent d8f6839 commit 2471abe
Showing 1 changed file with 112 additions and 14 deletions.
126 changes: 112 additions & 14 deletions Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
View file
Expand Up @@ -5,7 +5,7 @@ Authors: Joël Riou
-/
import Mathlib.CategoryTheory.Equivalence

#align_import algebraic_topology.dold_kan.compatibility from "leanprover-community/mathlib"@"160f568dcf772b2477791c844fc605f2f91f73d1"
#align_import algebraic_topology.dold_kan.compatibility from "leanprover-community/mathlib"@"18ee599842a5d17f189fe572f0ed8cb1d064d772"

/-! Tools for compatibilities between Dold-Kan equivalences
Expand Down Expand Up @@ -34,7 +34,7 @@ inverse of `eB`:
but whose inverse functor is `G`.
When extra assumptions are given, we shall also provide simplification lemmas for the
unit and counit isomorphisms of `equivalence`. (TODO)
unit and counit isomorphisms of `equivalence`.
-/

Expand Down Expand Up @@ -78,9 +78,9 @@ def equivalence₁CounitIso : (e'.inverse ⋙ eA.inverse) ⋙ F ≅ 𝟭 B' :=
calc
(e'.inverse ⋙ eA.inverse) ⋙ F ≅ (e'.inverse ⋙ eA.inverse) ⋙ eA.functor ⋙ e'.functor :=
isoWhiskerLeft _ hF.symm
_ ≅ e'.inverse ⋙ (eA.inverse ⋙ eA.functor) ⋙ e'.functor := (Iso.refl _)
_ ≅ e'.inverse ⋙ 𝟭 _ ⋙ e'.functor := (isoWhiskerLeft _ (isoWhiskerRight eA.counitIso _))
_ ≅ e'.inverse ⋙ e'.functor := (Iso.refl _)
_ ≅ e'.inverse ⋙ (eA.inverse ⋙ eA.functor) ⋙ e'.functor := Iso.refl _
_ ≅ e'.inverse ⋙ 𝟭 _ ⋙ e'.functor := isoWhiskerLeft _ (isoWhiskerRight eA.counitIso _)
_ ≅ e'.inverse ⋙ e'.functor := Iso.refl _
_ ≅ 𝟭 B' := e'.counitIso
#align algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso

Expand All @@ -97,10 +97,10 @@ theorem equivalence₁CounitIso_eq : (equivalence₁ hF).counitIso = equivalence
def equivalence₁UnitIso : 𝟭 A ≅ F ⋙ e'.inverse ⋙ eA.inverse :=
calc
𝟭 A ≅ eA.functor ⋙ eA.inverse := eA.unitIso
_ ≅ eA.functor ⋙ 𝟭 A' ⋙ eA.inverse := (Iso.refl _)
_ ≅ eA.functor ⋙ 𝟭 A' ⋙ eA.inverse := Iso.refl _
_ ≅ eA.functor ⋙ (e'.functor ⋙ e'.inverse) ⋙ eA.inverse :=
(isoWhiskerLeft _ (isoWhiskerRight e'.unitIso _))
_ ≅ (eA.functor ⋙ e'.functor) ⋙ e'.inverse ⋙ eA.inverse := (Iso.refl _)
isoWhiskerLeft _ (isoWhiskerRight e'.unitIso _)
_ ≅ (eA.functor ⋙ e'.functor) ⋙ e'.inverse ⋙ eA.inverse := Iso.refl _
_ ≅ F ⋙ e'.inverse ⋙ eA.inverse := isoWhiskerRight hF _
#align algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso

Expand Down Expand Up @@ -132,8 +132,8 @@ def equivalence₂CounitIso : (eB.functor ⋙ e'.inverse ⋙ eA.inverse) ⋙ F
eB.functor ⋙ (e'.inverse ⋙ eA.inverse ⋙ F) ⋙ eB.inverse :=
Iso.refl _
_ ≅ eB.functor ⋙ 𝟭 _ ⋙ eB.inverse :=
(isoWhiskerLeft _ (isoWhiskerRight (equivalence₁CounitIso hF) _))
_ ≅ eB.functor ⋙ eB.inverse := (Iso.refl _)
isoWhiskerLeft _ (isoWhiskerRight (equivalence₁CounitIso hF) _)
_ ≅ eB.functor ⋙ eB.inverse := Iso.refl _
_ ≅ 𝟭 B := eB.unitIso.symm
#align algebraic_topology.dold_kan.compatibility.equivalence₂_counit_iso AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso

Expand All @@ -150,9 +150,9 @@ theorem equivalence₂CounitIso_eq :
def equivalence₂UnitIso : 𝟭 A ≅ (F ⋙ eB.inverse) ⋙ eB.functor ⋙ e'.inverse ⋙ eA.inverse :=
calc
𝟭 A ≅ F ⋙ e'.inverse ⋙ eA.inverse := equivalence₁UnitIso hF
_ ≅ F ⋙ 𝟭 B' ⋙ e'.inverse ⋙ eA.inverse := (Iso.refl _)
_ ≅ F ⋙ 𝟭 B' ⋙ e'.inverse ⋙ eA.inverse := Iso.refl _
_ ≅ F ⋙ (eB.inverse ⋙ eB.functor) ⋙ e'.inverse ⋙ eA.inverse :=
(isoWhiskerLeft _ (isoWhiskerRight eB.counitIso.symm _))
isoWhiskerLeft _ (isoWhiskerRight eB.counitIso.symm _)
_ ≅ (F ⋙ eB.inverse) ⋙ eB.functor ⋙ e'.inverse ⋙ eA.inverse := Iso.refl _
#align algebraic_topology.dold_kan.compatibility.equivalence₂_unit_iso AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso

Expand All @@ -174,8 +174,8 @@ def equivalence : A ≌ B :=
refine' IsEquivalence.ofIso _ (IsEquivalence.ofEquivalence (equivalence₂ eB hF).symm)
calc
eB.functor ⋙ e'.inverse ⋙ eA.inverse ≅ (eB.functor ⋙ e'.inverse) ⋙ eA.inverse := Iso.refl _
_ ≅ (G ⋙ eA.functor) ⋙ eA.inverse := (isoWhiskerRight hG _)
_ ≅ G ⋙ 𝟭 A := (isoWhiskerLeft _ eA.unitIso.symm)
_ ≅ (G ⋙ eA.functor) ⋙ eA.inverse := isoWhiskerRight hG _
_ ≅ G ⋙ 𝟭 A := isoWhiskerLeft _ eA.unitIso.symm
_ ≅ G := Functor.rightUnitor G
G.asEquivalence.symm
#align algebraic_topology.dold_kan.compatibility.equivalence AlgebraicTopology.DoldKan.Compatibility.equivalence
Expand All @@ -184,6 +184,104 @@ theorem equivalence_functor : (equivalence hF hG).functor = F ⋙ eB.inverse :=
rfl
#align algebraic_topology.dold_kan.compatibility.equivalence_functor AlgebraicTopology.DoldKan.Compatibility.equivalence_functor

/-- The isomorphism `eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor` deduced
from the counit isomorphism of `e'`. -/
@[simps! hom_app]
def τ₀ : eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor :=
calc
eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor ⋙ 𝟭 _ := isoWhiskerLeft _ e'.counitIso
_ ≅ eB.functor := Functor.rightUnitor _
#align algebraic_topology.dold_kan.compatibility.τ₀ AlgebraicTopology.DoldKan.Compatibility.τ₀

/-- The isomorphism `eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor` deduced
from the isomorphisms `hF : eA.functor ⋙ e'.functor ≅ F`,
`hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor` and the datum of
an isomorphism `η : G ⋙ F ≅ eB.functor`. -/
@[simps! hom_app]
def τ₁ (η : G ⋙ F ≅ eB.functor) : eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor :=
calc
eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ (eB.functor ⋙ e'.inverse) ⋙ e'.functor :=
Iso.refl _
_ ≅ (G ⋙ eA.functor) ⋙ e'.functor := isoWhiskerRight hG _
_ ≅ G ⋙ eA.functor ⋙ e'.functor := by rfl
_ ≅ G ⋙ F := isoWhiskerLeft _ hF
_ ≅ eB.functor := η
#align algebraic_topology.dold_kan.compatibility.τ₁ AlgebraicTopology.DoldKan.Compatibility.τ₁

variable (η : G ⋙ F ≅ eB.functor) (hη : τ₀ = τ₁ hF hG η)

/-- The counit isomorphism of `equivalence`. -/
@[simps!]
def equivalenceCounitIso : G ⋙ F ⋙ eB.inverse ≅ 𝟭 B :=
calc
G ⋙ F ⋙ eB.inverse ≅ (G ⋙ F) ⋙ eB.inverse := Iso.refl _
_ ≅ eB.functor ⋙ eB.inverse := isoWhiskerRight η _
_ ≅ 𝟭 B := eB.unitIso.symm
#align algebraic_topology.dold_kan.compatibility.equivalence_counit_iso AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso

variable {η hF hG}

theorem equivalenceCounitIso_eq : (equivalence hF hG).counitIso = equivalenceCounitIso η := by
ext1; apply NatTrans.ext; ext Y
dsimp [equivalence, Functor.asEquivalence, IsEquivalence.ofEquivalence]
rw [equivalenceCounitIso_hom_app, IsEquivalence.ofIso_unitIso_inv_app]
dsimp
simp only [comp_id, id_comp, F.map_comp, assoc,
equivalence₂CounitIso_eq, equivalence₂CounitIso_hom_app,
← eB.inverse.map_comp_assoc, ← τ₀_hom_app, hη, τ₁_hom_app]
erw [hF.inv.naturality_assoc, hF.inv.naturality_assoc]
dsimp
congr 2
simp only [assoc, ← e'.functor.map_comp_assoc, Equivalence.fun_inv_map,
Iso.inv_hom_id_app_assoc, hG.inv_hom_id_app]
dsimp
rw [comp_id, eA.functor_unitIso_comp, e'.functor.map_id, id_comp, hF.inv_hom_id_app_assoc]
#align algebraic_topology.dold_kan.compatibility.equivalence_counit_iso_eq AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_eq

variable (hF)

/-- The isomorphism `eA.functor ≅ F ⋙ e'.inverse` deduced from the
unit isomorphism of `e'` and the isomorphism `hF : eA.functor ⋙ e'.functor ≅ F`. -/
@[simps!]
def υ : eA.functor ≅ F ⋙ e'.inverse :=
calc
eA.functor ≅ eA.functor ⋙ 𝟭 A' := (Functor.leftUnitor _).symm
_ ≅ eA.functor ⋙ e'.functor ⋙ e'.inverse := (isoWhiskerLeft _ e'.unitIso)
_ ≅ (eA.functor ⋙ e'.functor) ⋙ e'.inverse := Iso.refl _
_ ≅ F ⋙ e'.inverse := isoWhiskerRight hF _
#align algebraic_topology.dold_kan.compatibility.υ AlgebraicTopology.DoldKan.Compatibility.υ

variable (ε : eA.functor ≅ F ⋙ e'.inverse) (hε : υ hF = ε) (hG)

/-- The unit isomorphism of `equivalence`. -/
@[simps!]
def equivalenceUnitIso : 𝟭 A ≅ (F ⋙ eB.inverse) ⋙ G :=
calc
𝟭 A ≅ eA.functor ⋙ eA.inverse := eA.unitIso
_ ≅ (F ⋙ e'.inverse) ⋙ eA.inverse := isoWhiskerRight ε _
_ ≅ F ⋙ 𝟭 B' ⋙ e'.inverse ⋙ eA.inverse := Iso.refl _
_ ≅ F ⋙ (eB.inverse ⋙ eB.functor) ⋙ e'.inverse ⋙ eA.inverse :=
isoWhiskerLeft _ (isoWhiskerRight eB.counitIso.symm _)
_ ≅ (F ⋙ eB.inverse) ⋙ (eB.functor ⋙ e'.inverse) ⋙ eA.inverse := Iso.refl _
_ ≅ (F ⋙ eB.inverse) ⋙ (G ⋙ eA.functor) ⋙ eA.inverse :=
isoWhiskerLeft _ (isoWhiskerRight hG _)
_ ≅ (F ⋙ eB.inverse ⋙ G) ⋙ eA.functor ⋙ eA.inverse := Iso.refl _
_ ≅ (F ⋙ eB.inverse ⋙ G) ⋙ 𝟭 A := isoWhiskerLeft _ eA.unitIso.symm
_ ≅ (F ⋙ eB.inverse) ⋙ G := Iso.refl _
#align algebraic_topology.dold_kan.compatibility.equivalence_unit_iso AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso

variable {ε hF hG}

theorem equivalenceUnitIso_eq : (equivalence hF hG).unitIso = equivalenceUnitIso hG ε := by
ext1; apply NatTrans.ext; ext X
dsimp [equivalence, Functor.asEquivalence, IsEquivalence.ofEquivalence, IsEquivalence.inverse]
rw [IsEquivalence.ofIso_counitIso_inv_app]
dsimp
erw [id_comp, comp_id]
simp only [equivalence₂UnitIso_eq eB hF, equivalence₂UnitIso_hom_app,
assoc, equivalenceUnitIso_hom_app, ← eA.inverse.map_comp_assoc, ← hε, υ_hom_app]
#align algebraic_topology.dold_kan.compatibility.equivalence_unit_iso_eq AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_eq

end Compatibility

end DoldKan
Expand Down

0 comments on commit 2471abe

Please sign in to comment.