From 0f286b04de42e2980e8a0dcc5c71172b8b948028 Mon Sep 17 00:00:00 2001 From: Jason Yuen <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 13 Jun 2023 23:55:50 +0000 Subject: [PATCH] feat: port CategoryTheory.DifferentialObject (#4020) Co-authored-by: int-y1 Co-authored-by: Jujian Zhang Co-authored-by: Scott Morrison --- Mathlib.lean | 1 + .../CategoryTheory/DifferentialObject.lean | 328 ++++++++++++++++++ 2 files changed, 329 insertions(+) create mode 100644 Mathlib/CategoryTheory/DifferentialObject.lean diff --git a/Mathlib.lean b/Mathlib.lean index ebb316fd988f5..c04d7f7514449 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -799,6 +799,7 @@ import Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom import Mathlib.CategoryTheory.Conj import Mathlib.CategoryTheory.ConnectedComponents import Mathlib.CategoryTheory.Core +import Mathlib.CategoryTheory.DifferentialObject import Mathlib.CategoryTheory.DiscreteCategory import Mathlib.CategoryTheory.Elements import Mathlib.CategoryTheory.Elementwise diff --git a/Mathlib/CategoryTheory/DifferentialObject.lean b/Mathlib/CategoryTheory/DifferentialObject.lean new file mode 100644 index 0000000000000..26f7ba935a799 --- /dev/null +++ b/Mathlib/CategoryTheory/DifferentialObject.lean @@ -0,0 +1,328 @@ +/- +Copyright (c) 2020 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison + +! This file was ported from Lean 3 source module category_theory.differential_object +! leanprover-community/mathlib commit 6876fa15e3158ff3e4a4e2af1fb6e1945c6e8803 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Data.Int.Basic +import Mathlib.CategoryTheory.Shift.Basic +import Mathlib.CategoryTheory.ConcreteCategory.Basic + +/-! +# Differential objects in a category. + +A differential object in a category with zero morphisms and a shift is +an object `X` equipped with +a morphism `d : obj ⟶ obj⟦1⟧`, such that `d^2 = 0`. + +We build the category of differential objects, and some basic constructions +such as the forgetful functor, zero morphisms and zero objects, and the shift functor +on differential objects. +-/ + + +open CategoryTheory.Limits + +universe v u + +namespace CategoryTheory + +variable (C : Type u) [Category.{v} C] + +-- TODO: generalize to `HasShift C A` for an arbitrary `[AddMonoid A]` `[One A]`. +variable [HasZeroMorphisms C] [HasShift C ℤ] + +/-- A differential object in a category with zero morphisms and a shift is +an object `obj` equipped with +a morphism `d : obj ⟶ obj⟦1⟧`, such that `d^2 = 0`. -/ +-- Porting note: Removed `@[nolint has_nonempty_instance]` +structure DifferentialObject where + /-- The underlying object of a differential object. -/ + obj : C + /-- The differential of a differential object. -/ + d : obj ⟶ obj⟦(1 : ℤ)⟧ + /-- The differential `d` satisfies that `d² = 0`. -/ + d_squared : d ≫ d⟦(1 : ℤ)⟧' = 0 := by aesop_cat +#align category_theory.differential_object CategoryTheory.DifferentialObject + +attribute [simp] DifferentialObject.d_squared + +variable {C} + +namespace DifferentialObject + +/-- A morphism of differential objects is a morphism commuting with the differentials. -/ +@[ext] -- Porting note: Removed `nolint has_nonempty_instance` +structure Hom (X Y : DifferentialObject C) where + /-- The morphism between underlying objects of the two differentiable objects. -/ + f : X.obj ⟶ Y.obj + comm : X.d ≫ f⟦1⟧' = f ≫ Y.d := by aesop_cat +#align category_theory.differential_object.hom CategoryTheory.DifferentialObject.Hom + +attribute [reassoc (attr := simp)] Hom.comm + +namespace Hom + +/-- The identity morphism of a differential object. -/ +@[simps] +def id (X : DifferentialObject C) : Hom X X where + f := 𝟙 X.obj +#align category_theory.differential_object.hom.id CategoryTheory.DifferentialObject.Hom.id + +/-- The composition of morphisms of differential objects. -/ +@[simps] +def comp {X Y Z : DifferentialObject C} (f : Hom X Y) (g : Hom Y Z) : Hom X Z where + f := f.f ≫ g.f +#align category_theory.differential_object.hom.comp CategoryTheory.DifferentialObject.Hom.comp + +end Hom + +instance categoryOfDifferentialObjects : Category (DifferentialObject C) where + Hom := Hom + id := Hom.id + comp f g := Hom.comp f g +#align category_theory.differential_object.category_of_differential_objects CategoryTheory.DifferentialObject.categoryOfDifferentialObjects + +-- Porting note: added +@[ext] +theorem ext {A B : DifferentialObject C} {f g : A ⟶ B} (w : f.f = g.f := by aesop_cat) : f = g := + Hom.ext _ _ w + +@[simp] +theorem id_f (X : DifferentialObject C) : (𝟙 X : X ⟶ X).f = 𝟙 X.obj := rfl +#align category_theory.differential_object.id_f CategoryTheory.DifferentialObject.id_f + +@[simp] +theorem comp_f {X Y Z : DifferentialObject C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).f = f.f ≫ g.f := rfl +#align category_theory.differential_object.comp_f CategoryTheory.DifferentialObject.comp_f + +@[simp] +theorem eqToHom_f {X Y : DifferentialObject C} (h : X = Y) : + Hom.f (eqToHom h) = eqToHom (congr_arg _ h) := by + subst h + rw [eqToHom_refl, eqToHom_refl] + rfl +#align category_theory.differential_object.eq_to_hom_f CategoryTheory.DifferentialObject.eqToHom_f + +variable (C) + +/-- The forgetful functor taking a differential object to its underlying object. -/ +def forget : DifferentialObject C ⥤ C where + obj X := X.obj + map f := f.f +#align category_theory.differential_object.forget CategoryTheory.DifferentialObject.forget + +instance forget_faithful : Faithful (forget C) where +#align category_theory.differential_object.forget_faithful CategoryTheory.DifferentialObject.forget_faithful + +instance {X Y : DifferentialObject C} : Zero (X ⟶ Y) := ⟨{f := 0}⟩ + +variable {C} + +@[simp] +theorem zero_f (P Q : DifferentialObject C) : (0 : P ⟶ Q).f = 0 := rfl +#align category_theory.differential_object.zero_f CategoryTheory.DifferentialObject.zero_f + +instance hasZeroMorphisms : HasZeroMorphisms (DifferentialObject C) where +#align category_theory.differential_object.has_zero_morphisms CategoryTheory.DifferentialObject.hasZeroMorphisms + +/-- An isomorphism of differential objects gives an isomorphism of the underlying objects. -/ +@[simps] +def isoApp {X Y : DifferentialObject C} (f : X ≅ Y) : X.obj ≅ Y.obj where + hom := f.hom.f + inv := f.inv.f + hom_inv_id := by dsimp; rw [← comp_f, Iso.hom_inv_id, id_f] + inv_hom_id := by dsimp; rw [← comp_f, Iso.inv_hom_id, id_f] +#align category_theory.differential_object.iso_app CategoryTheory.DifferentialObject.isoApp + +@[simp] +theorem isoApp_refl (X : DifferentialObject C) : isoApp (Iso.refl X) = Iso.refl X.obj := rfl +#align category_theory.differential_object.iso_app_refl CategoryTheory.DifferentialObject.isoApp_refl + +@[simp] +theorem isoApp_symm {X Y : DifferentialObject C} (f : X ≅ Y) : isoApp f.symm = (isoApp f).symm := + rfl +#align category_theory.differential_object.iso_app_symm CategoryTheory.DifferentialObject.isoApp_symm + +@[simp] +theorem isoApp_trans {X Y Z : DifferentialObject C} (f : X ≅ Y) (g : Y ≅ Z) : + isoApp (f ≪≫ g) = isoApp f ≪≫ isoApp g := rfl +#align category_theory.differential_object.iso_app_trans CategoryTheory.DifferentialObject.isoApp_trans + +/-- An isomorphism of differential objects can be constructed +from an isomorphism of the underlying objects that commutes with the differentials. -/ +@[simps] +def mkIso {X Y : DifferentialObject C} (f : X.obj ≅ Y.obj) (hf : X.d ≫ f.hom⟦1⟧' = f.hom ≫ Y.d) : + X ≅ Y where + hom := ⟨f.hom, hf⟩ + inv := ⟨f.inv, by + dsimp + rw [← Functor.mapIso_inv, Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, Functor.mapIso_hom, + hf]⟩ + hom_inv_id := by ext1; dsimp; exact f.hom_inv_id + inv_hom_id := by ext1; dsimp; exact f.inv_hom_id +#align category_theory.differential_object.mk_iso CategoryTheory.DifferentialObject.mkIso + +end DifferentialObject + +namespace Functor + +universe v' u' + +variable (D : Type u') [Category.{v'} D] + +variable [HasZeroMorphisms D] [HasShift D ℤ] + +/-- A functor `F : C ⥤ D` which commutes with shift functors on `C` and `D` and preserves zero +morphisms can be lifted to a functor `DifferentialObject C ⥤ DifferentialObject D`. -/ +@[simps] +def mapDifferentialObject (F : C ⥤ D) + (η : (shiftFunctor C (1 : ℤ)).comp F ⟶ F.comp (shiftFunctor D (1 : ℤ))) + (hF : ∀ c c', F.map (0 : c ⟶ c') = 0) : DifferentialObject C ⥤ DifferentialObject D where + obj X := + { obj := F.obj X.obj + d := F.map X.d ≫ η.app X.obj + d_squared := by + rw [Functor.map_comp, ← Functor.comp_map F (shiftFunctor D (1 : ℤ))] + slice_lhs 2 3 => rw [← η.naturality X.d] + rw [Functor.comp_map] + slice_lhs 1 2 => rw [← F.map_comp, X.d_squared, hF] + rw [zero_comp, zero_comp] } + map f := + { f := F.map f.f + comm := by + dsimp + slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : ℤ)), ← η.naturality f.f] + slice_lhs 1 2 => rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp] + rw [Category.assoc] } + map_id := by intros; ext; simp + map_comp := by intros; ext; simp +#align category_theory.functor.map_differential_object CategoryTheory.Functor.mapDifferentialObject + +end Functor + +end CategoryTheory + +namespace CategoryTheory + +namespace DifferentialObject + +variable (C : Type u) [Category.{v} C] + +variable [HasZeroObject C] [HasZeroMorphisms C] [HasShift C ℤ] + +open scoped ZeroObject + +instance hasZeroObject : HasZeroObject (DifferentialObject C) := by + -- Porting note(https://github.com/leanprover-community/mathlib4/issues/4998): added `aesop_cat` + -- Porting note: added `simp only [eq_iff_true_of_subsingleton]` + refine' ⟨⟨⟨0, 0, by aesop_cat⟩, fun X => ⟨⟨⟨⟨0, by aesop_cat⟩⟩, fun f => _⟩⟩, + fun X => ⟨⟨⟨⟨0, by aesop_cat⟩⟩, fun f => _⟩⟩⟩⟩ <;> ext <;> + simp only [eq_iff_true_of_subsingleton] +#align category_theory.differential_object.has_zero_object CategoryTheory.DifferentialObject.hasZeroObject + +end DifferentialObject + +namespace DifferentialObject + +variable (C : Type (u + 1)) [LargeCategory C] [ConcreteCategory C] [HasZeroMorphisms C] + [HasShift C ℤ] + +instance concreteCategoryOfDifferentialObjects : ConcreteCategory (DifferentialObject C) where + forget := forget C ⋙ CategoryTheory.forget C +#align category_theory.differential_object.concrete_category_of_differential_objects CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects + +instance : HasForget₂ (DifferentialObject C) C where + forget₂ := forget C + +end DifferentialObject + +/-! The category of differential objects itself has a shift functor. -/ + + +namespace DifferentialObject + +variable (C : Type u) [Category.{v} C] + +variable [HasZeroMorphisms C] [HasShift C ℤ] + +noncomputable section + +/-- The shift functor on `DifferentialObject C`. -/ +@[simps] +def shiftFunctor (n : ℤ) : DifferentialObject C ⥤ DifferentialObject C where + obj X := + { obj := X.obj⟦n⟧ + d := X.d⟦n⟧' ≫ (shiftComm _ _ _).hom + d_squared := by + rw [Functor.map_comp, Category.assoc, shiftComm_hom_comp_assoc, ← Functor.map_comp_assoc, + X.d_squared, Functor.map_zero, zero_comp] } + map f := + { f := f.f⟦n⟧' + comm := by + dsimp + erw [Category.assoc, shiftComm_hom_comp, ← Functor.map_comp_assoc, f.comm, + Functor.map_comp_assoc] + rfl } + map_id X := by ext1; dsimp; rw [Functor.map_id] + map_comp f g := by ext1; dsimp; rw [Functor.map_comp] +#align category_theory.differential_object.shift_functor CategoryTheory.DifferentialObject.shiftFunctor + +/-- The shift functor on `DifferentialObject C` is additive. -/ +@[simps!] +nonrec def shiftFunctorAdd (m n : ℤ) : + shiftFunctor C (m + n) ≅ shiftFunctor C m ⋙ shiftFunctor C n := by + refine' NatIso.ofComponents (fun X => mkIso (shiftAdd X.obj _ _) _) (fun f => _) + · dsimp + rw [← cancel_epi ((shiftFunctorAdd C m n).inv.app X.obj)] + simp only [Category.assoc, Iso.inv_hom_id_app_assoc] + erw [← NatTrans.naturality_assoc] + dsimp + simp only [Functor.map_comp, Category.assoc, + shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app 1 m n X.obj, + Iso.inv_hom_id_app_assoc] + · ext; dsimp; exact NatTrans.naturality _ _ +#align category_theory.differential_object.shift_functor_add CategoryTheory.DifferentialObject.shiftFunctorAdd + +section + +/-- The shift by zero is naturally isomorphic to the identity. -/ +@[simps!] +def shiftZero : shiftFunctor C 0 ≅ 𝟭 (DifferentialObject C) := by + refine' NatIso.ofComponents (fun X => mkIso ((shiftFunctorZero C ℤ).app X.obj) _) (fun f => _) + · erw [← NatTrans.naturality] + dsimp + simp only [shiftFunctorZero_hom_app_shift, Category.assoc] + · aesop_cat +#align category_theory.differential_object.shift_zero CategoryTheory.DifferentialObject.shiftZero + +end + +instance : HasShift (DifferentialObject C) ℤ := + hasShiftMk _ _ + { F := shiftFunctor C + zero := shiftZero C + add := shiftFunctorAdd C + assoc_hom_app := fun m₁ m₂ m₃ X => by + ext1 + convert shiftFunctorAdd_assoc_hom_app m₁ m₂ m₃ X.obj + dsimp [shiftFunctorAdd'] + simp + zero_add_hom_app := fun n X => by + ext1 + convert shiftFunctorAdd_zero_add_hom_app n X.obj + simp + add_zero_hom_app := fun n X => by + ext1 + convert shiftFunctorAdd_add_zero_hom_app n X.obj + simp } + +end + +end DifferentialObject + +end CategoryTheory