Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-28 23:45 6876fa15

View on Github →

refactor(category_theory/shift): improve automation (#18670)

Estimated changes

Modified src/category_theory/differential_object.lean

added def category_theory.differential_object.shift_zero

deleted def category_theory.differential_object.shift_ε

Modified src/category_theory/graded_object.lean

Deleted src/category_theory/shift.lean

deleted def category_theory.add_neg_equiv

deleted theorem category_theory.eq_to_hom_comp_shift_add_inv₁

deleted theorem category_theory.eq_to_hom_comp_shift_add_inv₁₂

deleted theorem category_theory.eq_to_hom_comp_shift_add_inv₂

deleted theorem category_theory.eq_to_hom_μ_app

deleted theorem category_theory.has_shift.shift_obj_obj

deleted def category_theory.has_shift_mk

deleted def category_theory.has_shift_of_fully_faithful

deleted def category_theory.has_shift_of_fully_faithful_comm

deleted def category_theory.shift_add

deleted theorem category_theory.shift_add_hom_comp_eq_to_hom₁

deleted theorem category_theory.shift_add_hom_comp_eq_to_hom₁₂

deleted theorem category_theory.shift_add_hom_comp_eq_to_hom₂

deleted theorem category_theory.shift_comm'

deleted def category_theory.shift_comm

deleted theorem category_theory.shift_comm_hom_comp

deleted theorem category_theory.shift_comm_symm

deleted def category_theory.shift_equiv

deleted theorem category_theory.shift_equiv_triangle

deleted def category_theory.shift_functor

deleted def category_theory.shift_functor_add

deleted def category_theory.shift_functor_comp_shift_functor_neg

deleted theorem category_theory.shift_functor_inv

deleted def category_theory.shift_functor_neg_comp_shift_functor

deleted def category_theory.shift_functor_zero

deleted structure category_theory.shift_mk_core

deleted def category_theory.shift_monoidal_functor

deleted theorem category_theory.shift_neg_shift'

deleted def category_theory.shift_neg_shift

deleted theorem category_theory.shift_shift'

deleted theorem category_theory.shift_shift_neg'

deleted def category_theory.shift_shift_neg

deleted theorem category_theory.shift_shift_neg_hom_shift

deleted theorem category_theory.shift_shift_neg_inv_shift

deleted theorem category_theory.shift_shift_neg_shift_eq

deleted theorem category_theory.shift_zero'

deleted def category_theory.shift_zero

deleted theorem category_theory.shift_zero_eq_zero

deleted theorem category_theory.μ_inv_app_eq_to_hom

Created src/category_theory/shift/basic.lean

added theorem category_theory.has_shift.shift_obj_obj

added def category_theory.has_shift_mk

added def category_theory.has_shift_of_fully_faithful

added def category_theory.has_shift_of_fully_faithful_add

added def category_theory.has_shift_of_fully_faithful_zero

added theorem category_theory.map_has_shift_of_fully_faithful_add_hom_app

added theorem category_theory.map_has_shift_of_fully_faithful_add_inv_app

added theorem category_theory.map_has_shift_of_fully_faithful_zero_hom_app

added theorem category_theory.map_has_shift_of_fully_faithful_zero_inv_app

added def category_theory.shift_add

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 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 theorem category_theory.shift_functor_add'_add_zero

added theorem category_theory.shift_functor_add'_add_zero_hom_app

added theorem category_theory.shift_functor_add'_add_zero_inv_app

added theorem category_theory.shift_functor_add'_assoc

added theorem category_theory.shift_functor_add'_assoc_hom_app

added theorem category_theory.shift_functor_add'_assoc_inv_app

added theorem category_theory.shift_functor_add'_eq_shift_functor_add

added theorem category_theory.shift_functor_add'_zero_add

added theorem category_theory.shift_functor_add'_zero_add_hom_app

added theorem category_theory.shift_functor_add'_zero_add_inv_app

added def category_theory.shift_functor_add

added theorem category_theory.shift_functor_add_add_zero_hom_app

added theorem category_theory.shift_functor_add_add_zero_inv_app

added theorem category_theory.shift_functor_add_assoc

added theorem category_theory.shift_functor_add_assoc_hom_app

added theorem category_theory.shift_functor_add_assoc_inv_app

added theorem category_theory.shift_functor_add_zero_add_hom_app

added theorem category_theory.shift_functor_add_zero_add_inv_app

added def category_theory.shift_functor_comm

added theorem category_theory.shift_functor_comm_eq

added theorem category_theory.shift_functor_comm_hom_app_comp_shift_shift_functor_add_hom_app

added theorem category_theory.shift_functor_comm_symm

added def category_theory.shift_functor_comp_iso_id

added theorem category_theory.shift_functor_inv

added def category_theory.shift_functor_zero

added theorem category_theory.shift_functor_zero_hom_app_shift

added theorem category_theory.shift_functor_zero_inv_app_shift

added theorem category_theory.shift_mk_core.add_zero_inv_app

added theorem category_theory.shift_mk_core.assoc_inv_app

added theorem category_theory.shift_mk_core.shift_functor_add_eq

added theorem category_theory.shift_mk_core.shift_functor_eq

added theorem category_theory.shift_mk_core.shift_functor_zero_eq

added theorem category_theory.shift_mk_core.zero_add_inv_app

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_functor_comp_iso_id_add_neg_self_hom_app

added theorem category_theory.shift_shift_functor_comp_iso_id_add_neg_self_inv_app

added theorem category_theory.shift_shift_functor_comp_iso_id_hom_app

added theorem category_theory.shift_shift_functor_comp_iso_id_inv_app

added theorem category_theory.shift_shift_functor_comp_iso_id_neg_add_self_hom_app

added theorem category_theory.shift_shift_functor_comp_iso_id_neg_add_self_inv_app

added theorem category_theory.shift_shift_neg'

added def category_theory.shift_shift_neg

added theorem category_theory.shift_zero'

added def category_theory.shift_zero

added theorem category_theory.shift_zero_eq_zero

Modified src/category_theory/triangulated/basic.lean

added def category_theory.pretriangulated.triangle.hom_mk

added def category_theory.pretriangulated.triangle.iso_mk

Modified src/category_theory/triangulated/pretriangulated.lean

deleted theorem category_theory.pretriangulated.triangulated_functor.map_distinguished

deleted def category_theory.pretriangulated.triangulated_functor.map_triangle

deleted structure category_theory.pretriangulated.triangulated_functor

deleted def category_theory.pretriangulated.triangulated_functor_struct.id

deleted def category_theory.pretriangulated.triangulated_functor_struct.map_triangle

deleted structure category_theory.pretriangulated.triangulated_functor_struct

Modified src/category_theory/triangulated/rotate.lean

deleted def category_theory.pretriangulated.from_inv_rotate_rotate

deleted def category_theory.pretriangulated.from_rotate_inv_rotate

deleted def category_theory.pretriangulated.inv_rot_comp_rot_hom

deleted def category_theory.pretriangulated.inv_rot_comp_rot_inv

deleted def category_theory.pretriangulated.rot_comp_inv_rot_hom

deleted def category_theory.pretriangulated.rot_comp_inv_rot_inv

deleted def category_theory.pretriangulated.to_inv_rotate_rotate

deleted def category_theory.pretriangulated.to_rotate_inv_rotate

deleted def category_theory.pretriangulated.triangle_morphism.inv_rotate

deleted def category_theory.pretriangulated.triangle_morphism.rotate