mathlib3 documentation

category_theory.bicategory.coherence_tactic

A coherence tactic for bicategories, and ⊗≫ (composition up to associators) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We provide a coherence tactic, which proves that any two 2-morphisms (with the same source and target) in a bicategory which are built out of associators and unitors are equal.

We also provide f ⊗≫ g, the bicategorical_comp operation, which automatically inserts associators and unitors as needed to make the target of f match the source of g.

This file mainly deals with the type class setup for the coherence tactic. The actual front end tactic is given in category_theory/monooidal/coherence.lean at the same time as the coherence tactic for monoidal categories.

source
@[class]
structure category_theory.bicategory.lift_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) :
Type (max u v)

A typeclass carrying a choice of lift of a 1-morphism from B to free_bicategory B.

Instances of this typeclass
Instances of other typeclasses for category_theory.bicategory.lift_hom
  • category_theory.bicategory.lift_hom.has_sizeof_inst
source
@[protected, instance]
def category_theory.bicategory.lift_hom_id {B : Type u} [category_theory.bicategory B] {a : B} :
category_theory.bicategory.lift_hom (𝟙 a)
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom_comp {B : Type u} [category_theory.bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] :
category_theory.bicategory.lift_hom (f ≫ g)
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom_of {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) :
category_theory.bicategory.lift_hom f
Equations
source
@[class]
structure category_theory.bicategory.lift_hom₂ {B : Type u} [category_theory.bicategory B] {a b : B} {f g : a ⟶ b} [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] (η : f ⟶ g) :
Type (max u v)

A typeclass carrying a choice of lift of a 2-morphism from B to free_bicategory B.

Instances of this typeclass
Instances of other typeclasses for category_theory.bicategory.lift_hom₂
  • category_theory.bicategory.lift_hom₂.has_sizeof_inst
source
@[protected, instance]
def category_theory.bicategory.lift_hom₂_id {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) [category_theory.bicategory.lift_hom f] :
category_theory.bicategory.lift_hom₂ (𝟙 f)
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom₂_left_unitor_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) [category_theory.bicategory.lift_hom f] :
category_theory.bicategory.lift_hom₂ (category_theory.bicategory.left_unitor f).hom
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom₂_left_unitor_inv {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) [category_theory.bicategory.lift_hom f] :
category_theory.bicategory.lift_hom₂ (category_theory.bicategory.left_unitor f).inv
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom₂_right_unitor_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) [category_theory.bicategory.lift_hom f] :
category_theory.bicategory.lift_hom₂ (category_theory.bicategory.right_unitor f).hom
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom₂_right_unitor_inv {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) [category_theory.bicategory.lift_hom f] :
category_theory.bicategory.lift_hom₂ (category_theory.bicategory.right_unitor f).inv
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom₂_associator_hom {B : Type u} [category_theory.bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] :
category_theory.bicategory.lift_hom₂ (category_theory.bicategory.associator f g h).hom
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom₂_associator_inv {B : Type u} [category_theory.bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] :
category_theory.bicategory.lift_hom₂ (category_theory.bicategory.associator f g h).inv
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom₂_comp {B : Type u} [category_theory.bicategory B] {a b : B} {f g h : a ⟶ b} [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] (η : f ⟶ g) (θ : g ⟶ h) [category_theory.bicategory.lift_hom₂ η] [category_theory.bicategory.lift_hom₂ θ] :
category_theory.bicategory.lift_hom₂ (η ≫ θ)
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom₂_whisker_left {B : Type u} [category_theory.bicategory B] {a b c : B} (f : a ⟶ b) [category_theory.bicategory.lift_hom f] {g h : b ⟶ c} (η : g ⟶ h) [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.lift_hom₂ η] :
category_theory.bicategory.lift_hom₂ (category_theory.bicategory.whisker_left f η)
Equations
source
@[protected, instance]
def category_theory.bicategory.lift_hom₂_whisker_right {B : Type u} [category_theory.bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom₂ η] {h : b ⟶ c} [category_theory.bicategory.lift_hom h] :
category_theory.bicategory.lift_hom₂ (category_theory.bicategory.whisker_right η h)
Equations
source
@[class]
structure category_theory.bicategory.bicategorical_coherence {B : Type u} [category_theory.bicategory B] {a b : B} (f g : a ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] :
Type w

A typeclass carrying a choice of bicategorical structural isomorphism between two objects. Used by the ⊗≫ bicategorical composition operator, and the coherence tactic.

Instances of this typeclass
Instances of other typeclasses for category_theory.bicategory.bicategorical_coherence
  • category_theory.bicategory.bicategorical_coherence.has_sizeof_inst
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.refl {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) [category_theory.bicategory.lift_hom f] :
category_theory.bicategory.bicategorical_coherence f f
Equations
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.refl_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) [category_theory.bicategory.lift_hom f] :
category_theory.bicategory.bicategorical_coherence.hom f f = 𝟙 f
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.whisker_left_hom {B : Type u} [category_theory.bicategory B] {a b c : B} (f : a ⟶ b) (g h : b ⟶ c) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.bicategorical_coherence g h] :
category_theory.bicategory.bicategorical_coherence.hom (f ≫ g) (f ≫ h) = category_theory.bicategory.whisker_left f (category_theory.bicategory.bicategorical_coherence.hom g h)
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.whisker_left {B : Type u} [category_theory.bicategory B] {a b c : B} (f : a ⟶ b) (g h : b ⟶ c) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.bicategorical_coherence g h] :
category_theory.bicategory.bicategorical_coherence (f ≫ g) (f ≫ h)
Equations
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.whisker_right_hom {B : Type u} [category_theory.bicategory B] {a b c : B} (f g : a ⟶ b) (h : b ⟶ c) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.bicategorical_coherence f g] :
category_theory.bicategory.bicategorical_coherence.hom (f ≫ h) (g ≫ h) = category_theory.bicategory.whisker_right (category_theory.bicategory.bicategorical_coherence.hom f g) h
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.whisker_right {B : Type u} [category_theory.bicategory B] {a b c : B} (f g : a ⟶ b) (h : b ⟶ c) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.bicategorical_coherence f g] :
category_theory.bicategory.bicategorical_coherence (f ≫ h) (g ≫ h)
Equations
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.tensor_right {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence (𝟙 b) g] :
category_theory.bicategory.bicategorical_coherence f (f ≫ g)
Equations
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.tensor_right_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence (𝟙 b) g] :
category_theory.bicategory.bicategorical_coherence.hom f (f ≫ g) = (category_theory.bicategory.right_unitor f).inv ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.bicategorical_coherence.hom (𝟙 b) g)
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.tensor_right' {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence g (𝟙 b)] :
category_theory.bicategory.bicategorical_coherence (f ≫ g) f
Equations
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.tensor_right'_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence g (𝟙 b)] :
category_theory.bicategory.bicategorical_coherence.hom (f ≫ g) f = category_theory.bicategory.whisker_left f (category_theory.bicategory.bicategorical_coherence.hom g (𝟙 b)) ≫ (category_theory.bicategory.right_unitor f).hom
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.left {B : Type u} [category_theory.bicategory B] {a b : B} (f g : a ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence f g] :
category_theory.bicategory.bicategorical_coherence (𝟙 a ≫ f) g
Equations
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.left_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f g : a ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence f g] :
category_theory.bicategory.bicategorical_coherence.hom (𝟙 a ≫ f) g = (category_theory.bicategory.left_unitor f).hom ≫ category_theory.bicategory.bicategorical_coherence.hom f g
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.left'_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f g : a ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence f g] :
category_theory.bicategory.bicategorical_coherence.hom f (𝟙 a ≫ g) = category_theory.bicategory.bicategorical_coherence.hom f g ≫ (category_theory.bicategory.left_unitor g).inv
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.left' {B : Type u} [category_theory.bicategory B] {a b : B} (f g : a ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence f g] :
category_theory.bicategory.bicategorical_coherence f (𝟙 a ≫ g)
Equations
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.right {B : Type u} [category_theory.bicategory B] {a b : B} (f g : a ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence f g] :
category_theory.bicategory.bicategorical_coherence (f ≫ 𝟙 b) g
Equations
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.right_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f g : a ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence f g] :
category_theory.bicategory.bicategorical_coherence.hom (f ≫ 𝟙 b) g = (category_theory.bicategory.right_unitor f).hom ≫ category_theory.bicategory.bicategorical_coherence.hom f g
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.right'_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f g : a ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence f g] :
category_theory.bicategory.bicategorical_coherence.hom f (g ≫ 𝟙 b) = category_theory.bicategory.bicategorical_coherence.hom f g ≫ (category_theory.bicategory.right_unitor g).inv
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.right' {B : Type u} [category_theory.bicategory B] {a b : B} (f g : a ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence f g] :
category_theory.bicategory.bicategorical_coherence f (g ≫ 𝟙 b)
Equations
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.assoc {B : Type u} [category_theory.bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.lift_hom i] [category_theory.bicategory.bicategorical_coherence (f ≫ g ≫ h) i] :
category_theory.bicategory.bicategorical_coherence ((f ≫ g) ≫ h) i
Equations
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.assoc_hom {B : Type u} [category_theory.bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.lift_hom i] [category_theory.bicategory.bicategorical_coherence (f ≫ g ≫ h) i] :
category_theory.bicategory.bicategorical_coherence.hom ((f ≫ g) ≫ h) i = (category_theory.bicategory.associator f g h).hom ≫ category_theory.bicategory.bicategorical_coherence.hom (f ≫ g ≫ h) i
source
@[simp]
theorem category_theory.bicategory.bicategorical_coherence.assoc'_hom {B : Type u} [category_theory.bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.lift_hom i] [category_theory.bicategory.bicategorical_coherence i (f ≫ g ≫ h)] :
category_theory.bicategory.bicategorical_coherence.hom i ((f ≫ g) ≫ h) = category_theory.bicategory.bicategorical_coherence.hom i (f ≫ g ≫ h) ≫ (category_theory.bicategory.associator f g h).inv
source
@[protected, instance]
def category_theory.bicategory.bicategorical_coherence.assoc' {B : Type u} [category_theory.bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.lift_hom i] [category_theory.bicategory.bicategorical_coherence i (f ≫ g ≫ h)] :
category_theory.bicategory.bicategorical_coherence i ((f ≫ g) ≫ h)
Equations
source
noncomputable def category_theory.bicategory.bicategorical_iso {B : Type u} [category_theory.bicategory B] {a b : B} (f g : a ⟶ b) [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.bicategorical_coherence f g] :
f ≅ g

Construct an isomorphism between two objects in a bicategorical category out of unitors and associators.

Equations
source
def category_theory.bicategory.bicategorical_comp {B : Type u} [category_theory.bicategory B] {a b : B} {f g h i : a ⟶ b} [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.bicategorical_coherence g h] (η : f ⟶ g) (θ : h ⟶ i) :
f ⟶ i

Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.

Equations
source
noncomputable def category_theory.bicategory.bicategorical_iso_comp {B : Type u} [category_theory.bicategory B] {a b : B} {f g h i : a ⟶ b} [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] [category_theory.bicategory.bicategorical_coherence g h] (η : f ≅ g) (θ : h ≅ i) :
f ≅ i

Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.

Equations
source
@[simp]
theorem category_theory.bicategory.bicategorical_comp_refl {B : Type u} [category_theory.bicategory B] {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) :
category_theory.bicategory.bicategorical_comp η θ = η ≫ θ
source
meta def tactic.bicategorical_coherence  :
tactic unit

Coherence tactic for bicategories.

source
meta def tactic.bicategory.whisker_simps  :
tactic unit

Simp lemmas for rewriting a 2-morphism into a normal form.

source
@[nolint]
theorem tactic.bicategory.coherence.assoc_lift_hom₂ {B : Type u} [category_theory.bicategory B] {a b : B} {f g h i : a ⟶ b} [category_theory.bicategory.lift_hom f] [category_theory.bicategory.lift_hom g] [category_theory.bicategory.lift_hom h] (η : f ⟶ g) (θ : g ⟶ h) (ι : h ⟶ i) [category_theory.bicategory.lift_hom₂ η] [category_theory.bicategory.lift_hom₂ θ] :
η ≫ θ ≫ ι = (η ≫ θ) ≫ ι

Auxiliary simp lemma for the coherence tactic: this move brackets to the left in order to expose a maximal prefix built out of unitors and associators.