Over color category.

Color

The notion of color will plays a critical role of the formalisation of index notation used here. The way to describe color is through examples. Indices of real Lorentz tensors can either be up-colored or down-colored. On the other hand, indices of Einstein tensors can just down-colored. In the case of complex Lorentz tensors, indices can take one of six different colors, corresponding to up and down, dotted and undotted weyl fermion indices and up and down Lorentz indices.

def IndexNotation.OverColor (C : Type) : Type 1

The core of the category of Types over C.

Equations

• IndexNotation.OverColor C = CategoryTheory.Core (CategoryTheory.Over C)

instance IndexNotation.instGroupoidOverColor (C : Type) : CategoryTheory.Groupoid (OverColor C)

The instance of OverColor C as a groupoid.

Equations

• IndexNotation.instGroupoidOverColor C = CategoryTheory.coreCategory

theorem IndexNotation.OverColor.Hom.ext {C : Type} {f g : OverColor C} (m n : f ⟶ g) (h : m.hom = n.hom) : m = n

If m and n are morphisms in OverColor C, they are equal if their underlying morphisms in Over C are equal.

theorem IndexNotation.OverColor.Hom.ext_iff {C : Type} {f g : OverColor C} (m n : f ⟶ g) : (∀ (x : f.left), m.hom.left x = n.hom.left x) ↔ m = n

def IndexNotation.OverColor.Hom.toEquiv {C : Type} {f g : OverColor C} (m : f ⟶ g) : f.left ≃ g.left

Given a hom in OverColor C the underlying equivalence between types.

Equations

• IndexNotation.OverColor.Hom.toEquiv m = { toFun := m.hom.left, invFun := m.inv.left, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem IndexNotation.OverColor.Hom.toEquiv_id {C : Type} (f : OverColor C) : toEquiv (CategoryTheory.CategoryStruct.id f) = Equiv.refl f.left

The equivalence of types underlying the identity morphism is the reflexive equivalence.

@[simp]

theorem IndexNotation.OverColor.Hom.toEquiv_comp {C : Type} {f g h : OverColor C} (m : f ⟶ g) (n : g ⟶ h) : toEquiv (CategoryTheory.CategoryStruct.comp m n) = (toEquiv m).trans (toEquiv n)

The function toEquiv obeys compositions.

theorem IndexNotation.OverColor.Hom.toEquiv_symm_apply {C : Type} {f g : OverColor C} (m : f ⟶ g) (i : g.left) : f.hom ((toEquiv m).symm i) = g.hom i

theorem IndexNotation.OverColor.Hom.toEquiv_comp_hom {C : Type} {f g : OverColor C} (m : f ⟶ g) : g.hom ∘ ⇑(toEquiv m) = f.hom

theorem IndexNotation.OverColor.Hom.toEquiv_comp_inv_apply {C : Type} {f g : OverColor C} (m : f ⟶ g) (i : g.left) : f.hom ((toEquiv m).symm i) = g.hom i

theorem IndexNotation.OverColor.Hom.toEquiv_comp_apply {C : Type} {f g : OverColor C} (m : f ⟶ g) (i : f.left) : f.hom i = g.hom ((toEquiv m) i)

def IndexNotation.OverColor.Hom.toIso {C : Type} {f g : OverColor C} (m : f ⟶ g) : f ≅ g

Given a morphism in OverColor C, the corresponding isomorphism.

Equations

• IndexNotation.OverColor.Hom.toIso m = { hom := m, inv := CategoryTheory.Iso.symm m, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem IndexNotation.OverColor.Hom.hom_comp {C : Type} {f g h : OverColor C} (m : f ⟶ g) (n : g ⟶ h) : (CategoryTheory.CategoryStruct.comp m n).hom = CategoryTheory.CategoryStruct.comp m.hom n.hom

The monoidal structure on OverColor C.

The category OverColor C can, through the disjoint union, be given the structure of a symmetric monoidal category.

instance IndexNotation.OverColor.instMonoidalCategoryStruct (C : Type) : CategoryTheory.MonoidalCategoryStruct (OverColor C)

The category OverColor C carries an instance of a Monoidal category structure.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_tensorObj_right_as (C : Type) (f g : OverColor C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj f g).right.as = PUnit.unit

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_associator_inv_hom_left (C : Type) (X Y Z : OverColor C) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) X ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) Y Z)).left) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom.left a✝ = (Equiv.sumAssoc X.left Y.left Z.left).symm a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_tensorHom_hom_left (C : Type) {X₁ Y₁ X₂ Y₂ : OverColor C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) (a✝ : (CategoryTheory.Over.mk (Sum.elim X₁.hom X₂.hom)).left) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom.left a✝ = Sum.map (⇑(Hom.toEquiv f)) (⇑(Hom.toEquiv g)) a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_rightUnitor_inv_inv_left (C : Type) (X : OverColor C) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) X (CategoryTheory.Over.mk Empty.elim)).left) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.inv.left a✝ = (Equiv.sumEmpty X.left Empty) a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_leftUnitor_inv_hom_left (C : Type) (X : OverColor C) (a✝ : X.left) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom.left a✝ = Sum.inr a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_whiskerLeft_hom_left (C : Type) (X Y1 Y2 : OverColor C) (m : Y1 ⟶ Y2) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) X Y1).left) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X m).hom.left a✝ = Sum.map id (⇑(Hom.toEquiv m)) a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_whiskerRight_inv_left (C : Type) {X₁✝ X₂✝ : OverColor C} (m : X₁✝ ⟶ X₂✝) (X : OverColor C) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) X₂✝ X).left) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight m X).inv.left a✝ = Sum.map (⇑(Hom.toEquiv m).symm) id a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_leftUnitor_inv_inv_left (C : Type) (X : OverColor C) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) (CategoryTheory.Over.mk Empty.elim) X).left) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.inv.left a✝ = (Equiv.emptySum Empty X.left) a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_tensorUnit_hom (C : Type) (a✝ : Empty) : (𝟙_ (OverColor C)).hom a✝ = a✝.elim

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_tensorObj_left (C : Type) (f g : OverColor C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj f g).left = (f.left ⊕ g.left)

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_tensorObj_hom (C : Type) (f g : OverColor C) (a✝ : (CategoryTheory.Functor.id Type).obj f.left ⊕ (CategoryTheory.Functor.id Type).obj g.left) : (CategoryTheory.MonoidalCategoryStruct.tensorObj f g).hom a✝ = Sum.elim f.hom g.hom a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_associator_inv_inv_left (C : Type) (X Y Z : OverColor C) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) X Y) Z).left) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.inv.left a✝ = (Equiv.sumAssoc X.left Y.left Z.left) a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_rightUnitor_inv_hom_left (C : Type) (X : OverColor C) (a✝ : X.left) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom.left a✝ = Sum.inl a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_leftUnitor_hom_inv_left (C : Type) (X : OverColor C) (a✝ : X.left) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.inv.left a✝ = Sum.inr a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_associator_hom_hom_left (C : Type) (X Y Z : OverColor C) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) X Y) Z).left) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom.left a✝ = (Equiv.sumAssoc X.left Y.left Z.left) a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_rightUnitor_hom_hom_left (C : Type) (X : OverColor C) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) X (CategoryTheory.Over.mk Empty.elim)).left) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom.left a✝ = (Equiv.sumEmpty X.left Empty) a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_leftUnitor_hom_hom_left (C : Type) (X : OverColor C) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) (CategoryTheory.Over.mk Empty.elim) X).left) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom.left a✝ = (Equiv.emptySum Empty X.left) a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_tensorHom_inv_left (C : Type) {X₁ Y₁ X₂ Y₂ : OverColor C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) (a✝ : (CategoryTheory.Over.mk (Sum.elim Y₁.hom Y₂.hom)).left) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).inv.left a✝ = Sum.map (⇑(Hom.toEquiv f).symm) (⇑(Hom.toEquiv g).symm) a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_tensorUnit_left (C : Type) : (𝟙_ (OverColor C)).left = Empty

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_associator_hom_inv_left (C : Type) (X Y Z : OverColor C) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) X ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) Y Z)).left) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.inv.left a✝ = (Equiv.sumAssoc X.left Y.left Z.left).symm a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_whiskerLeft_inv_left (C : Type) (X Y1 Y2 : OverColor C) (m : Y1 ⟶ Y2) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) X Y2).left) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X m).inv.left a✝ = Sum.map id (⇑(Hom.toEquiv m).symm) a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_rightUnitor_hom_inv_left (C : Type) (X : OverColor C) (a✝ : X.left) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.inv.left a✝ = Sum.inl a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_whiskerRight_hom_left (C : Type) {X₁✝ X₂✝ : OverColor C} (m : X₁✝ ⟶ X₂✝) (X : OverColor C) (a✝ : ((fun (f g : OverColor C) => CategoryTheory.Over.mk (Sum.elim f.hom g.hom)) X₁✝ X).left) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight m X).hom.left a✝ = Sum.map (⇑(Hom.toEquiv m)) id a✝

@[simp]

theorem IndexNotation.OverColor.instMonoidalCategoryStruct_tensorUnit_right_as (C : Type) : (𝟙_ (OverColor C)).right.as = PUnit.unit

instance IndexNotation.OverColor.instMonoidalCategory (C : Type) : CategoryTheory.MonoidalCategory (OverColor C)

The category OverColor C carries an instance of a Monoidal category.

Equations

• IndexNotation.OverColor.instMonoidalCategory C = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance IndexNotation.OverColor.instBraidedCategory (C : Type) : CategoryTheory.BraidedCategory (OverColor C)

The category OverColor C carries an instance of a braided category.

Equations

• One or more equations did not get rendered due to their size.

instance IndexNotation.OverColor.instSymmetricCategory (C : Type) : CategoryTheory.SymmetricCategory (OverColor C)

The category OverColor C carries an instance of a symmetric monoidal category.

Equations

• IndexNotation.OverColor.instSymmetricCategory C = CategoryTheory.SymmetricCategory.mk ⋯

def IndexNotation.OverColor.mk {X C : Type} (f : X → C) : OverColor C

Make an object of OverColor C from a map X → C.

Equations

• IndexNotation.OverColor.mk f = CategoryTheory.Over.mk f

@[simp]

theorem IndexNotation.OverColor.mk_hom {X C : Type} (f : X → C) : (mk f).hom = f

@[simp]

theorem IndexNotation.OverColor.mk_left {X C : Type} (f : X → C) : (mk f).left = X

theorem IndexNotation.OverColor.Hom.fin_ext {C : Type} {n : ℕ} {f g : Fin n → C} (σ σ' : mk f ⟶ mk g) (h : ∀ (i : Fin n), σ.hom.left i = σ'.hom.left i) : σ = σ'

@[simp]

theorem IndexNotation.OverColor.β_hom_toEquiv {X C Y : Type} (f : X → C) (g : Y → C) : Hom.toEquiv (β_ (mk f) (mk g)).hom = Equiv.sumComm X Y

@[simp]

theorem IndexNotation.OverColor.β_inv_toEquiv {X C Y : Type} (f : X → C) (g : Y → C) : Hom.toEquiv (β_ (mk f) (mk g)).inv = Equiv.sumComm Y X

@[simp]

theorem IndexNotation.OverColor.whiskeringLeft_toEquiv {X C Y Z : Type} (f : X → C) (g : Y → C) (h : Z → C) (σ : mk f ⟶ mk g) : Hom.toEquiv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (mk h) σ) = (Equiv.refl Z).sumCongr (Hom.toEquiv σ)

@[simp]

theorem IndexNotation.OverColor.whiskeringRight_toEquiv {X C Y Z : Type} (f : X → C) (g : Y → C) (h : Z → C) (σ : mk f ⟶ mk g) : Hom.toEquiv (CategoryTheory.MonoidalCategoryStruct.whiskerRight σ (mk h)) = (Hom.toEquiv σ).sumCongr (Equiv.refl Z)

@[simp]

theorem IndexNotation.OverColor.α_hom_toEquiv {X C Y Z : Type} (f : X → C) (g : Y → C) (h : Z → C) : Hom.toEquiv (CategoryTheory.MonoidalCategoryStruct.associator (mk f) (mk g) (mk h)).hom = Equiv.sumAssoc X Y Z

@[simp]

theorem IndexNotation.OverColor.α_inv_toEquiv {X C Y Z : Type} (f : X → C) (g : Y → C) (h : Z → C) : Hom.toEquiv (CategoryTheory.MonoidalCategoryStruct.associator (mk f) (mk g) (mk h)).inv = (Equiv.sumAssoc X Y Z).symm