Commit 2022-04-07 18:41 4ff75f5b

refactor(category_theory/bicategory): set simp-normal form for 2-morphisms (#13185)

Problem

The definition of bicategories contains the following axioms:

associator_naturality_left : ∀ {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
  (η ▷ g) ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h)
associator_naturality_middle : ∀ (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
  (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ (η ▷ h)
associator_naturality_right : ∀ (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
  (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ (g ◁ η) 
left_unitor_naturality : ∀ {f g : a ⟶ b} (η : f ⟶ g),
  𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η
right_unitor_naturality : ∀ {f g : a ⟶ b} (η : f ⟶ g) :
  η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η

By using these axioms, we can see that, for example, 2-morphisms (f₁ ≫ f₂) ◁ (f₃ ◁ (η ▷ (f₄ ≫ f₅))) and f₁ ◁ ((𝟙_ ≫ f₂ ≫ f₃) ◁ ((η ▷ f₄) ▷ f₅)) are equal up to some associators and unitors. The problem is that the proof of this fact requires tedious rewriting. We should insert appropriate associators and unitors, and then rewrite using the above axioms manually. This tedious rewriting is also a problem when we use the (forthcoming) coherence tactic (bicategorical version of #13125), which only works if the non-structural 2-morphisms in the LHS and the RHS are the same.

Main change

The main proposal of this PR is to introduce a normal form of such 2-morphisms, and put simp attributes to suitable lemmas in order to rewrite any 2-morphism into the normal form. For example, the normal form of the previouse example is f₁ ◁ (f₂ ◁ (f₃ ◁ ((η ▷ f₄) ▷ f₅))). The precise definition of the normal form can be found in the docs in basic.lean file. The new simp lemmas introduced in this PR are the following:

whisker_right_comp : ∀ {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
  η ▷ (g ≫ h) = (α_ f g h).inv ≫ η ▷ g ▷ h ≫ (α_ f' g h).hom 
whisker_assoc : ∀ (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
  (f ◁ η) ▷ h = (α_ f g h).hom ≫ f ◁ (η ▷ h) ≫ (α_ f g' h).inv
comp_whisker_left : ∀ (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
  (f ≫ g) ◁ η = (α_ f g h).hom ≫ f ◁ g ◁ η ≫ (α_ f g h').inv
id_whisker_left : ∀ {f g : a ⟶ b} (η : f ⟶ g),
  𝟙 a ◁ η = (λ_ f).hom ≫ η ≫ (λ_ g).inv
whisker_right_id : ∀ {f g : a ⟶ b} (η : f ⟶ g),
  η ▷ 𝟙 b = (ρ_ f).hom ≫ η ≫ (ρ_ g).inv

Logically, these are equivalent to the five axioms presented above. The point is that these equalities have the definite simplification direction.

Improvement

Some proofs that had been based on tedious rewriting are now automated. For example, the conditions in oplax_nat_trans.id, oplax_nat_trans.comp, and several functions in functor_bicategory.lean are now proved by tidy.

Specific changes

The new simp lemmas whisker_right_comp etc. actually have been included in the definition of bicategories instead of associate_naturality_left etc. so that the latter lemmas are proved in later of the file just by simp.
The precedence of the whiskering notations "infixr ◁:70" and "infixr ◁:70" have been changed into "infixr ◁:81" and "infixr ◁:81", which is now higher than that of the composition ≫. This setting is consistent with the normal form introduced in this PR in the sence that an expression is in normal form only if it has the minimal number of parentheses in this setting. For example, the normal form f₁ ◁ (f₂ ◁ (f₃ ◁ ((η ▷ f₄) ▷ f₅))) can be written as f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅.
The unneeded parentheses caused by the precedence change have been removed.
The lemmas whisker_right_id and whisker_right_comp have been renamed to id_whisker_right and comp_whisker_right since these are more consistent with the notation. Note that the name whisker_right_id and whisker_right_comp are now used for the two of the five simp lemmas presented above.
The lemmas in basic.lean have been rearranged to be more logically consistent.