Color

In the context of tensors Color is defined as the type of indices of a tensor. For example if A_μ^ν is a real Lorentz tensors, we say it has indicies of color [down, up]. For complex Lorentz Tensors there are six different colors, corresponding to the up and down indices of the Lorentz group, the dotted and undotted Weyl fermion indices.

Note if you only want to work with tensors, and not understand their implementation you can safely ignore these files.

Overview of directory

This file

Let C be the type of colors for a given species of tensor. In this file we define the category OverColor C. The objects of OverColor C correspond to allowed colorings of indices represented as a map X → C from a type X to C. Usually X will be Fin n for some n : ℕ. The morphisms of OverColor C correspond to color-preserving permutaitons of indices.

We also define here a symmetric-monoidal structure on OverColor C.

Discrete

The file Discrete contains some basic properties of the category Discrete C.

Lift

The file Lift we define the lift of a functor F : Discrete C ⥤ Rep k G to a symmetric monodial functor OverColor C ⥤ Rep k G, given by taking tensor products.

References

• Formalization of physics index notation in Lean 4, Tooby-Smith. https://doi.org/10.48550/arXiv.2411.07667.

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

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 = { of := CategoryTheory.Over.mk f }

@[reducible, inline]

abbrev IndexNotation.OverColor.hom {C : Type} (f : OverColor C) : (CategoryTheory.Functor.id Type).obj f.of.left ⟶ (CategoryTheory.Functor.fromPUnit C).obj f.of.right

The underlying morphism in the category of Types of a object f in OverColor C.

Equations

• f.hom = f.of.hom

@[reducible, inline]

abbrev IndexNotation.OverColor.left {C : Type} (f : OverColor C) : Type

The underlying object in the category of Types of a object f in OverColor C.

Equations

• f.left = f.of.left

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

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

Morphisms in the OverColor category.

@[reducible, inline]

abbrev CategoryTheory.CoreHom.hom {C : Type} {f g : IndexNotation.OverColor C} (m : f ⟶ g) : f.of ⟶ g.of

The underlying morphism in the category of Types of a morphism m in OverColor C.

Equations

• CategoryTheory.CoreHom.hom m = m.iso.hom

@[reducible, inline]

abbrev CategoryTheory.CoreHom.inv {C : Type} {f g : IndexNotation.OverColor C} (m : f ⟶ g) : g.of ⟶ f.of

The underlying inverse-morphism in the category of Types of a morphism m in OverColor C.

Equations

• CategoryTheory.CoreHom.inv m = m.iso.inv

theorem CategoryTheory.CoreHom.hom_inv_id {C : Type} {f g : IndexNotation.OverColor C} (m : f ⟶ g) : CategoryStruct.comp m.iso.hom m.iso.inv = CategoryStruct.id f.of

theorem CategoryTheory.CoreHom.inv_hom_id {C : Type} {f g : IndexNotation.OverColor C} (m : f ⟶ g) : CategoryStruct.comp m.iso.inv m.iso.hom = CategoryStruct.id g.of

@[reducible, inline]

abbrev CategoryTheory.CoreHom.symm {C : Type} {f g : IndexNotation.OverColor C} (m : f ⟶ g) : g ⟶ f

The inverse of a morphism in OverColor C.

Equations

• CategoryTheory.CoreHom.symm m = { iso := m.iso.symm }

theorem IndexNotation.OverColor.Hom.ext {C : Type} {f g : OverColor C} (m n : f ⟶ g) (h : CategoryTheory.CoreHom.hom m = CategoryTheory.CoreHom.hom n) : 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.of.left), (CategoryTheory.CoreHom.hom m).left x = (CategoryTheory.CoreHom.hom n).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 := (CategoryTheory.CoreHom.hom m).left, invFun := (CategoryTheory.CoreHom.inv m).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.CoreHom.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.CoreHom.hom (CategoryTheory.CategoryStruct.comp m n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CoreHom.hom m) (CategoryTheory.CoreHom.hom n)

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.associator_hom_iso_inv_left (C : Type) (X Y Z : OverColor C) (a✝ : (mk (Sum.elim X.hom (mk (Sum.elim Y.hom Z.hom)).hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.iso.inv.left a✝ = (Equiv.sumAssoc X.left Y.left Z.left).symm a✝

@[simp]

theorem IndexNotation.OverColor.rightUnitor_hom_iso_inv_left (C : Type) (X : OverColor C) (a✝ : X.of.left) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.iso.inv.left a✝ = (Equiv.sumEmpty X.left Empty).symm a✝

@[simp]

theorem IndexNotation.OverColor.associator_inv_iso_hom_left (C : Type) (X Y Z : OverColor C) (a✝ : (mk (Sum.elim X.hom (mk (Sum.elim Y.hom Z.hom)).hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.iso.hom.left a✝ = (Equiv.sumAssoc X.left Y.left Z.left).symm a✝

@[simp]

theorem IndexNotation.OverColor.leftUnitor_hom_iso_inv_left (C : Type) (X : OverColor C) (a✝ : X.of.left) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.iso.inv.left a✝ = (Equiv.emptySum Empty X.left).symm a✝

@[simp]

theorem IndexNotation.OverColor.whiskerLeft_iso_hom_left (C : Type) (X Y1 Y2 : OverColor C) (m : Y1 ⟶ Y2) (a✝ : (mk (Sum.elim X.hom Y1.hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X m).iso.hom.left a✝ = ((Equiv.refl X.left).sumCongr (Hom.toEquiv m)) a✝

@[simp]

theorem IndexNotation.OverColor.tensorHom_iso_hom_left (C : Type) {X₁ Y₁ X₂ Y₂ : OverColor C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) (a✝ : ((fun (f g : OverColor C) => mk (Sum.elim f.hom g.hom)) X₁ X₂).of.left) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).iso.hom.left a✝ = ((Equiv.refl Y₁.left).sumCongr (Hom.toEquiv g)) (((Hom.toEquiv f).sumCongr (Equiv.refl X₂.left)) a✝)

@[simp]

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

@[simp]

theorem IndexNotation.OverColor.tensorHom_iso_inv_left (C : Type) {X₁ Y₁ X₂ Y₂ : OverColor C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) (a✝ : ((fun (f g : OverColor C) => mk (Sum.elim f.hom g.hom)) Y₁ Y₂).of.left) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).iso.inv.left a✝ = ((Hom.toEquiv f).sumCongr (Equiv.refl X₂.left)).symm (((Equiv.refl Y₁.left).sumCongr (Hom.toEquiv g)).symm a✝)

@[simp]

theorem IndexNotation.OverColor.associator_inv_iso_inv_left (C : Type) (X Y Z : OverColor C) (a✝ : (mk (Sum.elim (mk (Sum.elim X.hom Y.hom)).hom Z.hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.iso.inv.left a✝ = (Equiv.sumAssoc X.left Y.left Z.left) a✝

@[simp]

theorem IndexNotation.OverColor.whiskerRight_iso_inv_left (C : Type) {X₁✝ X₂✝ : OverColor C} (m : X₁✝ ⟶ X₂✝) (X : OverColor C) (a✝ : (mk (Sum.elim X₂✝.hom X.hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight m X).iso.inv.left a✝ = ((Hom.toEquiv m).sumCongr (Equiv.refl X.left)).symm a✝

@[simp]

theorem IndexNotation.OverColor.whiskerRight_iso_hom_left (C : Type) {X₁✝ X₂✝ : OverColor C} (m : X₁✝ ⟶ X₂✝) (X : OverColor C) (a✝ : (mk (Sum.elim X₁✝.hom X.hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight m X).iso.hom.left a✝ = ((Hom.toEquiv m).sumCongr (Equiv.refl X.left)) a✝

@[simp]

theorem IndexNotation.OverColor.rightUnitor_inv_iso_inv_left (C : Type) (X : OverColor C) (a✝ : (mk (Sum.elim X.hom (mk Empty.elim).hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.iso.inv.left a✝ = (Equiv.sumEmpty X.left Empty) a✝

@[simp]

theorem IndexNotation.OverColor.tensorUnit_of_hom (C : Type) (a✝ : Empty) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (OverColor C)).of.hom a✝ = a✝.elim

@[simp]

theorem IndexNotation.OverColor.tensorUnit_of_left (C : Type) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (OverColor C)).of.left = Empty

@[simp]

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

@[simp]

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

@[simp]

theorem IndexNotation.OverColor.tensorUnit_of_right_as (C : Type) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (OverColor C)).of.right.as = PUnit.unit

@[simp]

theorem IndexNotation.OverColor.rightUnitor_hom_iso_hom_left (C : Type) (X : OverColor C) (a✝ : (mk (Sum.elim X.hom (mk Empty.elim).hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.iso.hom.left a✝ = (Equiv.sumEmpty X.left Empty) a✝

@[simp]

theorem IndexNotation.OverColor.leftUnitor_inv_iso_inv_left (C : Type) (X : OverColor C) (a✝ : (mk (Sum.elim (mk Empty.elim).hom X.hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.iso.inv.left a✝ = (Equiv.emptySum Empty X.left) a✝

@[simp]

theorem IndexNotation.OverColor.whiskerLeft_iso_inv_left (C : Type) (X Y1 Y2 : OverColor C) (m : Y1 ⟶ Y2) (a✝ : (mk (Sum.elim X.hom Y2.hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X m).iso.inv.left a✝ = ((Equiv.refl X.left).sumCongr (Hom.toEquiv m)).symm a✝

@[simp]

theorem IndexNotation.OverColor.leftUnitor_inv_iso_hom_left (C : Type) (X : OverColor C) (a✝ : X.of.left) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.iso.hom.left a✝ = (Equiv.emptySum Empty X.left).symm a✝

@[simp]

theorem IndexNotation.OverColor.rightUnitor_inv_iso_hom_left (C : Type) (X : OverColor C) (a✝ : X.of.left) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.iso.hom.left a✝ = (Equiv.sumEmpty X.left Empty).symm a✝

@[simp]

theorem IndexNotation.OverColor.associator_hom_iso_hom_left (C : Type) (X Y Z : OverColor C) (a✝ : (mk (Sum.elim (mk (Sum.elim X.hom Y.hom)).hom Z.hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.iso.hom.left a✝ = (Equiv.sumAssoc X.left Y.left Z.left) a✝

@[simp]

theorem IndexNotation.OverColor.leftUnitor_hom_iso_hom_left (C : Type) (X : OverColor C) (a✝ : (mk (Sum.elim (mk Empty.elim).hom X.hom)).of.left) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.iso.hom.left a✝ = (Equiv.emptySum Empty X.left) a✝

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

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

Equations

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

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 = { toBraidedCategory := IndexNotation.OverColor.instBraidedCategory C, symmetry := ⋯ }

theorem IndexNotation.OverColor.Hom.fin_ext {C : Type} {n : ℕ} {f g : Fin n → C} (σ σ' : mk f ⟶ mk g) (h : ∀ (i : Fin n), (CategoryTheory.CoreHom.hom σ).left i = (CategoryTheory.CoreHom.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

Isomorphisms.

def IndexNotation.OverColor.equivToIso {X C Y : Type} {c : X → C} (e : X ≃ Y) : mk c ≅ mk (c ∘ ⇑e.symm)

The isomorphism between c : X → C and c ∘ e.symm as objects in OverColor C for an equivalence e.

Equations

• IndexNotation.OverColor.equivToIso e = IndexNotation.OverColor.Hom.toIso { iso := CategoryTheory.Over.isoMk e.toIso ⋯ }

@[simp]

theorem IndexNotation.OverColor.equivToIso_homToEquiv {X C Y : Type} {c : X → C} (e : X ≃ Y) : Hom.toEquiv (equivToIso e).hom = e

@[simp]

theorem IndexNotation.OverColor.equivToIso_inv_homToEquiv {X C Y : Type} {c : X → C} (e : X ≃ Y) : Hom.toEquiv (equivToIso e).inv = e.symm

def IndexNotation.OverColor.equivToHom {X C Y : Type} {c : X → C} (e : X ≃ Y) : mk c ⟶ mk (c ∘ ⇑e.symm)

The homomorphism between c : X → C and c ∘ e.symm as objects in OverColor C for an equivalence e.

Equations

• IndexNotation.OverColor.equivToHom e = (IndexNotation.OverColor.equivToIso e).hom

def IndexNotation.OverColor.mkSum {X Y C : Type} (c : X ⊕ Y → C) : mk c ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (mk (c ∘ Sum.inl)) (mk (c ∘ Sum.inr))

Given a map X ⊕ Y → C, the isomorphism mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.inr).

Equations

• IndexNotation.OverColor.mkSum c = IndexNotation.OverColor.Hom.toIso { iso := CategoryTheory.Over.isoMk (Equiv.refl (IndexNotation.OverColor.mk c).of.left).toIso ⋯ }

@[simp]

theorem IndexNotation.OverColor.mkSum_homToEquiv {X Y C : Type} {c : X ⊕ Y → C} : Hom.toEquiv (mkSum c).hom = Equiv.refl (mk c).left

@[simp]

theorem IndexNotation.OverColor.mkSum_inv_homToEquiv {X Y C : Type} {c : X ⊕ Y → C} : Hom.toEquiv (mkSum c).inv = Equiv.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj (mk (c ∘ Sum.inl)) (mk (c ∘ Sum.inr))).left

def IndexNotation.OverColor.mkIso {X C : Type} {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2

The isomorphism between objects in OverColor C given equality of maps.

Equations

• IndexNotation.OverColor.mkIso h = IndexNotation.OverColor.Hom.toIso { iso := CategoryTheory.Over.isoMk (Equiv.refl (IndexNotation.OverColor.mk c1).of.left).toIso ⋯ }

theorem IndexNotation.OverColor.mkIso_refl_hom {X C : Type} {c : X → C} : (mkIso ⋯).hom = CategoryTheory.CategoryStruct.id (mk c)

theorem IndexNotation.OverColor.mkIso_hom_hom_left {X C : Type} {c1 c2 : X → C} (h : c1 = c2) : (CategoryTheory.CoreHom.hom (mkIso h).hom).left = (Equiv.refl X).toFun

@[simp]

theorem IndexNotation.OverColor.mkIso_hom_hom_left_apply {X C : Type} {c1 c2 : X → C} (h : c1 = c2) (x : X) : (CategoryTheory.CoreHom.hom (mkIso h).hom).left x = x

@[simp]

theorem IndexNotation.OverColor.equivToIso_mkIso_hom {X C : Type} {c1 c2 : X → C} (h : c1 = c2) : Hom.toEquiv (mkIso h).hom = Equiv.refl (mk c1).left

@[simp]

theorem IndexNotation.OverColor.equivToIso_mkIso_inv {X C : Type} {c1 c2 : X → C} (h : c1 = c2) : Hom.toEquiv (mkIso h).inv = Equiv.refl (mk c2).left

def IndexNotation.OverColor.equivToHomEq {X C Y : Type} {c : X → C} {c1 : Y → C} (e : X ≃ Y) (h : ∀ (x : Y), c1 x = (c ∘ ⇑e.symm) x := by try {simp; decide }; try decide) : mk c ⟶ mk c1

The morphism from mk c to mk c1 obtained by an equivalence and an equality lemma.

Equations

• IndexNotation.OverColor.equivToHomEq e h = CategoryTheory.CategoryStruct.comp (IndexNotation.OverColor.equivToHom e) (IndexNotation.OverColor.mkIso ⋯).hom

@[simp]

theorem IndexNotation.OverColor.equivToHomEq_hom_left {X C Y : Type} {c : X → C} {c1 : Y → C} (e : X ≃ Y) (h : ∀ (x : Y), c1 x = (c ∘ ⇑e.symm) x) : (CategoryTheory.CoreHom.hom (equivToHomEq e h)).left = e.toFun

@[simp]

theorem IndexNotation.OverColor.equivToHomEq_toEquiv {X C Y : Type} {c : X → C} {c1 : Y → C} (e : X ≃ Y) (h : ∀ (x : Y), c1 x = (c ∘ ⇑e.symm) x) : Hom.toEquiv (equivToHomEq e h) = e