From cecec0c843e16a7e244b2d1da718ba3b0ad2dd7e Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 6 Aug 2024 15:56:29 -0400 Subject: [PATCH] refactor: Lint --- HepLean/SpaceTime/LorentzTensor/Basic.lean | 16 +++++--- .../SpaceTime/LorentzTensor/Contraction.lean | 39 +++++++++++-------- .../LorentzTensor/IndexNotation/Basic.lean | 5 +-- .../IndexNotation/IndexListColor.lean | 8 ++-- .../IndexNotation/TensorIndex.lean | 2 +- .../LorentzTensor/Real/IndexNotation.lean | 21 +++++----- .../LorentzTensor/RisingLowering.lean | 4 +- 7 files changed, 52 insertions(+), 43 deletions(-) diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean index 0807543..7950fa1 100644 --- a/HepLean/SpaceTime/LorentzTensor/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean @@ -105,11 +105,15 @@ variable {𝓒 : TensorColor} [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] variable (cX : ColorMap 𝓒 X) (cY : ColorMap 𝓒 Y) (cZ : ColorMap 𝓒 Z) +/-- A relation, given an equivalence of types, between ColorMap which is true + if related by composition of the equivalence. -/ def MapIso (e : X ≃ Y) (cX : ColorMap 𝓒 X) (cY : ColorMap 𝓒 Y) : Prop := cX = cY ∘ e +/-- The sum of two color maps, formed by `Sum.elim`. -/ def sum (cX : ColorMap 𝓒 X) (cY : ColorMap 𝓒 Y) : ColorMap 𝓒 (Sum X Y) := Sum.elim cX cY +/-- The dual of a color map, formed by composition with `𝓒.Ο„`. -/ def dual (cX : ColorMap 𝓒 X) : ColorMap 𝓒 X := 𝓒.Ο„ ∘ cX namespace MapIso @@ -127,7 +131,7 @@ lemma trans (h : cX.MapIso e cY) (h' : cY.MapIso e' cZ) : subst h h' simp -lemma sum {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX.MapIso eX cX') (hY : cY.MapIso eY cY') : +lemma sum {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX.MapIso eX cX') (hY : cY.MapIso eY cY') : (cX.sum cY).MapIso (eX.sumCongr eY) (cX'.sum cY') := by funext x subst hX hY @@ -136,7 +140,7 @@ lemma sum {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX.MapIso eX cX') (hY : cY.MapI | Sum.inr x => rfl lemma dual {e : X ≃ Y} (h : cX.MapIso e cY) : - cX.dual.MapIso e cY.dual := by + cX.dual.MapIso e cY.dual := by subst h rfl @@ -569,9 +573,10 @@ lemma tensoratorEquiv_tmul_tprod (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor c @[simp] lemma tensoratorEquiv_symm_tprod (f : 𝓣.PureTensor (Sum.elim cX cY)) : (𝓣.tensoratorEquiv cX cY).symm ((PiTensorProduct.tprod R) f) = - (PiTensorProduct.tprod R) (𝓣.inlPureTensor f) βŠ—β‚œ[R] (PiTensorProduct.tprod R) (𝓣.inrPureTensor f) := by + (PiTensorProduct.tprod R) (𝓣.inlPureTensor f) βŠ—β‚œ[R] + (PiTensorProduct.tprod R) (𝓣.inrPureTensor f) := by simp [tensoratorEquiv, tensorator] - change (PiTensorProduct.lift 𝓣.domCoprod) ((PiTensorProduct.tprod R) f) = _ + change (PiTensorProduct.lift 𝓣.domCoprod) ((PiTensorProduct.tprod R) f) = _ simp [domCoprod] @[simp] @@ -669,11 +674,12 @@ lemma contrDual_symm_contrRightAux_apply_tmul (h : Ξ½ = Ξ·) -/ +/-- The equivalence between `𝓣.Tensor cX` and `R` when the indexing set `X` is empty. -/ def isEmptyEquiv [IsEmpty X] : 𝓣.Tensor cX ≃ₗ[R] R := PiTensorProduct.isEmptyEquiv X @[simp] -def isEmptyEquiv_tprod [IsEmpty X] (f : 𝓣.PureTensor cX) : +lemma isEmptyEquiv_tprod [IsEmpty X] (f : 𝓣.PureTensor cX) : 𝓣.isEmptyEquiv (PiTensorProduct.tprod R f) = 1 := by simp only [isEmptyEquiv] erw [PiTensorProduct.isEmptyEquiv_apply_tprod] diff --git a/HepLean/SpaceTime/LorentzTensor/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/Contraction.lean index 5479db3..d23f116 100644 --- a/HepLean/SpaceTime/LorentzTensor/Contraction.lean +++ b/HepLean/SpaceTime/LorentzTensor/Contraction.lean @@ -54,6 +54,8 @@ variable {𝓒 : TensorColor} [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] variable (cX : ColorMap 𝓒 X) (cY : ColorMap 𝓒 Y) (cZ : ColorMap 𝓒 Z) +/-- Given an equivalence `e` of types the condition that the color map `cX` is the dual to `cY` + up to this equivalence. -/ def ContrAll (e : X ≃ Y) (cX : ColorMap 𝓒 X) (cY : ColorMap 𝓒 Y) : Prop := cX = 𝓒.Ο„ ∘ cY ∘ e @@ -73,7 +75,7 @@ lemma symm (h : cX.ContrAll e cY) : cY.ContrAll e.symm cX := by exact (𝓒.Ο„_involutive (cY x)).symm lemma trans_mapIso {e : X ≃ Y} {e' : Z ≃ Y} - (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cY) : cX.ContrAll (e.trans e'.symm) cZ := by + (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cY) : cX.ContrAll (e.trans e'.symm) cZ := by subst h h' funext x simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply] @@ -86,21 +88,30 @@ lemma mapIso_trans {e : X ≃ Y} {e' : Z ≃ X} end ContrAll +/-- Given an equivalence `(C βŠ• C) βŠ• P ≃ X` the restriction of a color map `cX` on to `P`. -/ def contr (e : (C βŠ• C) βŠ• P ≃ X) (cX : ColorMap 𝓒 X) : ColorMap 𝓒 P := cX ∘ e ∘ Sum.inr +/-- Given an equivalence `(C βŠ• C) βŠ• P ≃ X` the restriction of a color map `cX` on `X` + to the first `C`. -/ def contrLeft (e : (C βŠ• C) βŠ• P ≃ X) (cX : ColorMap 𝓒 X) : ColorMap 𝓒 C := cX ∘ e ∘ Sum.inl ∘ Sum.inl +/-- Given an equivalence `(C βŠ• C) βŠ• P ≃ X` the restriction of a color map `cX` on `X` + to the second `C`. -/ def contrRight (e : (C βŠ• C) βŠ• P ≃ X) (cX : ColorMap 𝓒 X) : ColorMap 𝓒 C := cX ∘ e ∘ Sum.inl ∘ Sum.inr +/-- Given an equivalence `(C βŠ• C) βŠ• P ≃ X` the condition on `cX` so that we contract + the `C`'s under this equivalence. -/ def ContrCond (e : (C βŠ• C) βŠ• P ≃ X) (cX : ColorMap 𝓒 X) : Prop := cX ∘ e ∘ Sum.inl ∘ Sum.inl = 𝓒.Ο„ ∘ cX ∘ e ∘ Sum.inl ∘ Sum.inr namespace ContrCond -variable {e : (C βŠ• C) βŠ• P ≃ X} {e' : Y ≃ Z} {cX : ColorMap 𝓒 X} {cY : ColorMap 𝓒 Y} {cZ : ColorMap 𝓒 Z} +variable {e : (C βŠ• C) βŠ• P ≃ X} {e' : Y ≃ Z} {cX : ColorMap 𝓒 X} {cY : ColorMap 𝓒 Y} + {cZ : ColorMap 𝓒 Z} + variable {cX' : ColorMap 𝓒 X'} {cY' : ColorMap 𝓒 Y'} lemma to_contrAll (h : cX.ContrCond e) : @@ -189,7 +200,7 @@ lemma contrAll'_tmul_tprod_tprod (fx : (i : X) β†’ 𝓣.ColorModule (cX i)) MultilinearMap.mkPiAlgebra_apply] @[simp] -lemma contrAll'_isEmpty_tmul [IsEmpty X] (x : 𝓣.Tensor cX) (y : 𝓣.Tensor (𝓣.Ο„ ∘ cX)) : +lemma contrAll'_isEmpty_tmul [IsEmpty X] (x : 𝓣.Tensor cX) (y : 𝓣.Tensor (𝓣.Ο„ ∘ cX)) : 𝓣.contrAll' (x βŠ—β‚œ y) = 𝓣.isEmptyEquiv x * 𝓣.isEmptyEquiv y := by refine PiTensorProduct.induction_on' x ?_ (by intro a b hx hy @@ -211,7 +222,6 @@ lemma contrAll'_isEmpty_tmul [IsEmpty X] (x : 𝓣.Tensor cX) (y : 𝓣.Tensor MultilinearMap.mkPiAlgebra_apply, Finset.univ_eq_empty, Finset.prod_empty] erw [isEmptyEquiv_tprod] - @[simp] lemma contrAll'_mapIso (e : X ≃ Y) (h : cX.MapIso e cY) : 𝓣.contrAll' βˆ˜β‚— @@ -235,13 +245,13 @@ lemma contrAll'_mapIso (e : X ≃ Y) (h : cX.MapIso e cY) : LinearEquiv.refl_apply, smul_eq_mul, smul_tmul] apply congrArg apply congrArg - erw [contrAll'_tmul_tprod_tprod ] + erw [contrAll'_tmul_tprod_tprod] erw [TensorProduct.congr_tmul] simp only [PiTensorProduct.lift.tprod, LinearEquiv.refl_apply] erw [mapIso_tprod] erw [contrAll'_tmul_tprod_tprod] rw [mkPiAlgebra_equiv e] - simp only [ Equiv.symm_symm_apply, LinearMap.coe_comp, + simp only [Equiv.symm_symm_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, PiTensorProduct.reindex_tprod, PiTensorProduct.lift.tprod] apply congrArg @@ -278,17 +288,16 @@ lemma contrAll_tmul (e : X ≃ Y) (h : cX.ContrAll e cY) (x : 𝓣.Tensor cX) (y @[simp] lemma contrAll_mapIso_right_tmul (e : X ≃ Y) (e' : Z ≃ Y) - (h : c.ContrAll e cY ) (h' : cZ.MapIso e' cY) (x : 𝓣.Tensor c) (z : 𝓣.Tensor cZ) : + (h : c.ContrAll e cY) (h' : cZ.MapIso e' cY) (x : 𝓣.Tensor c) (z : 𝓣.Tensor cZ) : 𝓣.contrAll e h (x βŠ—β‚œ[R] 𝓣.mapIso e' h' z) = 𝓣.contrAll (e.trans e'.symm) (h.trans_mapIso h') (x βŠ—β‚œ[R] z) := by - simp only [contrAll_tmul, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul, - LinearEquiv.refl_apply, mapIso_mapIso] + simp only [contrAll_tmul, mapIso_mapIso] apply congrArg rfl @[simp] lemma contrAll_comp_mapIso_right (e : X ≃ Y) (e' : Z ≃ Y) - (h : c.ContrAll e cY ) (h' : cZ.MapIso e' cY) : 𝓣.contrAll e h βˆ˜β‚— + (h : c.ContrAll e cY) (h' : cZ.MapIso e' cY) : 𝓣.contrAll e h βˆ˜β‚— (TensorProduct.congr (LinearEquiv.refl R (𝓣.Tensor c)) (𝓣.mapIso e' h')).toLinearMap = 𝓣.contrAll (e.trans e'.symm) (h.trans_mapIso h') := by apply TensorProduct.ext' @@ -297,16 +306,15 @@ lemma contrAll_comp_mapIso_right (e : X ≃ Y) (e' : Z ≃ Y) @[simp] lemma contrAll_mapIso_left_tmul {e : X ≃ Y} {e' : Z ≃ X} - (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX ) (x : 𝓣.Tensor cZ) (y : 𝓣.Tensor cY) : + (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX) (x : 𝓣.Tensor cZ) (y : 𝓣.Tensor cY) : 𝓣.contrAll e h (𝓣.mapIso e' h' x βŠ—β‚œ[R] y) = 𝓣.contrAll (e'.trans e) (h.mapIso_trans h') (x βŠ—β‚œ[R] y) := by - simp only [contrAll_tmul, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul, - LinearEquiv.refl_apply, contrAll'_mapIso_tmul, mapIso_mapIso] + simp only [contrAll_tmul, contrAll'_mapIso_tmul, mapIso_mapIso] rfl @[simp] lemma contrAll_mapIso_left {e : X ≃ Y} {e' : Z ≃ X} - (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX ) : + (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX) : 𝓣.contrAll e h βˆ˜β‚— (TensorProduct.congr (𝓣.mapIso e' h') (LinearEquiv.refl R (𝓣.Tensor cY))).toLinearMap = 𝓣.contrAll (e'.trans e) (h.mapIso_trans h') := by @@ -375,7 +383,6 @@ lemma contrAll_rep (e : X ≃ Y) (h : cX.ContrAll e cY) (g : G) : nth_rewrite 2 [← contrDual_inv (cX x) g] rfl - @[simp] lemma contrAll_rep_apply {c : X β†’ 𝓣.Color} {d : Y β†’ 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.Ο„ ∘ d ∘ e) (g : G) (x : 𝓣.Tensor c βŠ— 𝓣.Tensor d) : @@ -397,7 +404,7 @@ lemma contrAll_rep_tmul {c : X β†’ 𝓣.Color} {d : Y β†’ 𝓣.Color} (e : X ≃ -/ lemma contr_cond (e : (C βŠ• C) βŠ• P ≃ X) : - cX.MapIso e.symm (Sum.elim (Sum.elim (cX.contrLeft e) (cX.contrRight e)) (cX.contr e)):= by + cX.MapIso e.symm (Sum.elim (Sum.elim (cX.contrLeft e) (cX.contrRight e)) (cX.contr e)) := by rw [TensorColor.ColorMap.MapIso, Equiv.eq_comp_symm] funext x match x with diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean index c5a6cba..35b9810 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean @@ -376,7 +376,7 @@ lemma hasNoContr_noContrFinset_card (h : l.HasNoContr) : l.noContrFinset.card = List.length l := by simp only [noContrFinset] rw [Finset.filter_true_of_mem] - simp + simp only [Finset.card_univ, Fintype.card_fin] intro x _ exact h x @@ -456,8 +456,7 @@ instance : Fintype l.contrPairSet := setFintype _ lemma contrPairSet_isEmpty_of_hasNoContr (h : l.HasNoContr) : IsEmpty l.contrPairSet := by simp only [contrPairSet, Subtype.coe_lt_coe, Set.coe_setOf, isEmpty_subtype, not_and, Prod.forall] - refine fun a b h' => h a.1 b.1 (Fin.ne_of_lt h') - + refine fun a b h' => h a.1 b.1 (Fin.ne_of_lt h') lemma getDual_lt_self_mem_contrPairSet {i : l.contrSubtype} (h : (l.getDual i).1 < i.1) : (l.getDual i, i) ∈ l.contrPairSet := diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean index 9c247ce..59fac34 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean @@ -56,7 +56,7 @@ lemma indexListColorProp_of_hasNoContr {s : IndexList 𝓒.Color} (h : s.HasNoCo -/ /-- The bool which is true if ever index appears at most once in the first element of entries of - `l.contrPairList`. I.e. If every element contracts with at most one other element. -/ + `l.contrPairList`. I.e. If every element contracts with at most one other element. -/ def colorPropFstBool (l : IndexList 𝓒.Color) : Bool := let l' := List.product l.contrPairList l.contrPairList let l'' := l'.filterMap fun (i, j) => if i.1 = j.1 ∧ i.2 β‰  j.2 then some i else none @@ -197,13 +197,11 @@ lemma splitContr_symm_apply_of_hasNoContr (h : l.1.HasNoContr) (x : Fin (l.1.noC simp [splitContr, noContrSubtypeEquiv, noContrFinset] trans (Finset.univ.orderEmbOfFin (by rw [l.1.hasNoContr_noContrFinset_card h]; simp)) x congr - rw [Finset.filter_true_of_mem (fun x _ => h x )] + rw [Finset.filter_true_of_mem (fun x _ => h x)] rw [@Finset.orderEmbOfFin_apply] simp only [List.get_eq_getElem, Fin.sort_univ, List.getElem_finRange] rfl - - /-! ## The contracted index list @@ -388,7 +386,7 @@ lemma of_contr_eq {s1 s2 : IndexListColor 𝓒} (hc : s1.contr = s2.contr) : PermContr s1 s2 := by simp [PermContr] rw [hc] - simp + simp only [List.Perm.refl, true_and] refine hasNoContr_color_eq_of_id_eq s2.contr.1 (s2.1.contrIndexList_hasNoContr) lemma toEquiv_contr_eq {s1 s2 : IndexListColor 𝓒} (hc : s1.contr = s2.contr) : diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean index b55ee19..e75c89b 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean @@ -62,7 +62,7 @@ lemma index_eq_of_eq {T₁ Tβ‚‚ : 𝓣.TensorIndex} (h : T₁ = Tβ‚‚) : T₁.ind cases h rfl lemma tensor_eq_of_eq {T₁ Tβ‚‚ : 𝓣.TensorIndex} (h : T₁ = Tβ‚‚) : T₁.tensor = - 𝓣.mapIso (Fin.castOrderIso (by rw [index_eq_of_eq h])).toEquiv + 𝓣.mapIso (Fin.castOrderIso (by rw [index_eq_of_eq h])).toEquiv (index_eq_colorMap_eq (index_eq_of_eq h)) Tβ‚‚.tensor := by have hi := index_eq_of_eq h cases T₁ diff --git a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean index 78eeeb1..4c9261f 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean @@ -15,7 +15,6 @@ to define the index notation for real Lorentz tensors. -/ - instance : IndexNotation realTensorColor.Color where charList := {'ᡘ', 'α΅€'} notaEquiv := @@ -76,7 +75,7 @@ noncomputable def fromIndexStringColor {cn : Fin n β†’ realTensorColor.Color} (T : (realLorentzTensor d).Tensor cn) (s : String) (hs : listCharIndexStringBool realTensorColor.Color s.toList = true) (hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)).length) - (hc : IndexListColor.colorPropBool (IndexString.toIndexList ⟨s, hs⟩)) + (hc : IndexListColor.colorPropBool (IndexString.toIndexList ⟨s, hs⟩)) (hd : TensorColor.ColorMap.DualMap.boolFin (IndexString.toIndexList ⟨s, hs⟩).colorMap (cn ∘ Fin.cast hn.symm)) : (realLorentzTensor d).TensorIndex := @@ -88,17 +87,17 @@ noncomputable def fromIndexStringColor {cn : Fin n β†’ realTensorColor.Color} /-- A tactics used to prove `colorPropBool` for real Lorentz tensors. -/ macro "prodTactic" : tactic => `(tactic| { - change @IndexListColor.colorPropBool realTensorColor _ _ _ - simp only [toTensorColor_eq, indexNotation_eq_color, fromIndexStringColor, mkDualMap, - String.toList, ↓Char.isValue, Equiv.coe_refl, Function.comp_apply, id_eq, ne_eq, - Function.comp_id, RelIso.coe_fn_toEquiv, prod_index, IndexListColor.prod] - rfl}) + change @IndexListColor.colorPropBool realTensorColor _ _ _ + simp only [toTensorColor_eq, indexNotation_eq_color, fromIndexStringColor, mkDualMap, + String.toList, ↓Char.isValue, Equiv.coe_refl, Function.comp_apply, id_eq, ne_eq, + Function.comp_id, RelIso.coe_fn_toEquiv, prod_index, IndexListColor.prod] + rfl}) /-- A tactic used to prove `boolFin` for real Lornetz tensors. -/ macro "dualMapTactic" : tactic => `(tactic| { - simp only [String.toList, ↓Char.isValue, toTensorColor_eq] - rfl}) + simp only [String.toList, ↓Char.isValue, toTensorColor_eq] + rfl}) /-- Notation for the construction of a tensor index from a tensor and a string. Conditions are checked automatically. -/ @@ -110,10 +109,10 @@ notation:10 T "βŠ—α΅€" S:11 => TensorIndex.prod T S (IndexListColor.colorPropBoo /-- An example showing the allowed constructions. -/ example (T : (realLorentzTensor d).Tensor ![ColorType.up, ColorType.down]) : True := by - let _ := T|"ᡀ₁ᡀ₂" + let _ := T|"ᡀ₁ᡀ₂" let _ := T|"α΅˜Β³α΅€β‚„" let _ := T|"ᡀ₁ᡀ₂" βŠ—α΅€ T|"α΅˜Β³α΅€β‚„" - let _ := T|"ᡀ₁ᡀ₂" βŠ—α΅€ T|"α΅˜Β³α΅€β‚„" βŠ—α΅€ T|"ᡘ¹ᡘ²" βŠ—α΅€ T|"α΅˜β΄α΅€β‚ƒ" + let _ := T|"ᡀ₁ᡀ₂" βŠ—α΅€ T|"α΅˜Β³α΅€β‚„" βŠ—α΅€ T|"ᡘ¹ᡘ²" βŠ—α΅€ T|"α΅˜β΄α΅€β‚ƒ" exact trivial end realLorentzTensor diff --git a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean index d663923..d4d64c4 100644 --- a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean +++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean @@ -19,7 +19,6 @@ noncomputable section open TensorProduct - namespace TensorColor variable {𝓒 : TensorColor} [DecidableEq 𝓒.Color] [Fintype 𝓒.Color] @@ -38,6 +37,8 @@ namespace ColorMap variable (cX : 𝓒.ColorMap X) +/-- Given an equivalence `C βŠ• P ≃ X` the color map obtained by `cX` by dualising + all indices in `C`. -/ def partDual (e : C βŠ• P ≃ X) : 𝓒.ColorMap X := (Sum.elim (𝓒.Ο„ ∘ cX ∘ e ∘ Sum.inl) (cX ∘ e ∘ Sum.inr) ∘ e.symm) @@ -117,7 +118,6 @@ end DualMap end ColorMap end TensorColor - variable {R : Type} [CommSemiring R] namespace TensorStructure