Isomorphisms in the OverColor category

Useful equivalences.

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 (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 (CategoryTheory.Over.isoMk (Equiv.refl (IndexNotation.OverColor.mk c).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 (CategoryTheory.Over.isoMk (Equiv.refl (IndexNotation.OverColor.mk c1).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) : (mkIso h).hom.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) : (mkIso h).hom.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 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 = 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 := by decide) : (equivToHomEq e h).hom.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 := by decide) : Hom.toEquiv (equivToHomEq e h) = e

def IndexNotation.OverColor.fin2Iso {C : Type} {c : Fin 2 → C} : mk c ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (mk ![c 0]) (mk ![c 1])

The isomorphism splitting a mk c for Fin 2 → C into the tensor product of the Fin 1 → C maps defined by c 0 and c 1.

Equations

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

def IndexNotation.OverColor.fin3Iso {C : Type} {c : Fin 3 → C} : mk c ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (mk ![c 0]) (mk ![c 1, c 2])

The isomorphism splitting a mk c for c : Fin 3 → C into the tensor product of a Fin 1 → C map ![c 0] and a Fin 2 → C map ![c 1, c 2].

Equations

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

def IndexNotation.OverColor.fin3Iso' {C : Type} {c1 c2 c3 : C} : mk ![c1, c2, c3] ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (mk fun (x : Fin 1) => c1) (mk ![c2, c3])

The isomorphism splitting a mk ![c1, c2, c3] into the tensor product of a Fin 1 → C map fun _ => c1 and a Fin 2 → C map ![c 1, c 2].

Equations

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

def IndexNotation.OverColor.extractOne {C : Type} {n : ℕ} (i : Fin n.succ.succ) {c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) : mk (c1 ∘ Fin.succAbove ((Hom.toEquiv σ).symm i)) ⟶ mk (c2 ∘ i.succAbove)

Removes a given i : Fin n.succ.succ from a morphism in OverColor C.

Equations

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

@[simp]

theorem IndexNotation.OverColor.extractOne_homToEquiv {C : Type} {n : ℕ} (i : Fin n.succ.succ) {c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) : Hom.toEquiv (extractOne i σ) = PhysLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)

def IndexNotation.OverColor.extractTwo {C : Type} {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) {c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) : mk (c1 ∘ Fin.succAbove ((Hom.toEquiv σ).symm i) ∘ Fin.succAbove ((Hom.toEquiv (extractOne i σ)).symm j)) ⟶ mk (c2 ∘ i.succAbove ∘ j.succAbove)

Removes a given i : Fin n.succ.succ and j : Fin n.succ from a morphism in OverColor C.

Equations

• One or more equations did not get rendered due to their size.
• IndexNotation.OverColor.extractTwo i_2 j_2 σ_2 = IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin 0)) ⋯

@[simp]

theorem IndexNotation.OverColor.extractTwo_hom_left_apply {C : Type} {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ) {c1 c2 : Fin n.succ.succ.succ → C} (σ : mk c1 ⟶ mk c2) (x : Fin n.succ) : (extractTwo i j σ).hom.left x = (PhysLean.Fin.finExtractOnePerm ((PhysLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j) (PhysLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))) x

@[simp]

theorem IndexNotation.OverColor.extractTwo_toEquiv {C : Type} {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ) {c1 c2 : Fin n.succ.succ.succ → C} (σ : mk c1 ⟶ mk c2) : Hom.toEquiv (extractTwo i j σ) = PhysLean.Fin.finExtractOnePerm ((PhysLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j) (PhysLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))

theorem IndexNotation.OverColor.extractTwo_toEquiv_symm {C : Type} {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ) {c1 c2 : Fin n.succ.succ.succ → C} (σ : mk c1 ⟶ mk c2) : (Hom.toEquiv (extractTwo i j σ)).symm = (PhysLean.Fin.finExtractOnePerm ((PhysLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j) (PhysLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))).symm

def IndexNotation.OverColor.extractTwoAux {C : Type} {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) {c c1 : Fin n.succ.succ → C} (σ : mk c ⟶ mk c1) : mk ((c ∘ ⇑(PhysLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)).symm) ∘ Sum.inr) ⟶ mk ((c1 ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr)

Removes a given i : Fin n.succ.succ and j : Fin n.succ from a morphism in OverColor C. This is from and to different (by equivalent) objects to extractTwo.

Equations

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

def IndexNotation.OverColor.extractTwoAux' {C : Type} {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) {c c1 : Fin n.succ.succ → C} (σ : mk c ⟶ mk c1) : mk ((c ∘ ⇑(PhysLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)).symm) ∘ Sum.inl) ⟶ mk ((c1 ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)

Given a morphism mk c ⟶ mk c1 the corresponding morphism on the Fin 1 ⊕ Fin 1 maps obtained by extracting i and j.

Equations

• IndexNotation.OverColor.extractTwoAux' i j σ = IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin 1 ⊕ Fin 1)) ⋯

theorem IndexNotation.OverColor.extractTwo_finExtractTwo_succ {C : Type} {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ) {c c1 : Fin n.succ.succ.succ → C} (σ : mk c ⟶ mk c1) : CategoryTheory.CategoryStruct.comp σ (CategoryTheory.CategoryStruct.comp (equivToIso (PhysLean.Fin.finExtractTwo i j)).hom (mkSum (c1 ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm)).hom) = CategoryTheory.CategoryStruct.comp (equivToIso (PhysLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j))).hom (CategoryTheory.CategoryStruct.comp (mkSum (c ∘ ⇑(PhysLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)).symm)).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (extractTwoAux' i j σ) (extractTwoAux i j σ)))

theorem IndexNotation.OverColor.extractTwo_finExtractTwo {C : Type} {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) {c c1 : Fin n.succ.succ → C} (σ : mk c ⟶ mk c1) : CategoryTheory.CategoryStruct.comp σ (CategoryTheory.CategoryStruct.comp (equivToIso (PhysLean.Fin.finExtractTwo i j)).hom (mkSum (c1 ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm)).hom) = CategoryTheory.CategoryStruct.comp (equivToIso (PhysLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j))).hom (CategoryTheory.CategoryStruct.comp (mkSum (c ∘ ⇑(PhysLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)).symm)).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (extractTwoAux' i j σ) (extractTwoAux i j σ)))

def IndexNotation.OverColor.contrPairFin1Fin1 {C : Type} (τ : C → C) (c : Fin 1 ⊕ Fin 1 → C) (h : c (Sum.inr 0) = τ (c (Sum.inl 0))) : mk c ≅ (contrPair C τ).obj (mk fun (x : Fin 1) => c (Sum.inl 0))

The isomorphism between a Fin 1 ⊕ Fin 1 → C satisfying the condition c (Sum.inr 0) = τ (c (Sum.inl 0)) and an object in the image of contrPair.

Equations

• IndexNotation.OverColor.contrPairFin1Fin1 τ c h = IndexNotation.OverColor.Hom.toIso (CategoryTheory.Over.isoMk (Equiv.refl (IndexNotation.OverColor.mk c).left).toIso ⋯)

def IndexNotation.OverColor.contrPairEquiv {C : Type} {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = τ (c i)) : mk c ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj ((contrPair C τ).obj (CategoryTheory.Over.mk fun (x : Fin 1) => c i)) (mk (c ∘ i.succAbove ∘ j.succAbove))

The Isomorphism between a Fin n.succ.succ → C and the product containing an object in the image of contrPair based on the given values.

Equations

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

def IndexNotation.OverColor.permFinOne {C : Type} (c : Fin 1 → C) : mk c ⟶ mk ![c 0]

Given a function c from Fin 1 to C, this function returns a morphism from mk c to mk ![c 0]. -

Equations

• IndexNotation.OverColor.permFinOne c = (IndexNotation.OverColor.mkIso ⋯).hom

def IndexNotation.OverColor.permFinTwo {C : Type} (c : Fin 2 → C) : mk c ⟶ mk ![c 0, c 1]

This a function that takes a function c from Fin 2 to C and returns a morphism from mk c to mk ![c 0, c 1]. -

Equations

• IndexNotation.OverColor.permFinTwo c = (IndexNotation.OverColor.mkIso ⋯).hom

def IndexNotation.OverColor.permFinThree {C : Type} (c : Fin 3 → C) : mk c ⟶ mk ![c 0, c 1, c 2]

This is a function that takes a function c from Fin 3 to C and returns a morphism from mk c to mk ![c 0, c 1, c 2]. -

Equations

• IndexNotation.OverColor.permFinThree c = (IndexNotation.OverColor.mkIso ⋯).hom