diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean index 4d737d3983b4a..99456b4dc08ce 100644 --- a/Mathlib/CategoryTheory/Opposites.lean +++ b/Mathlib/CategoryTheory/Opposites.lean @@ -460,6 +460,20 @@ theorem unop_op {X Y : Cᵒᵖ} (f : X ≅ Y) : f.unop.op = f := by (ext; rfl) theorem op_unop {X Y : C} (f : X ≅ Y) : f.op.unop = f := by (ext; rfl) #align category_theory.iso.op_unop CategoryTheory.Iso.op_unop +section + +variable {D : Type*} [Category D] {F G : C ⥤ Dᵒᵖ} (e : F ≅ G) (X : C) + +@[reassoc (attr := simp)] +lemma unop_hom_inv_id_app : (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 _ := by + rw [← unop_comp, inv_hom_id_app, unop_id] + +@[reassoc (attr := simp)] +lemma unop_inv_hom_id_app : (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 _ := by + rw [← unop_comp, hom_inv_id_app, unop_id] + +end + end Iso namespace NatIso diff --git a/Mathlib/CategoryTheory/Preadditive/Basic.lean b/Mathlib/CategoryTheory/Preadditive/Basic.lean index ec594368f418c..08ce6bf132e14 100644 --- a/Mathlib/CategoryTheory/Preadditive/Basic.lean +++ b/Mathlib/CategoryTheory/Preadditive/Basic.lean @@ -443,6 +443,38 @@ theorem hasCoequalizers_of_hasCokernels [HasCokernels C] : HasCoequalizers C := end Equalizers +section + +variable {C : Type*} [Category C] [Preadditive C] {X Y : C} + +instance : SMul (Units ℤ) (X ≅ Y) where + smul a e := + { hom := (a : ℤ) • e.hom + inv := ((a⁻¹ : Units ℤ) : ℤ) • e.inv + hom_inv_id := by + simp only [comp_zsmul, zsmul_comp, smul_smul, Units.inv_mul, one_smul, e.hom_inv_id] + inv_hom_id := by + simp only [comp_zsmul, zsmul_comp, smul_smul, Units.mul_inv, one_smul, e.inv_hom_id] } + +@[simp] +lemma smul_iso_hom (a : Units ℤ) (e : X ≅ Y) : (a • e).hom = (a : ℤ) • e.hom := rfl + +@[simp] +lemma smul_iso_inv (a : Units ℤ) (e : X ≅ Y) : (a • e).inv = ((a⁻¹ : Units ℤ) : ℤ) • e.inv := rfl + +instance : Neg (X ≅ Y) where + neg e := + { hom := -e.hom + inv := -e.inv } + +@[simp] +lemma neg_iso_hom (e : X ≅ Y) : (-e).hom = -e.hom := rfl + +@[simp] +lemma neg_iso_inv (e : X ≅ Y) : (-e).inv = -e.inv := rfl + +end + end Preadditive end CategoryTheory diff --git a/Mathlib/CategoryTheory/Triangulated/Opposite.lean b/Mathlib/CategoryTheory/Triangulated/Opposite.lean index cbe47c7c1c0b7..6af5abb1100e8 100644 --- a/Mathlib/CategoryTheory/Triangulated/Opposite.lean +++ b/Mathlib/CategoryTheory/Triangulated/Opposite.lean @@ -150,6 +150,33 @@ noncomputable def opShiftFunctorEquivalence (n : ℤ) : Cᵒᵖ ≌ Cᵒᵖ wher ((shiftFunctorCompIsoId C (-n) n (neg_add_self n)).hom.app X.unop)⟦-n⟧' = 𝟙 _ rw [shift_shiftFunctorCompIsoId_neg_add_self_hom_app n X.unop, Iso.inv_hom_id_app]) +/-! The naturality of the unit and counit isomorphisms are restated in the following +lemmas so as to mitigate the need for `erw`. -/ + +@[reassoc (attr := simp)] +lemma opShiftFunctorEquivalence_unitIso_hom_naturality (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : + f ≫ (opShiftFunctorEquivalence C n).unitIso.hom.app Y = + (opShiftFunctorEquivalence C n).unitIso.hom.app X ≫ (f⟦n⟧').unop⟦n⟧'.op := + (opShiftFunctorEquivalence C n).unitIso.hom.naturality f + +@[reassoc (attr := simp)] +lemma opShiftFunctorEquivalence_unitIso_inv_naturality (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : + (f⟦n⟧').unop⟦n⟧'.op ≫ (opShiftFunctorEquivalence C n).unitIso.inv.app Y = + (opShiftFunctorEquivalence C n).unitIso.inv.app X ≫ f := + (opShiftFunctorEquivalence C n).unitIso.inv.naturality f + +@[reassoc (attr := simp)] +lemma opShiftFunctorEquivalence_counitIso_hom_naturality (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : + f.unop⟦n⟧'.op⟦n⟧' ≫ (opShiftFunctorEquivalence C n).counitIso.hom.app Y = + (opShiftFunctorEquivalence C n).counitIso.hom.app X ≫ f := + (opShiftFunctorEquivalence C n).counitIso.hom.naturality f + +@[reassoc (attr := simp)] +lemma opShiftFunctorEquivalence_counitIso_inv_naturality (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : + f ≫ (opShiftFunctorEquivalence C n).counitIso.inv.app Y = + (opShiftFunctorEquivalence C n).counitIso.inv.app X ≫ f.unop⟦n⟧'.op⟦n⟧' := + (opShiftFunctorEquivalence C n).counitIso.inv.naturality f + variable {C} lemma shift_unop_opShiftFunctorEquivalence_counitIso_inv_app (X : Cᵒᵖ) (n : ℤ) : @@ -191,8 +218,8 @@ noncomputable def functor : (Triangle C)ᵒᵖ ⥤ Triangle Cᵒᵖ where comm₂ := Quiver.Hom.unop_inj φ.unop.comm₁.symm comm₃ := by dsimp - rw [assoc, ← Functor.map_comp, ← op_comp, ← φ.unop.comm₃, op_comp, Functor.map_comp] - erw [(opShiftFunctorEquivalence C 1).counitIso.inv.naturality_assoc φ.unop.hom₁.op] + rw [assoc, ← Functor.map_comp, ← op_comp, ← φ.unop.comm₃, op_comp, Functor.map_comp, + opShiftFunctorEquivalence_counitIso_inv_naturality_assoc] rfl } /-- The functor which sends a triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` in `Cᵒᵖ` to the triangle @@ -205,34 +232,22 @@ noncomputable def inverse : Triangle Cᵒᵖ ⥤ (Triangle C)ᵒᵖ where { hom₁ := φ.hom₃.unop hom₂ := φ.hom₂.unop hom₃ := φ.hom₁.unop - comm₁ := Opposite.op_injective φ.comm₂.symm - comm₂ := Opposite.op_injective φ.comm₁.symm - comm₃ := by + comm₁ := Quiver.Hom.op_inj φ.comm₂.symm + comm₂ := Quiver.Hom.op_inj φ.comm₁.symm + comm₃ := Quiver.Hom.op_inj (by dsimp - rw [assoc, ← Functor.map_comp, ← unop_comp, ← φ.comm₃, unop_comp, Functor.map_comp, - ← unop_comp_assoc] - apply Quiver.Hom.op_inj - simp only [Opposite.op_unop, op_comp, Quiver.Hom.op_unop, assoc, - Opposite.unop_op, unop_comp] - erw [← (opShiftFunctorEquivalence C 1).unitIso.inv.naturality φ.hom₁] - rfl } + rw [assoc, ← opShiftFunctorEquivalence_unitIso_inv_naturality, + ← op_comp_assoc, ← Functor.map_comp, ← unop_comp, ← φ.comm₃, + unop_comp, Functor.map_comp, op_comp, assoc]) } /-- The unit isomorphism of the equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ` .-/ @[simps!] noncomputable def unitIso : 𝟭 _ ≅ functor C ⋙ inverse C := - NatIso.ofComponents (fun T => Iso.op (by - refine' Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) _ _ _ - · aesop_cat - · aesop_cat - · dsimp - simp only [Functor.map_comp, Functor.map_id, comp_id, id_comp] - erw [← (NatIso.unop (opShiftFunctorEquivalence C 1).unitIso).inv.naturality_assoc] - rw [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app (Opposite.op T.unop.obj₁) 1] - dsimp - rw [← unop_comp, Iso.hom_inv_id_app] - dsimp - rw [comp_id])) + NatIso.ofComponents (fun T => Iso.op + (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat) + (Quiver.Hom.op_inj + (by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app])))) (fun {T₁ T₂} f => Quiver.Hom.unop_inj (by aesop_cat)) /-- The counit isomorphism of the @@ -244,10 +259,11 @@ noncomputable def counitIso : inverse C ⋙ functor C ≅ 𝟭 _ := · aesop_cat · aesop_cat · dsimp - rw [Functor.map_id, comp_id, id_comp, Functor.map_comp] - erw [← (opShiftFunctorEquivalence C 1).counitIso.inv.naturality_assoc T.mor₃] - simp only [opShiftFunctorEquivalence_counitIso_inv_app_shift, ← Functor.map_comp, - Iso.hom_inv_id_app, Functor.map_id, Functor.id_obj, comp_id, Functor.id_map]) + rw [Functor.map_id, comp_id, id_comp, Functor.map_comp, + ← opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, + opShiftFunctorEquivalence_counitIso_inv_app_shift, ← Functor.map_comp, + Iso.hom_inv_id_app, Functor.map_id] + simp only [Functor.id_obj, comp_id]) (by aesop_cat) end TriangleOpEquivalence @@ -300,8 +316,107 @@ lemma isomorphic_distinguished (T₁ : Triangle Cᵒᵖ) exact Pretriangulated.isomorphic_distinguished _ hT₁ _ ((triangleOpEquivalence C).inverse.mapIso e).unop.symm +/-- Up to rotation, the contractible triangle `X ⟶ X ⟶ 0 ⟶ X⟦1⟧` for `X : Cᵒᵖ` corresponds +to the contractible triangle for `X.unop` in `C`. -/ +@[simps!] +noncomputable def contractibleTriangleIso (X : Cᵒᵖ) : + contractibleTriangle X ≅ (triangleOpEquivalence C).functor.obj + (Opposite.op (contractibleTriangle X.unop).invRotate) := + Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) + (IsZero.iso (isZero_zero _) (by + dsimp + rw [IsZero.iff_id_eq_zero] + change (𝟙 ((0 : C)⟦(-1 : ℤ)⟧)).op = 0 + rw [← Functor.map_id, id_zero, Functor.map_zero, op_zero])) + (by aesop_cat) (by aesop_cat) (by aesop_cat) + +lemma contractible_distinguished (X : Cᵒᵖ) : + contractibleTriangle X ∈ distinguishedTriangles C := by + rw [mem_distinguishedTriangles_iff'] + exact ⟨_, inv_rot_of_distTriang _ (Pretriangulated.contractible_distinguished X.unop), + ⟨contractibleTriangleIso X⟩⟩ + +/-- Isomorphism expressing a compatibility of the equivalence `triangleOpEquivalence C` +with the rotation of triangles. -/ +noncomputable def rotateTriangleOpEquivalenceInverseObjRotateUnopIso (T : Triangle Cᵒᵖ) : + ((triangleOpEquivalence C).inverse.obj T.rotate).unop.rotate ≅ + ((triangleOpEquivalence C).inverse.obj T).unop := + Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) + (-((opShiftFunctorEquivalence C 1).unitIso.app T.obj₁).unop) (by simp) + (Quiver.Hom.op_inj (by aesop_cat)) (by aesop_cat) + +lemma rotate_distinguished_triangle (T : Triangle Cᵒᵖ) : + T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C := by + simp only [mem_distinguishedTriangles_iff, Pretriangulated.rotate_distinguished_triangle + ((triangleOpEquivalence C).inverse.obj (T.rotate)).unop] + exact distinguished_iff_of_iso (rotateTriangleOpEquivalenceInverseObjRotateUnopIso T).symm + +lemma distinguished_cocone_triangle {X Y : Cᵒᵖ} (f : X ⟶ Y) : + ∃ (Z : Cᵒᵖ) (g : Y ⟶ Z) (h : Z ⟶ X⟦(1 : ℤ)⟧), + Triangle.mk f g h ∈ distinguishedTriangles C := by + obtain ⟨Z, g, h, H⟩ := Pretriangulated.distinguished_cocone_triangle₁ f.unop + refine' ⟨_, g.op, (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫ + (shiftFunctor Cᵒᵖ (1 : ℤ)).map h.op, _⟩ + simp only [mem_distinguishedTriangles_iff] + refine' Pretriangulated.isomorphic_distinguished _ H _ _ + exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat) + (Quiver.Hom.op_inj (by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app])) + +lemma complete_distinguished_triangle_morphism (T₁ T₂ : Triangle Cᵒᵖ) + (hT₁ : T₁ ∈ distinguishedTriangles C) (hT₂ : T₂ ∈ distinguishedTriangles C) + (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁) : + ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ + T₁.mor₃ ≫ a⟦1⟧' = c ≫ T₂.mor₃ := by + rw [mem_distinguishedTriangles_iff] at hT₁ hT₂ + obtain ⟨c, hc₁, hc₂⟩ := + Pretriangulated.complete_distinguished_triangle_morphism₁ _ _ hT₂ hT₁ + b.unop a.unop (Quiver.Hom.op_inj comm.symm) + dsimp at c hc₁ hc₂ + replace hc₂ := ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫= hc₂ + dsimp at hc₂ + simp only [assoc, Iso.unop_hom_inv_id_app_assoc] at hc₂ + refine' ⟨c.op, Quiver.Hom.unop_inj hc₁.symm, Quiver.Hom.unop_inj _⟩ + apply (shiftFunctor C (1 : ℤ)).map_injective + rw [unop_comp, unop_comp, Functor.map_comp, Functor.map_comp, + Quiver.Hom.unop_op, hc₂, ← unop_comp_assoc, ← unop_comp_assoc, + ← opShiftFunctorEquivalence_unitIso_inv_naturality] + simp + +/-- The pretriangulated structure on the opposite category of +a pretriangulated category. It is a scoped instance, so that we need to +`open CategoryTheory.Pretriangulated.Opposite` in order to be able +to use it: the reason is that it relies on the definition of the shift +on the opposite category `Cᵒᵖ`, for which it is unclear whether it should +be a global instance or not. -/ +scoped instance : Pretriangulated Cᵒᵖ where + distinguishedTriangles := distinguishedTriangles C + isomorphic_distinguished := isomorphic_distinguished + contractible_distinguished := contractible_distinguished + distinguished_cocone_triangle := distinguished_cocone_triangle + rotate_distinguished_triangle := rotate_distinguished_triangle + complete_distinguished_triangle_morphism := complete_distinguished_triangle_morphism + end Opposite +variable {C} + +lemma mem_distTriang_op_iff (T : Triangle Cᵒᵖ) : + (T ∈ distTriang Cᵒᵖ) ↔ ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C := by + rfl + +lemma mem_distTriang_op_iff' (T : Triangle Cᵒᵖ) : + (T ∈ distTriang Cᵒᵖ) ↔ ∃ (T' : Triangle C) (_ : T' ∈ distTriang C), + Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T')) := + Opposite.mem_distinguishedTriangles_iff' T + +lemma op_distinguished (T : Triangle C) (hT : T ∈ distTriang C) : + ((triangleOpEquivalence C).functor.obj (Opposite.op T)) ∈ distTriang Cᵒᵖ := by + rw [mem_distTriang_op_iff'] + exact ⟨T, hT, ⟨Iso.refl _⟩⟩ + +lemma unop_distinguished (T : Triangle Cᵒᵖ) (hT : T ∈ distTriang Cᵒᵖ) : + ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C := hT + end Pretriangulated end CategoryTheory