Lean4
/-- Transport an exact pairing across an isomorphism in the first argument. -/
def exactPairingCongrLeft {X X' Y : C} [ExactPairing X' Y] (i : X ≅ X') : ExactPairing X Y
where
evaluation' := Y ◁ i.hom ≫ ε_ _ _
coevaluation' := η_ _ _ ≫ i.inv ▷ Y
evaluation_coevaluation' :=
calc
_ = η_ X' Y ▷ X ⊗≫ (i.inv ▷ (Y ⊗ X) ≫ X ◁ (Y ◁ i.hom)) ⊗≫ X ◁ ε_ X' Y := by monoidal
_ = 𝟙 _ ⊗≫ (η_ X' Y ▷ X ≫ (X' ⊗ Y) ◁ i.hom) ⊗≫ (i.inv ▷ (Y ⊗ X') ≫ X ◁ ε_ X' Y) ⊗≫ 𝟙 _ := by
rw [← whisker_exchange]; monoidal
_ = 𝟙 _ ⊗≫ i.hom ⊗≫ (η_ X' Y ▷ X' ⊗≫ X' ◁ ε_ X' Y) ⊗≫ i.inv ⊗≫ 𝟙 _ := by
rw [← whisker_exchange, ← whisker_exchange]; monoidal
_ = 𝟙 _ ⊗≫ (i.hom ≫ i.inv) ⊗≫ 𝟙 _ := by rw [evaluation_coevaluation'']; monoidal
_ = (λ_ X).hom ≫ (ρ_ X).inv := by
rw [Iso.hom_inv_id]
monoidal
coevaluation_evaluation' := by
calc
_ = Y ◁ η_ X' Y ≫ Y ◁ (i.inv ≫ i.hom) ▷ Y ⊗≫ ε_ X' Y ▷ Y := by monoidal
_ = Y ◁ η_ X' Y ⊗≫ ε_ X' Y ▷ Y := by rw [Iso.inv_hom_id]; monoidal
_ = _ := by
rw [coevaluation_evaluation'']
simp
