Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-28 19:49 8d24a1fe

View on Github →

refactor(category_theory/shift): make shifts more flexible (#10573)

Estimated changes

Modified src/algebra/homology/differential_object.lean

Modified src/category_theory/differential_object.lean

deleted def category_theory.differential_object.shift_counit

deleted def category_theory.differential_object.shift_counit_inv

deleted def category_theory.differential_object.shift_counit_iso

modified def category_theory.differential_object.shift_functor

added def category_theory.differential_object.shift_functor_add

deleted def category_theory.differential_object.shift_inverse

deleted def category_theory.differential_object.shift_inverse_obj

deleted def category_theory.differential_object.shift_unit

deleted def category_theory.differential_object.shift_unit_inv

deleted def category_theory.differential_object.shift_unit_iso

added def category_theory.differential_object.shift_ε

modified def category_theory.functor.map_differential_object

Modified src/category_theory/graded_object.lean

modified theorem category_theory.graded_object.shift_functor_obj_apply

Modified src/category_theory/shift.lean

added def category_theory.add_neg_equiv

added theorem category_theory.eq_to_hom_comp_shift_add_inv₁

added theorem category_theory.eq_to_hom_comp_shift_add_inv₁₂

added theorem category_theory.eq_to_hom_comp_shift_add_inv₂

added theorem category_theory.eq_to_hom_μ_app

added theorem category_theory.has_shift.shift_obj_obj

added def category_theory.has_shift_mk

added theorem category_theory.map_opaque_eq_to_iso_comp_app

added def category_theory.opaque_eq_to_iso

added theorem category_theory.opaque_eq_to_iso_inv

added theorem category_theory.opaque_eq_to_iso_symm

deleted def category_theory.shift

added def category_theory.shift_add

added theorem category_theory.shift_add_hom_comp_eq_to_hom₁

added theorem category_theory.shift_add_hom_comp_eq_to_hom₁₂

added theorem category_theory.shift_add_hom_comp_eq_to_hom₂

added theorem category_theory.shift_comm'

added def category_theory.shift_comm

added theorem category_theory.shift_comm_hom_comp

added theorem category_theory.shift_comm_symm

added def category_theory.shift_equiv

added theorem category_theory.shift_equiv_triangle

added def category_theory.shift_functor

added def category_theory.shift_functor_add

added def category_theory.shift_functor_comp_shift_functor_neg

added def category_theory.shift_functor_neg_comp_shift_functor

added def category_theory.shift_functor_zero

added structure category_theory.shift_mk_core

added def category_theory.shift_monoidal_functor

added theorem category_theory.shift_neg_shift'

added def category_theory.shift_neg_shift

added theorem category_theory.shift_shift'

added theorem category_theory.shift_shift_neg'

added def category_theory.shift_shift_neg

added theorem category_theory.shift_shift_neg_hom_shift

added theorem category_theory.shift_shift_neg_inv_shift

added theorem category_theory.shift_shift_neg_shift_eq

added theorem category_theory.shift_zero'

added def category_theory.shift_zero

modified theorem category_theory.shift_zero_eq_zero

added theorem category_theory.μ_inv_app_eq_to_hom

Modified src/category_theory/triangulated/basic.lean

Modified src/category_theory/triangulated/pretriangulated.lean

Modified src/category_theory/triangulated/rotate.lean

added def category_theory.triangulated.from_inv_rotate_rotate

added def category_theory.triangulated.from_rotate_inv_rotate

modified def category_theory.triangulated.inv_rot_comp_rot_hom

added def category_theory.triangulated.to_inv_rotate_rotate

added def category_theory.triangulated.to_rotate_inv_rotate