PhysLean Documentation

PhysLean.Relativity.Tensors.Color.Basic

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) :

The core of the category of Types over C.

Equations

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

Instances For

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) :

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

Equations

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

Instances For

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. #

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 := ⋯ }

Instances For

@[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 := ⋯ }

Instances For

@[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_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_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_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_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_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_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_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_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

@[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_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_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✝

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 ⋯

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

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 (CategoryTheory.Over.isoMk e.toIso ⋯)

Instances For

@[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

Instances For

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 ⋯)

Instances For

@[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 ⋯)

Instances For

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 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 = IndexNotation.OverColor.equivToHom e ≪≫ (IndexNotation.OverColor.mkIso ⋯).hom

Instances For

@[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) :

(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) :

Hom.toEquiv (equivToHomEq e h) = e