category_theory.sums.associator

source

def category_theory.sum.associator (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] :

(C ⊕ D) ⊕ E ⥤ C ⊕ D ⊕ E

The associator functor (C ⊕ D) ⊕ E ⥤ C ⊕ (D ⊕ E) for sums of categories.

Equations

category_theory.sum.associator C D E = {obj := λ (X : (C ⊕ D) ⊕ E), category_theory.sum.associator._match_1 C D E X, map := λ (X Y : (C ⊕ D) ⊕ E) (f : X ⟶ Y), category_theory.sum.associator._match_2 C D E X Y f, map_id' := _, map_comp' := _}
category_theory.sum.associator._match_1 C D E (sum.inr X) = sum.inr (sum.inr X)
category_theory.sum.associator._match_1 C D E (sum.inl (sum.inr X)) = sum.inr (sum.inl X)
category_theory.sum.associator._match_1 C D E (sum.inl (sum.inl X)) = sum.inl X
category_theory.sum.associator._match_2 C D E (sum.inr X) (sum.inr Y) f = f
category_theory.sum.associator._match_2 C D E (sum.inl (sum.inr X)) (sum.inl (sum.inr Y)) f = f
category_theory.sum.associator._match_2 C D E (sum.inl (sum.inl X)) (sum.inl (sum.inl Y)) f = f

Instances for category_theory.sum.associator

category_theory.sum.associator_is_equivalence

source

@[simp]

theorem category_theory.sum.associator_obj_inl_inl (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] (X : C) :

(category_theory.sum.associator C D E).obj (sum.inl (sum.inl X)) = sum.inl X

source

@[simp]

theorem category_theory.sum.associator_obj_inl_inr (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] (X : D) :

(category_theory.sum.associator C D E).obj (sum.inl (sum.inr X)) = sum.inr (sum.inl X)

source

@[simp]

theorem category_theory.sum.associator_obj_inr (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] (X : E) :

(category_theory.sum.associator C D E).obj (sum.inr X) = sum.inr (sum.inr X)

source

@[simp]

theorem category_theory.sum.associator_map_inl_inl (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] {X Y : C} (f : sum.inl (sum.inl X) ⟶ sum.inl (sum.inl Y)) :

(category_theory.sum.associator C D E).map f = f

source

@[simp]

theorem category_theory.sum.associator_map_inl_inr (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] {X Y : D} (f : sum.inl (sum.inr X) ⟶ sum.inl (sum.inr Y)) :

(category_theory.sum.associator C D E).map f = f

source

@[simp]

theorem category_theory.sum.associator_map_inr (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] {X Y : E} (f : sum.inr X ⟶ sum.inr Y) :

(category_theory.sum.associator C D E).map f = f

source

def category_theory.sum.inverse_associator (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] :

C ⊕ D ⊕ E ⥤ (C ⊕ D) ⊕ E

The inverse associator functor C ⊕ (D ⊕ E) ⥤ (C ⊕ D) ⊕ E for sums of categories.

Equations

category_theory.sum.inverse_associator C D E = {obj := λ (X : C ⊕ D ⊕ E), category_theory.sum.inverse_associator._match_1 C D E X, map := λ (X Y : C ⊕ D ⊕ E) (f : X ⟶ Y), category_theory.sum.inverse_associator._match_2 C D E X Y f, map_id' := _, map_comp' := _}
category_theory.sum.inverse_associator._match_1 C D E (sum.inr (sum.inr X)) = sum.inr X
category_theory.sum.inverse_associator._match_1 C D E (sum.inr (sum.inl X)) = sum.inl (sum.inr X)
category_theory.sum.inverse_associator._match_1 C D E (sum.inl X) = sum.inl (sum.inl X)
category_theory.sum.inverse_associator._match_2 C D E (sum.inr (sum.inr X)) (sum.inr (sum.inr Y)) f = f
category_theory.sum.inverse_associator._match_2 C D E (sum.inr (sum.inl X)) (sum.inr (sum.inl Y)) f = f
category_theory.sum.inverse_associator._match_2 C D E (sum.inl X) (sum.inl Y) f = f

Instances for category_theory.sum.inverse_associator

category_theory.sum.inverse_associator_is_equivalence

source

@[simp]

theorem category_theory.sum.inverse_associator_obj_inl (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] (X : C) :

(category_theory.sum.inverse_associator C D E).obj (sum.inl X) = sum.inl (sum.inl X)

source

@[simp]

theorem category_theory.sum.inverse_associator_obj_inr_inl (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] (X : D) :

(category_theory.sum.inverse_associator C D E).obj (sum.inr (sum.inl X)) = sum.inl (sum.inr X)

source

@[simp]

theorem category_theory.sum.inverse_associator_obj_inr_inr (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] (X : E) :

(category_theory.sum.inverse_associator C D E).obj (sum.inr (sum.inr X)) = sum.inr X

source

@[simp]

theorem category_theory.sum.inverse_associator_map_inl (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] {X Y : C} (f : sum.inl X ⟶ sum.inl Y) :

(category_theory.sum.inverse_associator C D E).map f = f

source

@[simp]

theorem category_theory.sum.inverse_associator_map_inr_inl (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] {X Y : D} (f : sum.inr (sum.inl X) ⟶ sum.inr (sum.inl Y)) :

(category_theory.sum.inverse_associator C D E).map f = f

source

@[simp]

theorem category_theory.sum.inverse_associator_map_inr_inr (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] {X Y : E} (f : sum.inr (sum.inr X) ⟶ sum.inr (sum.inr Y)) :

(category_theory.sum.inverse_associator C D E).map f = f

source

def category_theory.sum.associativity (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] :

(C ⊕ D) ⊕ E ≌ C ⊕ D ⊕ E

The equivalence of categories expressing associativity of sums of categories.

Equations

category_theory.sum.associativity C D E = category_theory.equivalence.mk (category_theory.sum.associator C D E) (category_theory.sum.inverse_associator C D E) (category_theory.nat_iso.of_components (λ (X : (C ⊕ D) ⊕ E), category_theory.eq_to_iso _) _) (category_theory.nat_iso.of_components (λ (X : C ⊕ D ⊕ E), category_theory.eq_to_iso _) _)

source

@[protected, instance]

def category_theory.sum.associator_is_equivalence (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] :

category_theory.is_equivalence (category_theory.sum.associator C D E)

Equations

category_theory.sum.associator_is_equivalence C D E = category_theory.is_equivalence.of_equivalence (category_theory.sum.associativity C D E)

source

@[protected, instance]

def category_theory.sum.inverse_associator_is_equivalence (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] :

category_theory.is_equivalence (category_theory.sum.inverse_associator C D E)

Equations

category_theory.sum.inverse_associator_is_equivalence C D E = category_theory.is_equivalence.of_equivalence_inverse (category_theory.sum.associativity C D E)

mathlib documentation

Associator for binary disjoint union of categories. #