From 5dfd29ab8dfaab854759fc63fda01e2fe343b416 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 10 Dec 2024 13:44:39 +0000 Subject: [PATCH 1/5] chore: Bump to 4.14.0 --- HepLean/AnomalyCancellation/SM/Basic.lean | 2 +- .../TwoHDM/GaugeOrbits.lean | 6 +- .../ComplexTensor/PauliMatrices/Basis.lean | 8 +- HepLean/Lorentz/Group/Basic.lean | 6 +- HepLean/Lorentz/RealVector/Contraction.lean | 4 +- HepLean/Lorentz/RealVector/Modules.lean | 4 +- HepLean/Mathematics/LinearMaps.lean | 2 +- HepLean/Mathematics/PiTensorProduct.lean | 32 ++--- HepLean/Mathematics/SO3/Basic.lean | 11 +- HepLean/Meta/TransverseTactics.lean | 2 +- HepLean/StandardModel/HiggsBoson/Basic.lean | 25 ++-- .../StandardModel/HiggsBoson/GaugeAction.lean | 21 ++- .../HiggsBoson/PointwiseInnerProd.lean | 8 +- .../StandardModel/HiggsBoson/Potential.lean | 6 +- HepLean/Tensors/OverColor/Discrete.lean | 22 +-- HepLean/Tensors/OverColor/Functors.lean | 89 +++++++----- HepLean/Tensors/OverColor/Lift.lean | 91 +++++++----- HepLean/Tensors/TensorSpecies/Basic.lean | 44 +++--- .../TensorSpecies/Contractions/ContrMap.lean | 51 ++----- HepLean/Tensors/TensorSpecies/Pure.lean | 9 +- HepLean/Tensors/Tree/Basic.lean | 4 +- HepLean/Tensors/Tree/Elab.lean | 6 +- .../Tensors/Tree/NodeIdentities/Basic.lean | 6 +- .../Tree/NodeIdentities/PermContr.lean | 12 +- .../Tensors/Tree/NodeIdentities/PermProd.lean | 8 +- .../Tree/NodeIdentities/ProdAssoc.lean | 22 +-- .../Tensors/Tree/NodeIdentities/ProdComm.lean | 5 +- .../Tree/NodeIdentities/ProdContr.lean | 20 +-- README.md | 2 +- lake-manifest.json | 132 ++++++++++-------- lakefile.toml | 4 +- lean-toolchain | 2 +- 32 files changed, 354 insertions(+), 312 deletions(-) diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean index b0ab4360..07737f2f 100644 --- a/HepLean/AnomalyCancellation/SM/Basic.lean +++ b/HepLean/AnomalyCancellation/SM/Basic.lean @@ -141,7 +141,7 @@ lemma accSU2_ext {S T : (SMCharges n).Charges} AddHom.coe_mk] repeat erw [Finset.sum_add_distrib] repeat erw [← Finset.mul_sum] - exact Mathlib.Tactic.LinearCombination.add_pf (congrArg (HMul.hMul 3) (hj 0)) (hj 3) + exact Mathlib.Tactic.LinearCombination.add_eq_eq (congrArg (HMul.hMul 3) (hj 0)) (hj 3) /-- The `SU(3)` anomaly equations. -/ @[simp] diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean b/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean index e3438f88..f27d8051 100644 --- a/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean +++ b/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean @@ -75,11 +75,11 @@ lemma prodMatrix_hermitian (Φ1 Φ2 : HiggsField) (x : SpaceTime) : /-- The map `prodMatrix` is a smooth function on spacetime. -/ lemma prodMatrix_smooth (Φ1 Φ2 : HiggsField) : - Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, Matrix (Fin 2) (Fin 2) ℂ) (prodMatrix Φ1 Φ2) := by + ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, Matrix (Fin 2) (Fin 2) ℂ) ⊤ (prodMatrix Φ1 Φ2) := by rw [show 𝓘(ℝ, Matrix (Fin 2) (Fin 2) ℂ) = modelWithCornersSelf ℝ (Fin 2 → Fin 2 → ℂ) from rfl, - smooth_pi_space] + contMDiff_pi_space] intro i - rw [smooth_pi_space] + rw [contMDiff_pi_space] intro j fin_cases i <;> fin_cases j <;> simpa only [prodMatrix, Fin.zero_eta, Fin.isValue, of_apply, cons_val', cons_val_zero, diff --git a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean index 220a3a7c..e3c81c5c 100644 --- a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean +++ b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean @@ -334,7 +334,7 @@ def pauliCoMap := ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Co ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 1) lemma pauliMatrix_contr_down_0 : - (contr 1 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod + (contr 1 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun _ => 0)).prod (tensorNode pauliContr)))).tensor = basisVector pauliCoMap (fun | 0 => 0 | 1 => 0 | 2 => 0) + basisVector pauliCoMap (fun | 0 => 0 | 1 => 1 | 2 => 1) := by @@ -379,7 +379,7 @@ lemma pauliMatrix_contr_down_0 : fin_cases k <;> rfl lemma pauliMatrix_contr_down_1 : - {(basisVector ![Color.down, Color.down] fun x => 1) | ν μ ⊗ + {(basisVector ![Color.down, Color.down] fun _ => 1) | ν μ ⊗ pauliContr | μ α β}ᵀ.tensor = basisVector pauliCoMap (fun | 0 => 1 | 1 => 0 | 2 => 1) + basisVector pauliCoMap (fun | 0 => 1 | 1 => 1 | 2 => 0) := by @@ -424,7 +424,7 @@ lemma pauliMatrix_contr_down_1 : fin_cases k <;> rfl lemma pauliMatrix_contr_down_2 : - {(basisVector ![Color.down, Color.down] fun x => 2) | μ ν ⊗ + {(basisVector ![Color.down, Color.down] fun _ => 2) | μ ν ⊗ pauliContr | ν α β}ᵀ.tensor = (- I) • basisVector pauliCoMap (fun | 0 => 2 | 1 => 0 | 2 => 1) + (I) • basisVector pauliCoMap (fun | 0 => 2 | 1 => 1 | 2 => 0) := by @@ -464,7 +464,7 @@ lemma pauliMatrix_contr_down_2 : · decide lemma pauliMatrix_contr_down_3 : - {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗ + {(basisVector ![Color.down, Color.down] fun _ => 3) | μ ν ⊗ pauliContr | ν α β}ᵀ.tensor = basisVector pauliCoMap (fun | 0 => 3 | 1 => 0 | 2 => 0) + (- 1 : ℂ) • basisVector pauliCoMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by diff --git a/HepLean/Lorentz/Group/Basic.lean b/HepLean/Lorentz/Group/Basic.lean index 9f794eb9..983e7c1a 100644 --- a/HepLean/Lorentz/Group/Basic.lean +++ b/HepLean/Lorentz/Group/Basic.lean @@ -241,17 +241,19 @@ lemma toProd_continuous : Continuous (@toProd d) := by MulOpposite.continuous_op.comp' ((continuous_const.matrix_mul (continuous_iff_le_induced.mpr fun U a => a).matrix_transpose).matrix_mul continuous_const)⟩ +open Topology + /-- The embedding from the Lorentz Group into the monoid of matrices times the opposite of the monoid of matrices. -/ lemma toProd_embedding : IsEmbedding (@toProd d) where - inj := toProd_injective + injective := toProd_injective eq_induced := (isInducing_iff ⇑toProd).mp (IsInducing.of_comp toProd_continuous continuous_fst ((isInducing_iff (Prod.fst ∘ ⇑toProd)).mpr rfl)) /-- The embedding from the Lorentz Group into `GL (Fin 4) ℝ`. -/ lemma toGL_embedding : IsEmbedding (@toGL d).toFun where - inj := toGL_injective + injective := toGL_injective eq_induced := by refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) fun _ ↦ ?_).symm rw [TopologicalSpace.ext_iff.mp toProd_embedding.eq_induced _, isOpen_induced_iff, diff --git a/HepLean/Lorentz/RealVector/Contraction.lean b/HepLean/Lorentz/RealVector/Contraction.lean index dea83773..afbdc4b2 100644 --- a/HepLean/Lorentz/RealVector/Contraction.lean +++ b/HepLean/Lorentz/RealVector/Contraction.lean @@ -347,9 +347,7 @@ lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔ Action.FunctorCategoryEquivalence.functor_obj_obj, map_add, map_sub] at hp' hn' linear_combination (norm := ring_nf) (1 / 4) * hp' + (-1/ 4) * hn' rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] - simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V, - Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, - Action.FunctorCategoryEquivalence.functor_obj_obj, add_sub_cancel, neg_add_cancel, e] + ring /-! diff --git a/HepLean/Lorentz/RealVector/Modules.lean b/HepLean/Lorentz/RealVector/Modules.lean index b1abe71f..70318d53 100644 --- a/HepLean/Lorentz/RealVector/Modules.lean +++ b/HepLean/Lorentz/RealVector/Modules.lean @@ -197,7 +197,7 @@ def toSpace (v : ContrMod d) : EuclideanSpace ℝ (Fin d) := v.val ∘ Sum.inr /-- The representation of the Lorentz group acting on `ContrℝModule d`. -/ def rep : Representation ℝ (LorentzGroup d) (ContrMod d) where toFun g := Matrix.toLinAlgEquiv stdBasis g - map_one' := (MulEquivClass.map_eq_one_iff (Matrix.toLinAlgEquiv stdBasis)).mpr rfl + map_one' := EmbeddingLike.map_eq_one_iff.mpr rfl map_mul' x y := by simp only [lorentzGroupIsGroup_mul_coe, _root_.map_mul] @@ -283,6 +283,8 @@ lemma toSelfAdjoint_symm_basis (i : Fin 1 ⊕ Fin 3) : instance : TopologicalSpace (ContrMod d) := TopologicalSpace.induced ContrMod.toFin1dℝEquiv (Pi.topologicalSpace) +open Topology + lemma toFin1dℝEquiv_isInducing : IsInducing (@ContrMod.toFin1dℝEquiv d) := by exact { eq_induced := rfl } diff --git a/HepLean/Mathematics/LinearMaps.lean b/HepLean/Mathematics/LinearMaps.lean index 22b43fe8..d90caf39 100644 --- a/HepLean/Mathematics/LinearMaps.lean +++ b/HepLean/Mathematics/LinearMaps.lean @@ -71,7 +71,7 @@ def mk₂ (f : V × V → ℚ) (map_smul : ∀ a S T, f (a • S, T) = a * f (S, intro T1 T2 simp only rw [swap, map_add] - exact Mathlib.Tactic.LinearCombination.add_pf (swap T1 S) (swap T2 S) + exact Mathlib.Tactic.LinearCombination.add_eq_eq (swap T1 S) (swap T2 S) map_smul' := by intro a T simp only [eq_ratCast, Rat.cast_eq_id, id_eq, smul_eq_mul] diff --git a/HepLean/Mathematics/PiTensorProduct.lean b/HepLean/Mathematics/PiTensorProduct.lean index f5ca75d8..8bd92eac 100644 --- a/HepLean/Mathematics/PiTensorProduct.lean +++ b/HepLean/Mathematics/PiTensorProduct.lean @@ -223,7 +223,7 @@ def domCoprod : MultilinearMap R (Sum.elim s1 s2) ((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i) where toFun f := (PiTensorProduct.tprod R (pureInl f)) ⊗ₜ (PiTensorProduct.tprod R (pureInr f)) - map_add' f xy v1 v2 := by + map_update_add' f xy v1 v2 := by haveI : DecidableEq (ι1 ⊕ ι2) := inferInstance haveI : DecidableEq ι1 := @Function.Injective.decidableEq ι1 (ι1 ⊕ ι2) Sum.inl _ Sum.inl_injective @@ -231,12 +231,12 @@ def domCoprod : @Function.Injective.decidableEq ι2 (ι1 ⊕ ι2) Sum.inr _ Sum.inr_injective match xy with | Sum.inl xy => - simp only [Sum.elim_inl, pureInl_update_left, MultilinearMap.map_add, pureInr_update_left, ← - add_tmul] + simp only [Sum.elim_inl, pureInl_update_left, MultilinearMap.map_update_add, + pureInr_update_left, ← add_tmul] | Sum.inr xy => - simp only [Sum.elim_inr, pureInr_update_right, MultilinearMap.map_add, pureInl_update_right, ← - tmul_add] - map_smul' f xy r p := by + simp only [Sum.elim_inr, pureInl_update_right, pureInr_update_right, + MultilinearMap.map_update_add, ← tmul_add] + map_update_smul' f xy r p := by haveI : DecidableEq (ι1 ⊕ ι2) := inferInstance haveI : DecidableEq ι1 := @Function.Injective.decidableEq ι1 (ι1 ⊕ ι2) Sum.inl _ Sum.inl_injective @@ -244,11 +244,11 @@ def domCoprod : @Function.Injective.decidableEq ι2 (ι1 ⊕ ι2) Sum.inr _ Sum.inr_injective match xy with | Sum.inl x => - simp only [Sum.elim_inl, pureInl_update_left, MultilinearMap.map_smul, pureInr_update_left, - smul_tmul, tmul_smul] + simp only [Sum.elim_inl, pureInl_update_left, MultilinearMap.map_update_smul, + pureInr_update_left, smul_tmul, tmul_smul] | Sum.inr y => - simp only [Sum.elim_inr, pureInl_update_right, pureInr_update_right, MultilinearMap.map_smul, - tmul_smul] + simp only [Sum.elim_inr, pureInl_update_right, pureInr_update_right, + MultilinearMap.map_update_smul, tmul_smul] /-- Expand `PiTensorProduct` on sums into a `TensorProduct` of two factors. -/ def tmulSymm : (⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i) →ₗ[R] @@ -308,21 +308,21 @@ def elimPureTensorMulLin : MultilinearMap R s1 (MultilinearMap R s2 (⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i)) where toFun p := { toFun := fun q => PiTensorProduct.tprod R (elimPureTensor p q) - map_add' := fun m x v1 v2 => by + map_update_add' := fun m x v1 v2 => by haveI : DecidableEq ι2 := inferInstance haveI := Classical.decEq ι1 - simp only [elimPureTensor_update_right, MultilinearMap.map_add] - map_smul' := fun m x r v => by + simp only [elimPureTensor_update_right, MultilinearMap.map_update_add] + map_update_smul' := fun m x r v => by haveI : DecidableEq ι2 := inferInstance haveI := Classical.decEq ι1 - simp only [elimPureTensor_update_right, MultilinearMap.map_smul]} - map_add' p x v1 v2 := by + simp only [elimPureTensor_update_right, MultilinearMap.map_update_smul]} + map_update_add' p x v1 v2 := by haveI : DecidableEq ι1 := inferInstance haveI := Classical.decEq ι2 apply MultilinearMap.ext intro y simp - map_smul' p x r v := by + map_update_smul' p x r v := by haveI : DecidableEq ι1 := inferInstance haveI := Classical.decEq ι2 apply MultilinearMap.ext diff --git a/HepLean/Mathematics/SO3/Basic.lean b/HepLean/Mathematics/SO3/Basic.lean index 0b0aad0e..c879aff0 100644 --- a/HepLean/Mathematics/SO3/Basic.lean +++ b/HepLean/Mathematics/SO3/Basic.lean @@ -26,7 +26,10 @@ instance SO3Group : Group SO3 where by simp only [det_mul, A.2.1, B.2.1, mul_one], by - simp only [transpose_mul, ← Matrix.mul_assoc, Matrix.mul_assoc, B.2.2, mul_one, A.2.2]⟩ + simp only [transpose_mul, ← Matrix.mul_assoc, Matrix.mul_assoc, B.2.2, mul_one, A.2.2] + trans A.1 * ((B.1 * (B.1)ᵀ) * (A.1)ᵀ) + · noncomm_ring + · simp [Matrix.mul_assoc, B.2.2, mul_one, A.2.2]⟩ mul_assoc A B C := Subtype.eq (Matrix.mul_assoc A.1 B.1 C.1) one := ⟨1, det_one, by rw [transpose_one, mul_one]⟩ one_mul A := Subtype.eq (Matrix.one_mul A.1) @@ -81,16 +84,18 @@ lemma toProd_continuous : Continuous toProd := Continuous.comp' (MulOpposite.continuous_op) (Continuous.matrix_transpose (continuous_iff_le_induced.mpr fun _ a ↦ a))⟩ +open Topology + /-- The embedding of `SO(3)` into the monoid of matrices times the opposite of the monoid of matrices. -/ lemma toProd_embedding : IsEmbedding toProd where - inj := toProd_injective + injective := toProd_injective eq_induced := (isInducing_iff ⇑toProd).mp (IsInducing.of_comp toProd_continuous continuous_fst ((isInducing_iff (Prod.fst ∘ ⇑toProd)).mpr rfl)) /-- The embedding of `SO(3)` into `GL (Fin 3) ℝ`. -/ lemma toGL_embedding : IsEmbedding toGL.toFun where - inj := toGL_injective + injective := toGL_injective eq_induced := by refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) ?_).symm intro s diff --git a/HepLean/Meta/TransverseTactics.lean b/HepLean/Meta/TransverseTactics.lean index 9704690f..ec7ac871 100644 --- a/HepLean/Meta/TransverseTactics.lean +++ b/HepLean/Meta/TransverseTactics.lean @@ -70,7 +70,7 @@ def traverseForest (file : FilePath) let t := steps.map fun (env, infoState) ↦ (infoState.trees.toList.map fun t ↦ (Lean.Elab.InfoTree.foldInfo (visitInfo file env visitTacticInfo) [] t).reverse) - t.join.join + t.flatten.flatten end transverseTactics diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean index b6463b61..5e20e2b3 100644 --- a/HepLean/StandardModel/HiggsBoson/Basic.lean +++ b/HepLean/StandardModel/HiggsBoson/Basic.lean @@ -53,8 +53,8 @@ def toFin2ℂ : HiggsVec →L[ℝ] (Fin 2 → ℂ) where map_smul' a x := rfl /-- The map `toFin2ℂ` is smooth. -/ -lemma smooth_toFin2ℂ : Smooth 𝓘(ℝ, HiggsVec) 𝓘(ℝ, Fin 2 → ℂ) toFin2ℂ := - ContinuousLinearMap.smooth toFin2ℂ +lemma smooth_toFin2ℂ : ContMDiff 𝓘(ℝ, HiggsVec) 𝓘(ℝ, Fin 2 → ℂ) ⊤ toFin2ℂ := + ContinuousLinearMap.contMDiff toFin2ℂ /-- An orthonormal basis of `HiggsVec`. -/ def orthonormBasis : OrthonormalBasis (Fin 2) ℂ HiggsVec := @@ -92,7 +92,7 @@ instance : SmoothVectorBundle HiggsVec HiggsBundle SpaceTime.asSmoothManifold := Bundle.Trivial.smoothVectorBundle HiggsVec /-- A Higgs field is a smooth section of the Higgs bundle. -/ -abbrev HiggsField : Type := SmoothSection SpaceTime.asSmoothManifold HiggsVec HiggsBundle +abbrev HiggsField : Type := ContMDiffSection SpaceTime.asSmoothManifold HiggsVec ⊤ HiggsBundle /-- Given a vector in `HiggsVec` the constant Higgs field with value equal to that section. -/ @@ -101,7 +101,7 @@ def HiggsVec.toField (φ : HiggsVec) : HiggsField where contMDiff_toFun := by intro x rw [Bundle.contMDiffAt_section] - exact smoothAt_const + exact contMDiffAt_const /-- For all spacetime points, the constant Higgs field defined by a Higgs vector, returns that Higgs Vector. -/ @@ -120,7 +120,8 @@ open HiggsVec /-- Given a `HiggsField`, the corresponding map from `SpaceTime` to `HiggsVec`. -/ def toHiggsVec (φ : HiggsField) : SpaceTime → HiggsVec := φ -lemma toHiggsVec_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, HiggsVec) φ.toHiggsVec := by +lemma toHiggsVec_smooth (φ : HiggsField) : + ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, HiggsVec) ⊤ φ.toHiggsVec := by intro x0 have h1 := φ.contMDiff x0 rw [Bundle.contMDiffAt_section] at h1 @@ -138,20 +139,20 @@ lemma toFin2ℂ_comp_toHiggsVec (φ : HiggsField) : -/ -lemma toVec_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ := +lemma toVec_smooth (φ : HiggsField) : ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, Fin 2 → ℂ) ⊤ φ := smooth_toFin2ℂ.comp φ.toHiggsVec_smooth lemma apply_smooth (φ : HiggsField) : - ∀ i, Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℂ) (fun (x : SpaceTime) => (φ x i)) := - (smooth_pi_space).mp (φ.toVec_smooth) + ∀ i, ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℂ) ⊤ (fun (x : SpaceTime) => (φ x i)) := + (contMDiff_pi_space).mp (φ.toVec_smooth) lemma apply_re_smooth (φ : HiggsField) (i : Fin 2) : - Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (reCLM ∘ (fun (x : SpaceTime) => (φ x i))) := - (ContinuousLinearMap.smooth reCLM).comp (φ.apply_smooth i) + ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) ⊤ (reCLM ∘ (fun (x : SpaceTime) => (φ x i))) := + (ContinuousLinearMap.contMDiff reCLM).comp (φ.apply_smooth i) lemma apply_im_smooth (φ : HiggsField) (i : Fin 2) : - Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (imCLM ∘ (fun (x : SpaceTime) => (φ x i))) := - (ContinuousLinearMap.smooth imCLM).comp (φ.apply_smooth i) + ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) ⊤ (imCLM ∘ (fun (x : SpaceTime) => (φ x i))) := + (ContinuousLinearMap.contMDiff imCLM).comp (φ.apply_smooth i) /-! diff --git a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean index eb90dc15..4c58fb7e 100644 --- a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean +++ b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean @@ -124,14 +124,21 @@ lemma rotateMatrix_unitary {φ : HiggsVec} (hφ : φ ≠ 0) : erw [mul_fin_two, one_fin_two] have : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ) ext i j - fin_cases i <;> fin_cases j <;> field_simp - <;> rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq] - · simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add, + fin_cases i <;> fin_cases j + · field_simp + rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq] + simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add, Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm] - · ring_nf - · ring_nf - · simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add, - Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm] + · simp only [Fin.isValue, Fin.zero_eta, Fin.mk_one, of_apply, cons_val', cons_val_one, head_cons, + empty_val', cons_val_fin_one, cons_val_zero] + ring_nf + · simp only [Fin.isValue, Fin.mk_one, Fin.zero_eta, of_apply, cons_val', cons_val_zero, + empty_val', cons_val_fin_one, cons_val_one, head_fin_const] + ring_nf + · field_simp + rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq] + simp only [Fin.isValue, mul_comm, mul_conj, PiLp.inner_apply, Complex.inner, ofReal_re, + Fin.sum_univ_two, ofReal_add] /-- The `rotateMatrix` for a non-zero Higgs vector is special unitary. -/ lemma rotateMatrix_specialUnitary {φ : HiggsVec} (hφ : φ ≠ 0) : diff --git a/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean b/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean index 591a8879..1fb52dbd 100644 --- a/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean +++ b/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean @@ -91,9 +91,9 @@ lemma innerProd_expand (φ1 φ2 : HiggsField) : RCLike.im_to_complex, I_sq, mul_neg, mul_one, neg_mul, sub_neg_eq_add, one_mul] ring -lemma smooth_innerProd (φ1 φ2 : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℂ) ⟪φ1, φ2⟫_H := by +lemma smooth_innerProd (φ1 φ2 : HiggsField) : ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℂ) ⊤ ⟪φ1, φ2⟫_H := by rw [innerProd_expand] - exact (ContinuousLinearMap.smooth (equivRealProdCLM.symm : ℝ × ℝ →L[ℝ] ℂ)).comp $ + exact (ContinuousLinearMap.contMDiff (equivRealProdCLM.symm : ℝ × ℝ →L[ℝ] ℂ)).comp $ (((((φ1.apply_re_smooth 0).smul (φ2.apply_re_smooth 0)).add ((φ1.apply_re_smooth 1).smul (φ2.apply_re_smooth 1))).add ((φ1.apply_im_smooth 0).smul (φ2.apply_im_smooth 0))).add @@ -171,9 +171,9 @@ lemma normSq_zero (φ : HiggsField) (x : SpaceTime) : φ.normSq x = 0 ↔ φ x = simp [normSq, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero] /-- The norm squared of the Higgs field is a smooth function on space-time. -/ -lemma normSq_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) φ.normSq := by +lemma normSq_smooth (φ : HiggsField) : ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) ⊤ φ.normSq := by rw [normSq_expand] - refine Smooth.add ?_ ?_ + refine ContMDiff.add ?_ ?_ · simp only [mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add] exact ((φ.apply_re_smooth 0).smul (φ.apply_re_smooth 0)).add $ (φ.apply_im_smooth 0).smul (φ.apply_im_smooth 0) diff --git a/HepLean/StandardModel/HiggsBoson/Potential.lean b/HepLean/StandardModel/HiggsBoson/Potential.lean index 447c368e..5b5b9b73 100644 --- a/HepLean/StandardModel/HiggsBoson/Potential.lean +++ b/HepLean/StandardModel/HiggsBoson/Potential.lean @@ -50,10 +50,10 @@ def toFun (φ : HiggsField) (x : SpaceTime) : ℝ := /-- The potential is smooth. -/ lemma toFun_smooth (φ : HiggsField) : - Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (fun x => P.toFun φ x) := by + ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) ⊤ (fun x => P.toFun φ x) := by simp only [toFun, normSq, neg_mul] - exact (smooth_const.smul φ.normSq_smooth).neg.add - ((smooth_const.smul φ.normSq_smooth).smul φ.normSq_smooth) + exact (contMDiff_const.smul φ.normSq_smooth).neg.add + ((contMDiff_const.smul φ.normSq_smooth).smul φ.normSq_smooth) /-- The Higgs potential formed by negating the mass squared and the quartic coupling. -/ def neg : Potential where diff --git a/HepLean/Tensors/OverColor/Discrete.lean b/HepLean/Tensors/OverColor/Discrete.lean index 65c7ae8a..f47620bc 100644 --- a/HepLean/Tensors/OverColor/Discrete.lean +++ b/HepLean/Tensors/OverColor/Discrete.lean @@ -33,7 +33,7 @@ def pair : Discrete C ⥤ Rep k G := F ⊗ F def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverColor.mk ![c,c]) := by symm apply ((lift.obj F).mapIso fin2Iso).trans - apply ((lift.obj F).μIso _ _).symm.trans + apply (Functor.Monoidal.μIso (lift.obj F).toFunctor _ _).symm.trans apply tensorIso ?_ ?_ · symm apply (forgetLiftApp F c).symm.trans @@ -54,7 +54,7 @@ def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) (lift.obj F).obj (OverColor.mk ![c1,c2]) := by symm apply ((lift.obj F).mapIso fin2Iso).trans - apply ((lift.obj F).μIso _ _).symm.trans + apply (Functor.Monoidal.μIso (lift.obj F).toFunctor _ _).symm.trans apply tensorIso ?_ ?_ · symm apply (forgetLiftApp F c1).symm.trans @@ -76,16 +76,16 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr pairIsoSep, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, forgetLiftApp, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_assoc, Iso.trans_hom, Iso.symm_hom, tensorIso_inv, Iso.trans_inv, Iso.symm_inv, Functor.mapIso_hom, tensor_comp, - MonoidalFunctor.μIso_hom, Functor.mapIso_inv, Category.assoc, - LaxMonoidalFunctor.μ_natural_assoc, Action.comp_hom, Action.instMonoidalCategory_tensorHom_hom, - Action.mkIso_inv_hom, LinearEquiv.toModuleIso_inv, Equivalence.symm_inverse, - Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, - ModuleCat.coe_comp, Function.comp_apply, ModuleCat.MonoidalCategory.tensorHom_tmul, - Functor.id_obj] + Functor.Monoidal.μIso_hom, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, Functor.mapIso_inv, + Category.assoc, Functor.LaxMonoidal.μ_natural_assoc, Action.comp_hom, + Action.instMonoidalCategory_tensorHom_hom, Action.mkIso_inv_hom, LinearEquiv.toModuleIso_inv, + Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, + Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply, + ModuleCat.MonoidalCategory.tensorHom_tmul, mk_hom, mk_left, Functor.id_obj] erw [forgetLiftAppV_symm_apply F c1, forgetLiftAppV_symm_apply F c2] change ((lift.obj F).map fin2Iso.inv).hom (((lift.obj F).map ((mkIso _).hom ⊗ (mkIso _).hom)).hom - (((lift.obj F).μ (mk fun _ => c1) (mk fun _ => c2)).hom + ((Functor.LaxMonoidal.μ (lift.obj F).toFunctor (mk fun _ => c1) (mk fun _ => c2)).hom (((PiTensorProduct.tprod k) fun _ => x) ⊗ₜ[k] (PiTensorProduct.tprod k) fun _ => y))) = _ rw [lift.obj_μ_tprod_tmul F (mk fun _ => c1) (mk fun _ => c2)] change ((lift.obj F).map fin2Iso.inv).hom @@ -209,7 +209,7 @@ def tripleIsoSep {c1 c2 c3 : C} : (lift.obj F).obj (OverColor.mk ![c1,c2,c3]) := (whiskerLeftIso (F.obj (Discrete.mk c1)) (pairIsoSep F (c1 := c2) (c2 := c3))).trans <| (whiskerRightIso (forgetLiftApp F c1).symm _).trans <| - ((lift.obj F).μIso _ _).trans <| + ((Functor.Monoidal.μIso (lift.obj F).toFunctor) _ _).trans <| (lift.obj F).mapIso fin3Iso'.symm lemma tripleIsoSep_tmul {c1 c2 c3 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discrete.mk c2)) @@ -218,7 +218,7 @@ lemma tripleIsoSep_tmul {c1 c2 c3 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj ( (fun | (0 : Fin 3) => x | (1 : Fin 3) => y | (2 : Fin 3) => z) := by simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Action.instMonoidalCategory_tensorObj_V, tripleIsoSep, Functor.mapIso_symm, Iso.trans_hom, whiskerLeftIso_hom, whiskerRightIso_hom, - Iso.symm_hom, MonoidalFunctor.μIso_hom, Functor.mapIso_inv, Action.comp_hom, + Iso.symm_hom, Functor.mapIso_inv, Action.comp_hom, Action.instMonoidalCategory_whiskerLeft_hom, Action.instMonoidalCategory_whiskerRight_hom, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply, diff --git a/HepLean/Tensors/OverColor/Functors.lean b/HepLean/Tensors/OverColor/Functors.lean index d2431eb8..8de5d4f3 100644 --- a/HepLean/Tensors/OverColor/Functors.lean +++ b/HepLean/Tensors/OverColor/Functors.lean @@ -16,58 +16,65 @@ open MonoidalCategory /-- The monoidal functor from `OverColor C` to `OverColor D` constructed from a map `f : C → D`. -/ -def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D) where - toFunctor := Core.functorToCore (Core.inclusion (Over C) ⋙ (Over.map f)) - ε := Over.isoMk (Iso.refl _) (by +def map {C D : Type} (f : C → D) : Functor (OverColor C) (OverColor D) := + Core.functorToCore (Core.inclusion (Over C) ⋙ (Over.map f)) + +instance map_laxMonoidal {C D : Type} (f : C → D) : Functor.LaxMonoidal (map f) where + ε' := Over.isoMk (Iso.refl _) (by ext x exact Empty.elim x) - μ X Y := Over.isoMk (Iso.refl _) (by + μ' := fun X Y => Over.isoMk (Iso.refl _) (by ext x match x with | Sum.inl x => rfl | Sum.inr x => rfl) - μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + μ'_natural_left := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by rfl - μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + μ'_natural_right := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by rfl - associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + associativity' := fun X Y Z => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl (Sum.inl x) => rfl | Sum.inl (Sum.inr x) => rfl | Sum.inr x => rfl - left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + left_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl x => rfl | Sum.inr x => rfl - right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + right_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl x => rfl | Sum.inr x => rfl +noncomputable instance map_monoidal {C D : Type} (f : C → D) : Functor.Monoidal (map f) := + Functor.Monoidal.ofLaxMonoidal _ + /-- The tensor product on `OverColor C` as a monoidal functor. -/ -def tensor (C : Type) : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where - toFunctor := MonoidalCategory.tensor (OverColor C) - ε := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso rfl - μ X Y := Over.isoMk (Equiv.sumSumSumComm X.1.left X.2.left Y.1.left Y.2.left).toIso (by +def tensor (C : Type) : Functor (OverColor C × OverColor C) (OverColor C) := + MonoidalCategory.tensor (OverColor C) + +instance tensor_laxMonoidal (C : Type) : Functor.LaxMonoidal (tensor C) where + ε' := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso rfl + μ' := fun X Y => Over.isoMk (Equiv.sumSumSumComm X.1.left X.2.left Y.1.left Y.2.left).toIso (by ext x match x with | Sum.inl (Sum.inl x) => rfl | Sum.inl (Sum.inr x) => rfl | Sum.inr (Sum.inl x) => rfl | Sum.inr (Sum.inr x) => rfl) - μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + μ'_natural_left := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl (Sum.inl x) => rfl | Sum.inl (Sum.inr x) => rfl | Sum.inr (Sum.inl x) => rfl | Sum.inr (Sum.inr x) => rfl - μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + μ'_natural_right := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl (Sum.inl x) => rfl | Sum.inl (Sum.inr x) => rfl | Sum.inr (Sum.inl x) => rfl | Sum.inr (Sum.inr x) => rfl - associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + associativity' := fun X Y Z => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl (Sum.inl (Sum.inl x)) => rfl | Sum.inl (Sum.inl (Sum.inr x)) => rfl @@ -75,52 +82,60 @@ def tensor (C : Type) : MonoidalFunctor (OverColor C × OverColor C) (OverColor | Sum.inl (Sum.inr (Sum.inr x)) => rfl | Sum.inr (Sum.inl x) => rfl | Sum.inr (Sum.inr x) => rfl - left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + left_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl x => exact Empty.elim x | Sum.inr (Sum.inl x)=> rfl | Sum.inr (Sum.inr x)=> rfl - right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + right_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl (Sum.inl x) => rfl | Sum.inl (Sum.inr x) => rfl | Sum.inr x => exact Empty.elim x -/-- The monoidal functor from `OverColor C` to `OverColor C × OverColor C` landing on the - diagonal. -/ -def diag (C : Type) : MonoidalFunctor (OverColor C) (OverColor C × OverColor C) := - MonoidalFunctor.diag (OverColor C) +noncomputable instance tensor_monoidal (C : Type) : Functor.Monoidal (tensor C) := + Functor.Monoidal.ofLaxMonoidal _ /-- The constant monoidal functor from `OverColor C` to itself landing on `𝟙_ (OverColor C)`. -/ -def const (C : Type) : MonoidalFunctor (OverColor C) (OverColor C) where - toFunctor := (Functor.const (OverColor C)).obj (𝟙_ (OverColor C)) - ε := 𝟙 (𝟙_ (OverColor C)) - μ _ _:= (λ_ (𝟙_ (OverColor C))).hom - μ_natural_left _ _ := by +def const (C : Type) : Functor (OverColor C) (OverColor C) := + (Functor.const (OverColor C)).obj (𝟙_ (OverColor C)) + +instance const_laxMonoidal (C : Type) : Functor.LaxMonoidal (const C) where + ε' := 𝟙 (𝟙_ (OverColor C)) + μ' := fun _ _ => (λ_ (𝟙_ (OverColor C))).hom + μ'_natural_left := fun _ _ => by simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerRight_id, - Category.id_comp, Iso.hom_inv_id, Category.comp_id] - μ_natural_right _ _ := by + Category.id_comp, Iso.hom_inv_id, Category.comp_id, const] + μ'_natural_right := fun _ _ => by simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerLeft_id, - Category.id_comp, Category.comp_id] - associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by + Category.id_comp, Category.comp_id, const] + associativity' := fun X Y Z => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by match i with | Sum.inl (Sum.inl i) => rfl | Sum.inl (Sum.inr i) => rfl | Sum.inr i => rfl - left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by + left_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by match i with | Sum.inl i => exact Empty.elim i | Sum.inr i => exact Empty.elim i - right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by + right_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by match i with | Sum.inl i => exact Empty.elim i | Sum.inr i => exact Empty.elim i +noncomputable instance const_monoidal (C : Type) : Functor.Monoidal (const C) := + Functor.Monoidal.ofLaxMonoidal _ + /-- The monoidal functor from `OverColor C` to `OverColor C` taking `f` to `f ⊗ τ_* f`. -/ -def contrPair (C : Type) (τ : C → C) : MonoidalFunctor (OverColor C) (OverColor C) := - OverColor.diag C - ⊗⋙ (MonoidalFunctor.prod (MonoidalFunctor.id (OverColor C)) (OverColor.map τ)) - ⊗⋙ OverColor.tensor C +def contrPair (C : Type) (τ : C → C) : Functor (OverColor C) (OverColor C) := + (Functor.diag (OverColor C)) + ⋙ (Functor.prod (Functor.id (OverColor C)) (OverColor.map τ)) + ⋙ (OverColor.tensor C) + +instance contrPair_laxMonoidal (C : Type) (τ : C → C) : Functor.LaxMonoidal (contrPair C τ) := + Functor.LaxMonoidal.comp (Functor.diag (OverColor C)) ((𝟭 (OverColor C)).prod (map τ) ⋙ tensor C) +noncomputable instance contrPair_monoidal (C : Type) (τ : C → C) : Functor.Monoidal (contrPair C τ) := + Functor.Monoidal.ofLaxMonoidal _ end OverColor end IndexNotation diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean index 9294fee4..599d8d0b 100644 --- a/HepLean/Tensors/OverColor/Lift.lean +++ b/HepLean/Tensors/OverColor/Lift.lean @@ -552,23 +552,30 @@ lemma objMap'_comp {X Y Z : OverColor C} (f : X ⟶ Y) (g : Y ⟶ Z) : rfl /-- The `BraidedFunctor (OverColor C) (Rep k G)` from a functor `Discrete C ⥤ Rep k G`. -/ -def obj' : BraidedFunctor (OverColor C) (Rep k G) where +def obj' : Functor (OverColor C) (Rep k G) where obj := objObj' F map := objMap' F - ε := (ε F).hom - μ X Y := (μ F X Y).hom - map_id f := objMap'_id F f - map_comp {X Y Z} f g := objMap'_comp F f g - μ_natural_left := μ_natural_left F - μ_natural_right := μ_natural_right F - associativity := associativity F - left_unitality := left_unitality F - right_unitality := right_unitality F - braided X Y := by - change (objMap' F) (β_ X Y).hom = _ + map_comp := fun f g => objMap'_comp F f g + map_id := fun f => objMap'_id F f + +instance obj'_laxBraidedFunctor : Functor.LaxBraided (obj' F) where + ε' := (ε F).hom + μ' := fun X Y => (μ F X Y).hom + μ'_natural_left := μ_natural_left F + μ'_natural_right := μ_natural_right F + associativity' := associativity F + left_unitality' := left_unitality F + right_unitality' := right_unitality F + braided := fun X Y => by + simp only [Functor.LaxMonoidal.μ, obj'] rw [braided F X Y] - congr - simp_all only [IsIso.Iso.inv_hom] + simp + +instance obj'_monoidalFunctor : Functor.Monoidal (obj' F) := + haveI : IsIso (Functor.LaxMonoidal.ε (obj' F)) := Action.isIso_of_hom_isIso (ε F).hom + haveI : (∀ (X Y : OverColor C), IsIso (Functor.LaxMonoidal.μ (obj' F) X Y)) := + fun X Y => Action.isIso_of_hom_isIso ((μ F X Y).hom) + Functor.Monoidal.ofLaxMonoidal _ variable {F F' : Discrete C ⥤ Rep k G} (η : F ⟶ F') @@ -633,7 +640,8 @@ lemma mapApp'_naturality {X Y : OverColor C} (f : X ⟶ Y) : (η.naturality (eqToHom (Discrete.eqToIso.proof_1 (Hom.toEquiv_comp_inv_apply f i)))) simpa [CategoryStruct.comp] using LinearMap.congr_fun hn (x ((Hom.toEquiv f).symm i)) -lemma mapApp'_unit : (obj' F).ε ≫ mapApp' η (𝟙_ (OverColor C)) = (obj' F').ε := by +lemma mapApp'_unit : Functor.LaxMonoidal.ε (obj' F) ≫ mapApp' η (𝟙_ (OverColor C)) = + Functor.LaxMonoidal.ε (obj' F') := by ext x simp only [obj', ε, instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj, instMonoidalCategoryStruct_tensorUnit_hom, objObj'_V_carrier, @@ -649,8 +657,8 @@ lemma mapApp'_unit : (obj' F).ε ≫ mapApp' η (𝟙_ (OverColor C)) = (obj' F' exact Empty.elim i lemma mapApp'_tensor (X Y : OverColor C) : - (obj' F).μ X Y ≫ mapApp' η (X ⊗ Y) = - (mapApp' η X ⊗ mapApp' η Y) ≫ (obj' F').μ X Y := by + (Functor.LaxMonoidal.μ (obj' F)) X Y ≫ mapApp' η (X ⊗ Y) = + (mapApp' η X ⊗ mapApp' η Y) ≫ (Functor.LaxMonoidal.μ (obj' F')) X Y := by ext1 apply HepLean.PiTensorProduct.induction_tmul (fun p q => ?_) simp only [obj', objObj'_V_carrier, instMonoidalCategoryStruct_tensorObj_left, @@ -672,9 +680,11 @@ lemma mapApp'_tensor (X Y : OverColor C) : /-- Given a natural transformation between `F F' : Discrete C ⥤ Rep k G` the monoidal natural transformation between `obj' F` and `obj' F'`. -/ -def map' : obj' F ⟶ obj' F' where +def map' : (obj' F) ⟶ (obj' F') where app := mapApp' η naturality _ _ f := mapApp'_naturality η f + +instance map'_isMonoidal : NatTrans.IsMonoidal (map' η) where unit := mapApp'_unit η tensor := mapApp'_tensor η @@ -683,13 +693,15 @@ end lift /-- The functor taking functors in `Discrete C ⥤ Rep k G` to monoidal functors in `BraidedFunctor (OverColor C) (Rep k G)`, built on the PiTensorProduct. -/ -noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ BraidedFunctor (OverColor C) (Rep k G) where - obj F := lift.obj' F - map η := lift.map' η +noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ LaxBraidedFunctor (OverColor C) (Rep k G) where + obj F := LaxBraidedFunctor.of (lift.obj' F) + map η := LaxMonoidalFunctor.homMk (lift.map' η) map_id F := by simp only [lift.map'] - refine MonoidalNatTrans.ext' (fun X => ?_) - ext x : 2 + refine LaxMonoidalFunctor.hom_ext ?_ + ext X : 2 + simp + ext x refine PiTensorProduct.induction_on' x ?_ (by intro x y hx hy simp only [Functor.id_obj, map_add, ModuleCat.coe_comp, Function.comp_apply] @@ -700,16 +712,18 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ BraidedFunctor (OverColor erw [lift.mapApp'_tprod] rfl map_comp {F G H} η θ := by - refine MonoidalNatTrans.ext' (fun X => ?_) + refine LaxMonoidalFunctor.hom_ext ?_ + ext X : 2 + simp only [LaxBraidedFunctor.toLaxMonoidalFunctor_toFunctor, LaxBraidedFunctor.of_toFunctor, + LaxMonoidalFunctor.homMk_hom, LaxBraidedFunctor.comp_hom, NatTrans.comp_app] ext x : 2 refine PiTensorProduct.induction_on' x ?_ (by intro x y hx hy simp only [Functor.id_obj, map_add, ModuleCat.coe_comp, Function.comp_apply] rw [hx, hy]) intro r y - simp only [Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod, map_smul, - MonoidalNatTrans.comp_toNatTrans, NatTrans.comp_app, Action.comp_hom, ModuleCat.coe_comp, - Function.comp_apply] + simp only [Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod, map_smul, Action.comp_hom, + ModuleCat.coe_comp, Function.comp_apply] apply congrArg simp only [lift.map'] erw [lift.mapApp'_tprod] @@ -722,6 +736,13 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ BraidedFunctor (OverColor namespace lift variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F') +noncomputable instance : (lift.obj F).Monoidal := obj'_monoidalFunctor F + +noncomputable instance : (lift.obj F).LaxBraided := obj'_laxBraidedFunctor F + +noncomputable instance : (lift.obj F).Braided := Functor.Braided.mk (fun X Y => + Functor.LaxBraided.braided X Y) + lemma map_tprod (F : Discrete C ⥤ Rep k G) {X Y : OverColor C} (f : X ⟶ Y) (p : (i : X.left) → F.obj (Discrete.mk <| X.hom i)) : ((lift.obj F).map f).hom (PiTensorProduct.tprod k p) = @@ -733,22 +754,22 @@ lemma map_tprod (F : Discrete C ⥤ Rep k G) {X Y : OverColor C} (f : X ⟶ Y) lemma obj_μ_tprod_tmul (F : Discrete C ⥤ Rep k G) (X Y : OverColor C) (p : (i : X.left) → (F.obj (Discrete.mk <| X.hom i))) (q : (i : Y.left) → F.obj (Discrete.mk <| Y.hom i)) : - ((lift.obj F).μ X Y).hom (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) = + (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) = (PiTensorProduct.tprod k) fun i => discreteSumEquiv F i (HepLean.PiTensorProduct.elimPureTensor p q i) := by exact μ_tmul_tprod F p q lemma μIso_inv_tprod (F : Discrete C ⥤ Rep k G) (X Y : OverColor C) (p : (i : (X ⊗ Y).left) → F.obj (Discrete.mk <| (X ⊗ Y).hom i)) : - ((lift.obj F).μIso X Y).inv.hom (PiTensorProduct.tprod k p) = + (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y).inv.hom (PiTensorProduct.tprod k p) = (PiTensorProduct.tprod k (fun i => p (Sum.inl i))) ⊗ₜ[k] (PiTensorProduct.tprod k (fun i => p (Sum.inr i))) := by - change ((Action.forget _ _).mapIso ((lift.obj F).μIso X Y)).inv (PiTensorProduct.tprod k p) = _ - trans ((Action.forget _ _).mapIso ((lift.obj F).μIso X Y)).toLinearEquiv.symm + change ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).inv (PiTensorProduct.tprod k p) = _ + trans ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).toLinearEquiv.symm (PiTensorProduct.tprod k p) · rfl erw [← LinearEquiv.eq_symm_apply] - change _ = ((lift.obj F).μ X Y).hom _ + change _ = (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom _ erw [obj_μ_tprod_tmul] congr funext i @@ -757,7 +778,7 @@ lemma μIso_inv_tprod (F : Discrete C ⥤ Rep k G) (X Y : OverColor C) | Sum.inr i => rfl @[simp] -lemma inv_μ (X Y : OverColor C) : inv ((lift.obj F).μ X Y) = +lemma inv_μ (X Y : OverColor C) : inv (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y) = (lift.μ F X Y).inv := by change inv (lift.μ F X Y).hom = _ exact IsIso.Iso.inv_hom (μ F X Y) @@ -769,9 +790,9 @@ def incl : Discrete C ⥤ OverColor C := Discrete.functor fun c => /-- The forgetful map from `BraidedFunctor (OverColor C) (Rep k G)` to `Discrete C ⥤ Rep k G` built on the inclusion `incl` and forgetting the monoidal structure. -/ -def forget : BraidedFunctor (OverColor C) (Rep k G) ⥤ (Discrete C ⥤ Rep k G) where +def forget : LaxBraidedFunctor (OverColor C) (Rep k G) ⥤ (Discrete C ⥤ Rep k G) where obj F := Discrete.functor fun c => F.obj (incl.obj (Discrete.mk c)) - map η := Discrete.natTrans fun c => η.app (incl.obj c) + map η := Discrete.natTrans fun c => η.hom.app (incl.obj c) variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F') diff --git a/HepLean/Tensors/TensorSpecies/Basic.lean b/HepLean/Tensors/TensorSpecies/Basic.lean index eb2f35ad..db1c058c 100644 --- a/HepLean/Tensors/TensorSpecies/Basic.lean +++ b/HepLean/Tensors/TensorSpecies/Basic.lean @@ -105,11 +105,19 @@ instance : Group S.G := S.G_group /-- The field `repDim` of a TensorSpecies is non-zero for all colors. -/ instance (c : S.C) : NeZero (S.repDim c) := S.repDim_neZero c -/-- The lift of the functor `S.F` to a monoidal functor. -/ -def F : BraidedFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FD +/-- The lift of the functor `S.F` to functor. -/ +def F : Functor (OverColor S.C) (Rep S.k S.G) := ((OverColor.lift).obj S.FD).toFunctor /- The definition of `F` as a lemma. -/ -lemma F_def : F S = (OverColor.lift).obj S.FD := rfl +lemma F_def : F S = ((OverColor.lift).obj S.FD).toFunctor := rfl + +instance F_monoidal : Functor.Monoidal S.F := lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor S.FD + +instance F_laxBraided : Functor.LaxBraided S.F := lift.instLaxBraidedRepObjFunctorDiscreteLaxBraidedFunctor S.FD + +instance F_braided : Functor.Braided S.F := Functor.Braided.mk + (fun X Y => Functor.LaxBraided.braided X Y) + lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} @@ -158,7 +166,7 @@ def evalIso {n : ℕ} (c : Fin n.succ → S.C) (OverColor.lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove)) := (S.F.mapIso (OverColor.equivToIso (HepLean.Fin.finExtractOne i))).trans <| (S.F.mapIso (OverColor.mkSum (c ∘ (HepLean.Fin.finExtractOne i).symm))).trans <| - (S.F.μIso _ _).symm.trans <| + (Functor.Monoidal.μIso S.F _ _).symm.trans <| tensorIso ((S.F.mapIso (OverColor.mkIso (by ext x; fin_cases x; rfl))).trans (OverColor.forgetLiftApp S.FD (c i))) (S.F.mapIso (OverColor.mkIso (by ext x; simp))) @@ -174,7 +182,7 @@ lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) change (((lift.obj S.FD).map (mkIso _).hom).hom ≫ (forgetLiftApp S.FD (c i)).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom) - (((lift.obj S.FD).μIso + ((Functor.Monoidal.μIso (lift.obj S.FD).toFunctor (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inl)) (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inr))).inv.hom (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractOne i).symm)).hom).hom @@ -184,7 +192,7 @@ lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) change (((lift.obj S.FD).map (mkIso _).hom).hom ≫ (forgetLiftApp S.FD (c i)).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom) - (((lift.obj S.FD).μIso + ((Functor.Monoidal.μIso (lift.obj S.FD).toFunctor (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inl)) (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inr))).inv.hom (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractOne i).symm)).hom).hom @@ -193,7 +201,7 @@ lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) change ((TensorProduct.map (((lift.obj S.FD).map (mkIso _).hom).hom ≫ (forgetLiftApp S.FD (c i)).hom.hom) ((lift.obj S.FD).map (mkIso _).hom).hom)) - (((lift.obj S.FD).μIso + ((Functor.Monoidal.μIso (lift.obj S.FD).toFunctor (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inl)) (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inr))).inv.hom ((((PiTensorProduct.tprod S.k) _)))) =_ @@ -247,7 +255,7 @@ def evalLinearMap {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin ( of representations. -/ def evalMap {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i))) : (S.F.obj (OverColor.mk c)).V ⟶ (S.F.obj (OverColor.mk (c ∘ i.succAbove))).V := - (S.evalIso c i).hom.hom ≫ ((Action.forgetMonoidal _ _).μIso _ _).inv + (S.evalIso c i).hom.hom ≫ (Functor.Monoidal.μIso (Action.forget _ _) _ _).inv ≫ ModuleCat.asHom (TensorProduct.map (S.evalLinearMap i e) LinearMap.id) ≫ ModuleCat.asHom (TensorProduct.lid S.k _).toLinearMap @@ -258,21 +266,21 @@ lemma evalMap_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (PiTensorProduct.tprod S.k (fun k => x (i.succAbove k)) : S.F.obj (OverColor.mk (c ∘ i.succAbove))) := by rw [evalMap] - simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, - Action.forgetMonoidal_toLaxMonoidalFunctor_toFunctor, Action.forget_obj, Functor.id_obj, mk_hom, - Function.comp_apply, ModuleCat.coe_comp] + simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Action.forget_obj, + Functor.Monoidal.μIso_inv, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, Action.forget_δ, + mk_left, Functor.id_obj, mk_hom, Function.comp_apply, Category.id_comp, ModuleCat.coe_comp] erw [evalIso_tprod] change ((TensorProduct.lid S.k ↑((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove))).V)) (((TensorProduct.map (S.evalLinearMap i e) LinearMap.id)) - (((Action.forgetMonoidal (ModuleCat S.k) (MonCat.of S.G)).μIso (S.FD.obj { as := c i }) + ((Functor.Monoidal.μIso (Action.forget (ModuleCat S.k) (MonCat.of S.G)) (S.FD.obj { as := c i }) ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove)))).inv (x i ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun k => x (i.succAbove k)))) = _ - simp only [Nat.succ_eq_add_one, Action.forgetMonoidal_toLaxMonoidalFunctor_toFunctor, - Action.forget_obj, Action.instMonoidalCategory_tensorObj_V, MonoidalFunctor.μIso, - Action.forgetMonoidal_toLaxMonoidalFunctor_μ, asIso_inv, IsIso.inv_id, Equivalence.symm_inverse, - Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, - Functor.id_obj, mk_hom, Function.comp_apply, ModuleCat.id_apply, TensorProduct.map_tmul, - LinearMap.id_coe, id_eq, TensorProduct.lid_tmul] + simp only [Nat.succ_eq_add_one, Action.forget_obj, Action.instMonoidalCategory_tensorObj_V, + Functor.Monoidal.μIso_inv, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, Action.forget_δ, + Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, + Action.FunctorCategoryEquivalence.functor_obj_obj, mk_left, Functor.id_obj, mk_hom, + Function.comp_apply, ModuleCat.id_apply, TensorProduct.map_tmul, LinearMap.id_coe, id_eq, + TensorProduct.lid_tmul] rfl /-! diff --git a/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean b/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean index 70bc1cd4..3b8065d9 100644 --- a/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean +++ b/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean @@ -30,7 +30,7 @@ def contrFin1Fin1 {n : ℕ} (c : Fin n.succ.succ → S.C) (OverColor.Discrete.pairτ S.FD S.τ).obj { as := c i } := by apply (S.F.mapIso (OverColor.mkSum (((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)))).trans - apply (S.F.μIso _ _).symm.trans + apply (Functor.Monoidal.μIso S.F _ _).symm.trans apply tensorIso ?_ ?_ · symm apply (OverColor.forgetLiftApp S.FD (c i)).symm.trans @@ -57,15 +57,15 @@ lemma contrFin1Fin1_inv_tmul {n : ℕ} (c : Fin n.succ.succ → S.C) (eqToHom (by simp [h]))).hom y) := by simp only [Nat.succ_eq_add_one, contrFin1Fin1, Functor.comp_obj, Discrete.functor_obj_eq_as, Function.comp_apply, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_inv, tensorIso_inv, - Iso.symm_inv, Functor.mapIso_hom, tensor_comp, MonoidalFunctor.μIso_hom, Category.assoc, - LaxMonoidalFunctor.μ_natural, Functor.mapIso_inv, Action.comp_hom, - Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorHom_hom, - Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, - Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Functor.id_obj, mk_hom, - Fin.isValue] + Iso.symm_inv, Functor.mapIso_hom, tensor_comp, Functor.Monoidal.μIso_hom, + Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, Category.assoc, Functor.LaxMonoidal.μ_natural, + Functor.mapIso_inv, Action.comp_hom, Action.instMonoidalCategory_tensorObj_V, + Action.instMonoidalCategory_tensorHom_hom, Equivalence.symm_inverse, + Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, + ModuleCat.coe_comp, mk_left, Functor.id_obj, mk_hom, Fin.isValue] change (S.F.map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom ((S.F.map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom - ((S.F.μ (OverColor.mk fun _ => c i) (OverColor.mk fun _ => S.τ (c i))).hom + ((Functor.LaxMonoidal.μ S.F (OverColor.mk fun _ => c i) (OverColor.mk fun _ => S.τ (c i))).hom ((((OverColor.forgetLiftApp S.FD (c i)).inv.hom x) ⊗ₜ[S.k] ((OverColor.forgetLiftApp S.FD (S.τ (c i))).inv.hom y))))) = _ simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse, @@ -76,7 +76,7 @@ lemma contrFin1Fin1_inv_tmul {n : ℕ} (c : Fin n.succ.succ → S.C) change ((OverColor.lift.obj S.FD).map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom (((OverColor.lift.obj S.FD).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom - (((OverColor.lift.obj S.FD).μ (OverColor.mk fun _ => c i) + ((Functor.LaxMonoidal.μ (OverColor.lift.obj S.FD).toFunctor (OverColor.mk fun _ => c i) (OverColor.mk fun _ => S.τ (c i))).hom (((PiTensorProduct.tprod S.k) fun _ => x) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun _ => y))) = _ rw [OverColor.lift.obj_μ_tprod_tmul S.FD] @@ -144,7 +144,7 @@ def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C) (OverColor.lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) := (S.F.mapIso (OverColor.equivToIso (HepLean.Fin.finExtractTwo i j))).trans <| (S.F.mapIso (OverColor.mkSum (c ∘ (HepLean.Fin.finExtractTwo i j).symm))).trans <| - (S.F.μIso _ _).symm.trans <| by + (Functor.Monoidal.μIso S.F _ _).symm.trans <| by refine tensorIso (S.contrFin1Fin1 c i j h) (S.F.mapIso (OverColor.mkIso (by ext x; simp))) lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C} @@ -152,7 +152,7 @@ lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C} (S.contrIso c1 i j h).hom.hom = (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom ≫ (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom ≫ - (S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) + (Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom ≫ ((S.contrFin1Fin1 c1 i j h).hom.hom ⊗ (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom) := by @@ -192,38 +192,15 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C) (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V) (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom) - (((lift.obj S.FD).μIso (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) + ((Functor.Monoidal.μIso (lift.obj S.FD).toFunctor (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom (((lift.obj S.FD).map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom ((PiTensorProduct.tprod S.k) x)))))) = _ rw [lift.map_tprod] - change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom - (((S.contr.app { as := c i }).hom ▷ - ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V) - (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom) - (((lift.obj S.FD).μIso (OverColor.mk - ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) - (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom - (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom - ((PiTensorProduct.tprod S.k) fun i_1 => - (lift.discreteFunctorMapEqIso S.FD _) - (x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm i_1))))))) = _ - rw [lift.map_tprod] - change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom - (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj - (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V) - (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom) - (((lift.obj S.FD).μIso - (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) - (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom - ((PiTensorProduct.tprod S.k) fun i_1 => - (lift.discreteFunctorMapEqIso S.FD _) - ((lift.discreteFunctorMapEqIso S.FD _) - (x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm - ((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm i_1)))))))) = _ - rw [lift.μIso_inv_tprod] + erw [lift.map_tprod] + erw [lift.μIso_inv_tprod] change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V) diff --git a/HepLean/Tensors/TensorSpecies/Pure.lean b/HepLean/Tensors/TensorSpecies/Pure.lean index de141419..e8ee183d 100644 --- a/HepLean/Tensors/TensorSpecies/Pure.lean +++ b/HepLean/Tensors/TensorSpecies/Pure.lean @@ -38,12 +38,9 @@ def tprod (p : Pure S c) : S.F.obj c := PiTensorProduct.tprod S.k p /-- The map `tprod` is equivariant with respect to the group action. -/ lemma tprod_equivariant (g : S.G) (p : Pure S c) : (ρ g p).tprod = (S.F.obj c).ρ g p.tprod := by - simp only [F_def, OverColor.lift, OverColor.lift.obj', OverColor.lift.objObj', - OverColor.instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj, - OverColor.instMonoidalCategoryStruct_tensorUnit_hom, - OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Rep.coe_of, tprod, Rep.of_ρ, - MonoidHom.coe_mk, OneHom.coe_mk, PiTensorProduct.map_tprod] + simp only [F_def, OverColor.lift, OverColor.lift.obj', LaxBraidedFunctor.of_toFunctor, + OverColor.lift.objObj', Functor.id_obj, Rep.coe_of, tprod, Rep.of_ρ, MonoidHom.coe_mk, + OneHom.coe_mk, PiTensorProduct.map_tprod] rfl end Pure diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean index acc9d961..6ecebc52 100644 --- a/HepLean/Tensors/Tree/Basic.lean +++ b/HepLean/Tensors/Tree/Basic.lean @@ -157,7 +157,7 @@ def tensor {n : ℕ} {c : Fin n → S.C} : TensorTree S c → S.F.obj (OverColor | action g t => (S.F.obj (OverColor.mk _)).ρ g t.tensor | perm σ t => (S.F.map σ).hom t.tensor | prod t1 t2 => (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom - ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor)) + ((Functor.LaxMonoidal.μ S.F _ _).hom (t1.tensor ⊗ₜ t2.tensor)) | contr i j h t => (S.contrMap _ i j h).hom t.tensor | eval i e t => (S.evalMap i (Fin.ofNat' _ e)) t.tensor @@ -192,7 +192,7 @@ lemma constThreeNode_tensor {c1 c2 c3 : S.C} lemma prod_tensor {c1 : Fin n → S.C} {c2 : Fin m → S.C} (t1 : TensorTree S c1) (t2 : TensorTree S c2) : (prod t1 t2).tensor = (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom - ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor)) := rfl + ((Functor.LaxMonoidal.μ S.F _ _).hom (t1.tensor ⊗ₜ t2.tensor)) := rfl lemma add_tensor (t1 t2 : TensorTree S c) : (add t1 t2).tensor = t1.tensor + t2.tensor := rfl diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean index 186101f9..fa82d4f4 100644 --- a/HepLean/Tensors/Tree/Elab.lean +++ b/HepLean/Tensors/Tree/Elab.lean @@ -327,7 +327,7 @@ partial def getContrPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do let ind ← getIndices stx let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x) let indEnum := indFilt.enum - let bind := List.bind indEnum (fun a => indEnum.map (fun b => (a, b))) + let bind := List.flatMap indEnum (fun a => indEnum.map (fun b => (a, b))) let filt ← bind.filterMapM (fun x => indexPosEq x.1 x.2) if ¬ ((filt.map Prod.fst).Nodup ∧ (filt.map Prod.snd).Nodup) then throwError "To many contractions" @@ -352,7 +352,7 @@ def toPairs (l : List ℕ) : List (ℕ × ℕ) := of elements before it in the list which are less then itself. This is used to form a list of pairs which can be used for contracting indices. -/ def contrListAdjust (l : List (ℕ × ℕ)) : List (ℕ × ℕ) := - let l' := l.bind (fun p => [p.1, p.2]) + let l' := l.flatMap (fun p => [p.1, p.2]) let l'' := List.mapAccumr (fun x (prev : List ℕ) => let e := prev.countP (fun y => y < x) @@ -394,7 +394,7 @@ partial def getContrPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do let ind ← getIndices stx let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x) let indEnum := indFilt.enum - let bind := List.bind indEnum (fun a => indEnum.map (fun b => (a, b))) + let bind := List.flatMap indEnum (fun a => indEnum.map (fun b => (a, b))) let filt ← bind.filterMapM (fun x => indexPosEq x.1 x.2) if ¬ ((filt.map Prod.fst).Nodup ∧ (filt.map Prod.snd).Nodup) then throwError "To many contractions" diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean index d32d527c..88358a77 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean @@ -312,15 +312,15 @@ lemma prod_action {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (g : S. simp only [prod_tensor, action_tensor, map_tmul] change _ = ((S.F.map (equivToIso finSumFinEquiv).hom).hom ≫ (S.F.obj (OverColor.mk (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm))).ρ g) - (((S.F.μ (OverColor.mk c) (OverColor.mk c1)).hom (t.tensor ⊗ₜ[S.k] t1.tensor))) + (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom (t.tensor ⊗ₜ[S.k] t1.tensor))) erw [← (S.F.map (equivToIso finSumFinEquiv).hom).comm g] simp only [Action.forget_obj, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply] change _ = (S.F.map (equivToIso finSumFinEquiv).hom).hom - (((S.F.μ (OverColor.mk c) (OverColor.mk c1)).hom ≫ (S.F.obj (OverColor.mk (Sum.elim c c1))).ρ g) + (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom ≫ (S.F.obj (OverColor.mk (Sum.elim c c1))).ρ g) (t.tensor ⊗ₜ[S.k] t1.tensor)) - erw [← (S.F.μ (OverColor.mk c) (OverColor.mk c1)).comm g] + erw [← (Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).comm g] rfl /-- An `action` node can be moved through a `add` node when acting on both elements. -/ diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean index 6eec409c..64e045a5 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean @@ -117,19 +117,17 @@ lemma contrIso_comm_aux_2 {n : ℕ} {c c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) : (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)).hom ≫ - (S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) + (Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom = - (S.F.μIso _ _).inv.hom ≫ + (Functor.Monoidal.μIso S.F _ _).inv.hom ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)).hom := by have h1 : (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)) ≫ - (S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) + (Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv = - (S.F.μIso _ _).inv ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)) := by + (Functor.Monoidal.μIso S.F _ _).inv ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)) := by erw [CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.Category.assoc] erw [CategoryTheory.IsIso.eq_inv_comp] - exact Eq.symm - (LaxMonoidalFunctor.μ_natural S.F.toLaxMonoidalFunctor (extractTwoAux' i j σ) - (extractTwoAux i j σ)) + exact (Functor.LaxMonoidal.μ_natural S.F (extractTwoAux' i j σ) (extractTwoAux i j σ)).symm exact congrArg (λ f => Action.Hom.hom f) h1 lemma contrIso_comm_aux_3 {n : ℕ} {c c1 : Fin n.succ.succ → S.C} diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean b/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean index 028b3690..bf355d2c 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean @@ -54,8 +54,8 @@ theorem prod_perm_left (t : TensorTree S c) (t2 : TensorTree S c2) : Action.FunctorCategoryEquivalence.functor_obj_obj, perm_tensor] change (S.F.map (equivToIso finSumFinEquiv).hom).hom (((S.F.map (σ) ▷ S.F.obj (OverColor.mk c2)) ≫ - S.F.μ (OverColor.mk c') (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor)) = _ - rw [S.F.μ_natural_left] + Functor.LaxMonoidal.μ S.F (OverColor.mk c') (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor)) = _ + rw [Functor.LaxMonoidal.μ_natural_left] simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply] @@ -72,9 +72,9 @@ theorem prod_perm_right (t2 : TensorTree S c2) (t : TensorTree S c) : Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, perm_tensor] change (S.F.map (equivToIso finSumFinEquiv).hom).hom - (((S.F.obj (OverColor.mk c2) ◁ S.F.map σ) ≫ S.F.μ (OverColor.mk c2) (OverColor.mk c')).hom + (((S.F.obj (OverColor.mk c2) ◁ S.F.map σ) ≫ Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c')).hom (t2.tensor ⊗ₜ[S.k] t.tensor)) = _ - rw [S.F.μ_natural_right] + rw [Functor.LaxMonoidal.μ_natural_right] simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply] diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean index 82a68454..80e3a5e6 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean @@ -63,7 +63,7 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree rw [perm_tensor] nth_rewrite 2 [prod_tensor] change _ = ((S.F.map (equivToIso finSumFinEquiv).hom) ≫ S.F.map (assocPerm c c2 c3).hom).hom - (((S.F.μ (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3)).hom + (((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3)).hom ((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor))) rw [← S.F.map_comp, finSumFinEquiv_comp_assocPerm] simp only [Functor.id_obj, mk_hom, whiskerRightIso_hom, Iso.symm_hom, whiskerLeftIso_hom, @@ -74,10 +74,10 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree apply congrArg change _ = (S.F.map (OverColor.mk c ◁ (equivToIso finSumFinEquiv).hom)).hom ((S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom - ((S.F.μ (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3) + ((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3) ≫ S.F.map ((equivToIso finSumFinEquiv).inv ▷ OverColor.mk c3)).hom (((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor)))) - rw [← S.F.μ_natural_left] + rw [← Functor.LaxMonoidal.μ_natural_left] simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, Action.comp_hom, @@ -89,20 +89,20 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree Action.FunctorCategoryEquivalence.functor_obj_obj] change _ = (S.F.map (OverColor.mk c ◁ (equivToIso finSumFinEquiv).hom)).hom ((S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom - ((S.F.μ (OverColor.mk (Sum.elim c c2)) (OverColor.mk c3)).hom + ((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2)) (OverColor.mk c3)).hom ((S.F.map (equivToIso finSumFinEquiv).hom ≫ S.F.map (equivToIso finSumFinEquiv).inv).hom - (((S.F.μ (OverColor.mk c) (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor))) ⊗ₜ[S.k] + (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor))) ⊗ₜ[S.k] t3.tensor))) simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, Iso.map_hom_inv_id, Action.id_hom, ModuleCat.id_apply] change _ = (S.F.map (OverColor.mk c ◁ (equivToIso finSumFinEquiv).hom)).hom - (((S.F.μ (OverColor.mk c) (OverColor.mk c2) ▷ S.F.obj (OverColor.mk c3)) ≫ - S.F.μ (OverColor.mk (Sum.elim c c2)) (OverColor.mk c3) ≫ + (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c2) ▷ S.F.obj (OverColor.mk c3)) ≫ + Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2)) (OverColor.mk c3) ≫ S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom (((t.tensor ⊗ₜ[S.k] t2.tensor) ⊗ₜ[S.k] t3.tensor))) - erw [S.F.associativity] + erw [Functor.LaxMonoidal.associativity] simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom, Action.instMonoidalCategory_associator_hom_hom, Action.instMonoidalCategory_whiskerLeft_hom, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, @@ -110,10 +110,10 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree ModuleCat.MonoidalCategory.associator_hom_apply] rw [prod_tensor] change ((_ ◁ (S.F.map (equivToIso finSumFinEquiv).hom)) ≫ - S.F.μ (OverColor.mk c) (OverColor.mk (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm))).hom + Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm))).hom (t.tensor ⊗ₜ[S.k] - ((S.F.μ (OverColor.mk c2) (OverColor.mk c3)).hom (t2.tensor ⊗ₜ[S.k] t3.tensor))) = _ - rw [S.F.μ_natural_right] + ((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c3)).hom (t2.tensor ⊗ₜ[S.k] t3.tensor))) = _ + rw [Functor.LaxMonoidal.μ_natural_right] simp only [Action.instMonoidalCategory_tensorObj_V, Action.comp_hom, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply] diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean index d4e4a325..ec687262 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean @@ -49,11 +49,12 @@ theorem prod_comm (t : TensorTree S c) (t2 : TensorTree S c2) : rw [perm_tensor] nth_rewrite 2 [prod_tensor] change _ = (S.F.map (equivToIso finSumFinEquiv).hom ≫ S.F.map (braidPerm c c2)).hom - ((S.F.μ (OverColor.mk c2) (OverColor.mk c)).hom (t2.tensor ⊗ₜ[S.k] t.tensor)) + ((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c)).hom (t2.tensor ⊗ₜ[S.k] t.tensor)) rw [← S.F.map_comp] rw [finSumFinEquiv_comp_braidPerm] rw [S.F.map_comp] - simp only [BraidedFunctor.braided, Category.assoc, Action.comp_hom, + rw [Functor.map_braiding] + simp only [Category.assoc, Action.comp_hom, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply] diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean index 106e28e6..0e416d25 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean @@ -172,13 +172,13 @@ lemma contrMap_prod_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c).left) → (q' : (i : (𝟭 Type).obj (OverColor.mk c1).left) → CoeSort.coe (S.FD.obj { as := (OverColor.mk c1).hom i })) : (S.F.map (equivToIso finSumFinEquiv).hom).hom - ((S.F.μ (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) (OverColor.mk c1)).hom + ((Functor.LaxMonoidal.μ S.F (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) (OverColor.mk c1)).hom ((q.contrMap.hom (PiTensorProduct.tprod S.k p)) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) q')) = (S.F.map (mkIso (by exact leftContr_map_eq q)).hom).hom (q.leftContr.contrMap.hom ((S.F.map (equivToIso (@leftContrEquivSuccSucc n n1)).hom).hom ((S.F.map (equivToIso finSumFinEquiv).hom).hom - ((S.F.μ (OverColor.mk c) (OverColor.mk c1)).hom + ((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom ((PiTensorProduct.tprod S.k) p ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) q'))))) := by conv_lhs => rw [contrMap, TensorSpecies.contrMap_tprod] simp only [TensorSpecies.F_def] @@ -272,9 +272,9 @@ lemma contrMap_prod_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c).left) → | Sum.inr k => exact q.sum_inr_succAbove_leftContrI_leftContrJ _ lemma contrMap_prod : - (q.contrMap ▷ S.F.obj (OverColor.mk c1)) ≫ (S.F.μ _ ((OverColor.mk c1))) ≫ + (q.contrMap ▷ S.F.obj (OverColor.mk c1)) ≫ (Functor.LaxMonoidal.μ S.F _ ((OverColor.mk c1))) ≫ S.F.map (OverColor.equivToIso finSumFinEquiv).hom = - (S.F.μ ((OverColor.mk c)) ((OverColor.mk c1))) ≫ + (Functor.LaxMonoidal.μ S.F ((OverColor.mk c)) ((OverColor.mk c1))) ≫ S.F.map (OverColor.equivToIso finSumFinEquiv).hom ≫ S.F.map (OverColor.equivToIso leftContrEquivSuccSucc).hom ≫ q.leftContr.contrMap ≫ S.F.map (OverColor.mkIso (q.leftContr_map_eq)).hom := by @@ -288,7 +288,7 @@ lemma contr_prod q.leftContr.h (perm (OverColor.equivToIso ContrPair.leftContrEquivSuccSucc).hom (prod t t1)))).tensor) := by simp only [contr_tensor, perm_tensor, prod_tensor] - change ((q.contrMap ▷ S.F.obj (OverColor.mk c1)) ≫ (S.F.μ _ ((OverColor.mk c1))) ≫ + change ((q.contrMap ▷ S.F.obj (OverColor.mk c1)) ≫ (Functor.LaxMonoidal.μ S.F _ ((OverColor.mk c1))) ≫ S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom (t.tensor ⊗ₜ[S.k] t1.tensor) = _ rw [contrMap_prod] simp only [Nat.succ_eq_add_one, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, @@ -405,12 +405,12 @@ lemma prod_contrMap_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c1).left) → (q' : (i : (𝟭 Type).obj (OverColor.mk c).left) → CoeSort.coe (S.FD.obj { as := (OverColor.mk c).hom i })) : (S.F.map (equivToIso finSumFinEquiv).hom).hom - ((S.F.μ (OverColor.mk c1) (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))).hom + ((Functor.LaxMonoidal.μ S.F (OverColor.mk c1) (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))).hom ((PiTensorProduct.tprod S.k) p ⊗ₜ[S.k] (q.contrMap.hom (PiTensorProduct.tprod S.k q')))) = (S.F.map (mkIso (by exact (rightContr_map_eq q))).hom).hom (q.rightContr.contrMap.hom (((S.F.map (equivToIso finSumFinEquiv).hom).hom - ((S.F.μ (OverColor.mk c1) (OverColor.mk c)).hom + ((Functor.LaxMonoidal.μ S.F (OverColor.mk c1) (OverColor.mk c)).hom ((PiTensorProduct.tprod S.k) p ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) q'))))) := by conv_lhs => rw [contrMap, TensorSpecies.contrMap_tprod] simp only [TensorSpecies.F_def] @@ -517,9 +517,9 @@ lemma prod_contrMap_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c1).left) → | Sum.inr k => exact sum_inr_succAbove_rightContrI_rightContrJ _ _ lemma prod_contrMap : - (S.F.obj (OverColor.mk c1) ◁ q.contrMap) ≫ (S.F.μ ((OverColor.mk c1)) _) ≫ + (S.F.obj (OverColor.mk c1) ◁ q.contrMap) ≫ (Functor.LaxMonoidal.μ S.F ((OverColor.mk c1)) _) ≫ S.F.map (OverColor.equivToIso finSumFinEquiv).hom = - (S.F.μ ((OverColor.mk c1)) ((OverColor.mk c))) ≫ + (Functor.LaxMonoidal.μ S.F ((OverColor.mk c1)) ((OverColor.mk c))) ≫ S.F.map (OverColor.equivToIso finSumFinEquiv).hom ≫ q.rightContr.contrMap ≫ S.F.map (OverColor.mkIso (q.rightContr_map_eq)).hom := by ext1 @@ -530,7 +530,7 @@ lemma prod_contr (t1 : TensorTree S c1) (t : TensorTree S c) : (contr (q.rightContrI n1) (q.rightContrJ n1) q.rightContr.h (prod t1 t))).tensor) := by simp only [contr_tensor, perm_tensor, prod_tensor] - change ((S.F.obj (OverColor.mk c1) ◁ q.contrMap) ≫ (S.F.μ ((OverColor.mk c1)) _) ≫ + change ((S.F.obj (OverColor.mk c1) ◁ q.contrMap) ≫ (Functor.LaxMonoidal.μ S.F ((OverColor.mk c1)) _) ≫ S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom (t1.tensor ⊗ₜ[S.k] t.tensor) = _ rw [prod_contrMap] simp only [Nat.succ_eq_add_one, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, diff --git a/README.md b/README.md index a9195724..8ab94df9 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ [![](https://img.shields.io/badge/Informal_dependencies-Graph-green)](https://heplean.github.io/HepLean/InformalGraph) [![](https://img.shields.io/badge/View_The-Stats-blue)](https://heplean.github.io/HepLean/Stats) -[![](https://img.shields.io/badge/Lean-v4.13.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.13.0) +[![](https://img.shields.io/badge/Lean-v4.14.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.14.0) [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/HEPLean/HepLean) A project to digitalize high energy physics. diff --git a/lake-manifest.json b/lake-manifest.json index 0da12d3f..8f020b7b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,62 +1,72 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/batteries", + [{"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18", - "name": "batteries", + "scope": "", + "rev": "0a8cd7afb471bb1fdd335118bf1e253a38a2af53", + "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", + "inputRev": "v4.14.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785", - "name": "Qq", + "scope": "", + "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84", + "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, + "inputRev": "v4.14.0", + "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + {"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46", - "name": "aesop", + "scope": "", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", + {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af", - "name": "proofwidgets", + "scope": "", + "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff", + "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.43", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/dupuisf/BibtexQuery", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", - "name": "Cli", + "scope": "", + "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c", + "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb", - "name": "importGraph", + "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", + "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, @@ -65,61 +75,61 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7bedaed1ef024add1e171cc17706b012a9a37802", + "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "scope": "", - "rev": "d5ab93e3a3afadaf265a583a92f7e7c47203b540", - "name": "mathlib", + "scope": "leanprover-community", + "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7", + "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.13.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/acmepjz/md4lean", + "inputRev": "v4.14.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "scope": "", - "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005", - "name": "MD4Lean", + "scope": "leanprover-community", + "rev": "68280daef58803f68368eb2e53046dabcd270c9d", + "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v0.0.47", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "scope": "", - "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0", - "name": "UnicodeBasic", + "scope": "leanprover-community", + "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.14.0", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "scope": "", - "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8", - "name": "BibtexQuery", + "scope": "leanprover-community", + "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", + "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "scope": "", - "rev": "ccb4e97ffb7ad0f9b1852e9669d5e2922f984175", - "name": "«doc-gen4»", + "scope": "leanprover-community", + "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.13.0-rc1", - "inherited": false, - "configFile": "lakefile.lean"}], + "inputRev": "v4.14.0", + "inherited": true, + "configFile": "lakefile.toml"}], "name": "hep_lean", "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml index fe39226c..4f09c806 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,12 +6,12 @@ defaultTargets = ["HepLean"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.13.0" +rev = "v4.14.0" [[require]] name = "«doc-gen4»" git = "https://github.com/leanprover/doc-gen4" -rev = "v4.13.0-rc1" +rev = "v4.14.0" [[lean_lib]] name = "HepLean" diff --git a/lean-toolchain b/lean-toolchain index 4f86f953..401bc146 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.13.0 +leanprover/lean4:v4.14.0 \ No newline at end of file From 9d4c21fd6da9cfedd0b0b7eb02a77c3e3f9a5229 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 10 Dec 2024 14:02:31 +0000 Subject: [PATCH 2/5] refactor: Lint --- HepLean/Tensors/OverColor/Functors.lean | 50 +++++++++++-------- HepLean/Tensors/OverColor/Lift.lean | 27 +++++++--- HepLean/Tensors/TensorSpecies/Basic.lean | 10 ++-- .../TensorSpecies/Contractions/ContrMap.lean | 7 +-- .../Tensors/Tree/NodeIdentities/Basic.lean | 7 +-- .../Tree/NodeIdentities/PermContr.lean | 9 ++-- .../Tensors/Tree/NodeIdentities/PermProd.lean | 6 ++- .../Tree/NodeIdentities/ProdAssoc.lean | 17 ++++--- .../Tensors/Tree/NodeIdentities/ProdComm.lean | 3 +- .../Tree/NodeIdentities/ProdContr.lean | 12 +++-- scripts/lint_all.lean | 6 +-- 11 files changed, 98 insertions(+), 56 deletions(-) diff --git a/HepLean/Tensors/OverColor/Functors.lean b/HepLean/Tensors/OverColor/Functors.lean index 8de5d4f3..bd96061f 100644 --- a/HepLean/Tensors/OverColor/Functors.lean +++ b/HepLean/Tensors/OverColor/Functors.lean @@ -19,20 +19,21 @@ open MonoidalCategory def map {C D : Type} (f : C → D) : Functor (OverColor C) (OverColor D) := Core.functorToCore (Core.inclusion (Over C) ⋙ (Over.map f)) +/-- The functor `map f` is lax-monoidal. -/ instance map_laxMonoidal {C D : Type} (f : C → D) : Functor.LaxMonoidal (map f) where ε' := Over.isoMk (Iso.refl _) (by ext x exact Empty.elim x) - μ' := fun X Y => Over.isoMk (Iso.refl _) (by + μ' := fun X Y => Over.isoMk (Iso.refl _) (by ext x match x with | Sum.inl x => rfl | Sum.inr x => rfl) - μ'_natural_left := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + μ'_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by rfl - μ'_natural_right := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + μ'_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by rfl - associativity' := fun X Y Z => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + associativity' X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl (Sum.inl x) => rfl | Sum.inl (Sum.inr x) => rfl @@ -46,6 +47,7 @@ instance map_laxMonoidal {C D : Type} (f : C → D) : Functor.LaxMonoidal (map f | Sum.inl x => rfl | Sum.inr x => rfl +/-- The functor `map f` is lax-monoidal. -/ noncomputable instance map_monoidal {C D : Type} (f : C → D) : Functor.Monoidal (map f) := Functor.Monoidal.ofLaxMonoidal _ @@ -53,6 +55,7 @@ noncomputable instance map_monoidal {C D : Type} (f : C → D) : Functor.Monoida def tensor (C : Type) : Functor (OverColor C × OverColor C) (OverColor C) := MonoidalCategory.tensor (OverColor C) +/-- The functor tensor is lax-monoidal. -/ instance tensor_laxMonoidal (C : Type) : Functor.LaxMonoidal (tensor C) where ε' := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso rfl μ' := fun X Y => Over.isoMk (Equiv.sumSumSumComm X.1.left X.2.left Y.1.left Y.2.left).toIso (by @@ -62,19 +65,19 @@ instance tensor_laxMonoidal (C : Type) : Functor.LaxMonoidal (tensor C) where | Sum.inl (Sum.inr x) => rfl | Sum.inr (Sum.inl x) => rfl | Sum.inr (Sum.inr x) => rfl) - μ'_natural_left := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + μ'_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl (Sum.inl x) => rfl | Sum.inl (Sum.inr x) => rfl | Sum.inr (Sum.inl x) => rfl | Sum.inr (Sum.inr x) => rfl - μ'_natural_right := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + μ'_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl (Sum.inl x) => rfl | Sum.inl (Sum.inr x) => rfl | Sum.inr (Sum.inl x) => rfl | Sum.inr (Sum.inr x) => rfl - associativity' := fun X Y Z => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + associativity' X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl (Sum.inl (Sum.inl x)) => rfl | Sum.inl (Sum.inl (Sum.inr x)) => rfl @@ -82,60 +85,67 @@ instance tensor_laxMonoidal (C : Type) : Functor.LaxMonoidal (tensor C) where | Sum.inl (Sum.inr (Sum.inr x)) => rfl | Sum.inr (Sum.inl x) => rfl | Sum.inr (Sum.inr x) => rfl - left_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + left_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl x => exact Empty.elim x | Sum.inr (Sum.inl x)=> rfl | Sum.inr (Sum.inr x)=> rfl - right_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by + right_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by match x with | Sum.inl (Sum.inl x) => rfl | Sum.inl (Sum.inr x) => rfl | Sum.inr x => exact Empty.elim x +/-- The functor tensor is monoidal. -/ noncomputable instance tensor_monoidal (C : Type) : Functor.Monoidal (tensor C) := Functor.Monoidal.ofLaxMonoidal _ /-- The constant monoidal functor from `OverColor C` to itself landing on `𝟙_ (OverColor C)`. -/ def const (C : Type) : Functor (OverColor C) (OverColor C) := - (Functor.const (OverColor C)).obj (𝟙_ (OverColor C)) + (Functor.const (OverColor C)).obj (𝟙_ (OverColor C)) +/-- The functor `const C` is lax monoidal. -/ instance const_laxMonoidal (C : Type) : Functor.LaxMonoidal (const C) where ε' := 𝟙 (𝟙_ (OverColor C)) μ' := fun _ _ => (λ_ (𝟙_ (OverColor C))).hom - μ'_natural_left := fun _ _ => by + μ'_natural_left := fun _ _ => by simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerRight_id, Category.id_comp, Iso.hom_inv_id, Category.comp_id, const] μ'_natural_right := fun _ _ => by simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerLeft_id, Category.id_comp, Category.comp_id, const] - associativity' := fun X Y Z => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by + associativity' X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => match i with | Sum.inl (Sum.inl i) => rfl | Sum.inl (Sum.inr i) => rfl | Sum.inr i => rfl - left_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by + left_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => match i with - | Sum.inl i => exact Empty.elim i - | Sum.inr i => exact Empty.elim i - right_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by + | Sum.inl i => Empty.elim i + | Sum.inr i => Empty.elim i + right_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => match i with - | Sum.inl i => exact Empty.elim i - | Sum.inr i => exact Empty.elim i + | Sum.inl i => Empty.elim i + | Sum.inr i => Empty.elim i +/-- The functor `const C` is monoidal. -/ noncomputable instance const_monoidal (C : Type) : Functor.Monoidal (const C) := Functor.Monoidal.ofLaxMonoidal _ /-- The monoidal functor from `OverColor C` to `OverColor C` taking `f` to `f ⊗ τ_* f`. -/ def contrPair (C : Type) (τ : C → C) : Functor (OverColor C) (OverColor C) := - (Functor.diag (OverColor C)) + (Functor.diag (OverColor C)) ⋙ (Functor.prod (Functor.id (OverColor C)) (OverColor.map τ)) ⋙ (OverColor.tensor C) +/-- The functor `contrPair` is lax-monoidal. -/ instance contrPair_laxMonoidal (C : Type) (τ : C → C) : Functor.LaxMonoidal (contrPair C τ) := Functor.LaxMonoidal.comp (Functor.diag (OverColor C)) ((𝟭 (OverColor C)).prod (map τ) ⋙ tensor C) -noncomputable instance contrPair_monoidal (C : Type) (τ : C → C) : Functor.Monoidal (contrPair C τ) := +/-- The functor `contrPair` is monoidal. -/ +noncomputable instance contrPair_monoidal (C : Type) (τ : C → C) : + Functor.Monoidal (contrPair C τ) := Functor.Monoidal.ofLaxMonoidal _ + end OverColor end IndexNotation diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean index 599d8d0b..7a314ff3 100644 --- a/HepLean/Tensors/OverColor/Lift.lean +++ b/HepLean/Tensors/OverColor/Lift.lean @@ -551,13 +551,14 @@ lemma objMap'_comp {X Y Z : OverColor C} (f : X ⟶ Y) (g : Y ⟶ Z) : rw [discreteFun_hom_trans] rfl -/-- The `BraidedFunctor (OverColor C) (Rep k G)` from a functor `Discrete C ⥤ Rep k G`. -/ +/-- The `Functor (OverColor C) (Rep k G)` from a functor `Discrete C ⥤ Rep k G`. -/ def obj' : Functor (OverColor C) (Rep k G) where obj := objObj' F map := objMap' F - map_comp := fun f g => objMap'_comp F f g + map_comp := fun f g => objMap'_comp F f g map_id := fun f => objMap'_id F f +/-- The lift of a functor is lax braided. -/ instance obj'_laxBraidedFunctor : Functor.LaxBraided (obj' F) where ε' := (ε F).hom μ' := fun X Y => (μ F X Y).hom @@ -571,12 +572,17 @@ instance obj'_laxBraidedFunctor : Functor.LaxBraided (obj' F) where rw [braided F X Y] simp +/-- The lift of a functor is monoidal. -/ instance obj'_monoidalFunctor : Functor.Monoidal (obj' F) := haveI : IsIso (Functor.LaxMonoidal.ε (obj' F)) := Action.isIso_of_hom_isIso (ε F).hom haveI : (∀ (X Y : OverColor C), IsIso (Functor.LaxMonoidal.μ (obj' F) X Y)) := fun X Y => Action.isIso_of_hom_isIso ((μ F X Y).hom) Functor.Monoidal.ofLaxMonoidal _ +/-- The lift of a functor is braided. -/ +instance obj'_braided : Functor.Braided (obj' F) := Functor.Braided.mk (fun X Y => + Functor.LaxBraided.braided X Y) + variable {F F' : Discrete C ⥤ Rep k G} (η : F ⟶ F') /-- The maps for a natural transformation between `obj' F` and `obj' F'`. -/ @@ -680,10 +686,11 @@ lemma mapApp'_tensor (X Y : OverColor C) : /-- Given a natural transformation between `F F' : Discrete C ⥤ Rep k G` the monoidal natural transformation between `obj' F` and `obj' F'`. -/ -def map' : (obj' F) ⟶ (obj' F') where +def map' : (obj' F) ⟶ (obj' F') where app := mapApp' η naturality _ _ f := mapApp'_naturality η f +/-- The lift of a natural transformation is monoidal. -/ instance map'_isMonoidal : NatTrans.IsMonoidal (map' η) where unit := mapApp'_unit η tensor := mapApp'_tensor η @@ -736,10 +743,13 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ LaxBraidedFunctor (OverCol namespace lift variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F') +/-- The lift of a functor is monoidal. -/ noncomputable instance : (lift.obj F).Monoidal := obj'_monoidalFunctor F +/-- The lift of a functor is lax-braided. -/ noncomputable instance : (lift.obj F).LaxBraided := obj'_laxBraidedFunctor F +/-- The lift of a functor is braided. -/ noncomputable instance : (lift.obj F).Braided := Functor.Braided.mk (fun X Y => Functor.LaxBraided.braided X Y) @@ -754,7 +764,8 @@ lemma map_tprod (F : Discrete C ⥤ Rep k G) {X Y : OverColor C} (f : X ⟶ Y) lemma obj_μ_tprod_tmul (F : Discrete C ⥤ Rep k G) (X Y : OverColor C) (p : (i : X.left) → (F.obj (Discrete.mk <| X.hom i))) (q : (i : Y.left) → F.obj (Discrete.mk <| Y.hom i)) : - (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) = + (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom + (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) = (PiTensorProduct.tprod k) fun i => discreteSumEquiv F i (HepLean.PiTensorProduct.elimPureTensor p q i) := by exact μ_tmul_tprod F p q @@ -764,12 +775,14 @@ lemma μIso_inv_tprod (F : Discrete C ⥤ Rep k G) (X Y : OverColor C) (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y).inv.hom (PiTensorProduct.tprod k p) = (PiTensorProduct.tprod k (fun i => p (Sum.inl i))) ⊗ₜ[k] (PiTensorProduct.tprod k (fun i => p (Sum.inr i))) := by - change ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).inv (PiTensorProduct.tprod k p) = _ - trans ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).toLinearEquiv.symm + change ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).inv + (PiTensorProduct.tprod k p) = _ + trans ((Action.forget _ _).mapIso + (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).toLinearEquiv.symm (PiTensorProduct.tprod k p) · rfl erw [← LinearEquiv.eq_symm_apply] - change _ = (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom _ + change _ = (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom _ erw [obj_μ_tprod_tmul] congr funext i diff --git a/HepLean/Tensors/TensorSpecies/Basic.lean b/HepLean/Tensors/TensorSpecies/Basic.lean index db1c058c..29dd8b5c 100644 --- a/HepLean/Tensors/TensorSpecies/Basic.lean +++ b/HepLean/Tensors/TensorSpecies/Basic.lean @@ -111,14 +111,18 @@ def F : Functor (OverColor S.C) (Rep S.k S.G) := ((OverColor.lift).obj S.FD).toF /- The definition of `F` as a lemma. -/ lemma F_def : F S = ((OverColor.lift).obj S.FD).toFunctor := rfl -instance F_monoidal : Functor.Monoidal S.F := lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor S.FD +/-- The functor `F` is monoidal. -/ +instance F_monoidal : Functor.Monoidal S.F := + lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor S.FD -instance F_laxBraided : Functor.LaxBraided S.F := lift.instLaxBraidedRepObjFunctorDiscreteLaxBraidedFunctor S.FD +/-- The functor `F` is lax-braided. -/ +instance F_laxBraided : Functor.LaxBraided S.F := + lift.instLaxBraidedRepObjFunctorDiscreteLaxBraidedFunctor S.FD +/-- The functor `F` is braided. -/ instance F_braided : Functor.Braided S.F := Functor.Braided.mk (fun X Y => Functor.LaxBraided.braided X Y) - lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (h : c1 (i.succAbove j) = S.τ (c1 i)) (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) : diff --git a/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean b/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean index 3b8065d9..b1dc6c36 100644 --- a/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean +++ b/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean @@ -152,7 +152,8 @@ lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C} (S.contrIso c1 i j h).hom.hom = (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom ≫ (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom ≫ - (Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) + (Functor.Monoidal.μIso S.F + (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom ≫ ((S.contrFin1Fin1 c1 i j h).hom.hom ⊗ (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom) := by @@ -192,8 +193,8 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C) (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V) (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom) - ((Functor.Monoidal.μIso (lift.obj S.FD).toFunctor (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) - ∘ Sum.inl)) + ((Functor.Monoidal.μIso (lift.obj S.FD).toFunctor + (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom (((lift.obj S.FD).map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean index 88358a77..6511800f 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean @@ -312,14 +312,15 @@ lemma prod_action {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (g : S. simp only [prod_tensor, action_tensor, map_tmul] change _ = ((S.F.map (equivToIso finSumFinEquiv).hom).hom ≫ (S.F.obj (OverColor.mk (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm))).ρ g) - (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom (t.tensor ⊗ₜ[S.k] t1.tensor))) + (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom + (t.tensor ⊗ₜ[S.k] t1.tensor))) erw [← (S.F.map (equivToIso finSumFinEquiv).hom).comm g] simp only [Action.forget_obj, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply] change _ = (S.F.map (equivToIso finSumFinEquiv).hom).hom - (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom ≫ (S.F.obj (OverColor.mk (Sum.elim c c1))).ρ g) - (t.tensor ⊗ₜ[S.k] t1.tensor)) + (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom ≫ + (S.F.obj (OverColor.mk (Sum.elim c c1))).ρ g) (t.tensor ⊗ₜ[S.k] t1.tensor)) erw [← (Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).comm g] rfl diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean index 64e045a5..efb0911b 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean @@ -117,14 +117,17 @@ lemma contrIso_comm_aux_2 {n : ℕ} {c c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) : (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)).hom ≫ - (Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) + (Functor.Monoidal.μIso S.F + (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom = (Functor.Monoidal.μIso S.F _ _).inv.hom ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)).hom := by have h1 : (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)) ≫ - (Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) + (Functor.Monoidal.μIso S.F + (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv = - (Functor.Monoidal.μIso S.F _ _).inv ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)) := by + (Functor.Monoidal.μIso S.F _ _).inv ≫ + (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)) := by erw [CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.Category.assoc] erw [CategoryTheory.IsIso.eq_inv_comp] exact (Functor.LaxMonoidal.μ_natural S.F (extractTwoAux' i j σ) (extractTwoAux i j σ)).symm diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean b/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean index bf355d2c..1df572e2 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean @@ -54,7 +54,8 @@ theorem prod_perm_left (t : TensorTree S c) (t2 : TensorTree S c2) : Action.FunctorCategoryEquivalence.functor_obj_obj, perm_tensor] change (S.F.map (equivToIso finSumFinEquiv).hom).hom (((S.F.map (σ) ▷ S.F.obj (OverColor.mk c2)) ≫ - Functor.LaxMonoidal.μ S.F (OverColor.mk c') (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor)) = _ + Functor.LaxMonoidal.μ S.F (OverColor.mk c') (OverColor.mk c2)).hom + (t.tensor ⊗ₜ[S.k] t2.tensor)) = _ rw [Functor.LaxMonoidal.μ_natural_left] simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, @@ -72,7 +73,8 @@ theorem prod_perm_right (t2 : TensorTree S c2) (t : TensorTree S c) : Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, perm_tensor] change (S.F.map (equivToIso finSumFinEquiv).hom).hom - (((S.F.obj (OverColor.mk c2) ◁ S.F.map σ) ≫ Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c')).hom + (((S.F.obj (OverColor.mk c2) ◁ S.F.map σ) ≫ + Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c')).hom (t2.tensor ⊗ₜ[S.k] t.tensor)) = _ rw [Functor.LaxMonoidal.μ_natural_right] simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom, diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean index 80e3a5e6..1ee32810 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean @@ -63,8 +63,8 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree rw [perm_tensor] nth_rewrite 2 [prod_tensor] change _ = ((S.F.map (equivToIso finSumFinEquiv).hom) ≫ S.F.map (assocPerm c c2 c3).hom).hom - (((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3)).hom - ((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor))) + (((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) + (OverColor.mk c3)).hom ((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor))) rw [← S.F.map_comp, finSumFinEquiv_comp_assocPerm] simp only [Functor.id_obj, mk_hom, whiskerRightIso_hom, Iso.symm_hom, whiskerLeftIso_hom, Functor.map_comp, Action.comp_hom, Action.instMonoidalCategory_tensorObj_V, @@ -74,7 +74,8 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree apply congrArg change _ = (S.F.map (OverColor.mk c ◁ (equivToIso finSumFinEquiv).hom)).hom ((S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom - ((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3) + ((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) + (OverColor.mk c3) ≫ S.F.map ((equivToIso finSumFinEquiv).inv ▷ OverColor.mk c3)).hom (((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor)))) rw [← Functor.LaxMonoidal.μ_natural_left] @@ -91,8 +92,8 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree ((S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom ((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2)) (OverColor.mk c3)).hom ((S.F.map (equivToIso finSumFinEquiv).hom ≫ S.F.map (equivToIso finSumFinEquiv).inv).hom - (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor))) ⊗ₜ[S.k] - t3.tensor))) + (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c2)).hom + (t.tensor ⊗ₜ[S.k] t2.tensor))) ⊗ₜ[S.k] t3.tensor))) simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, Iso.map_hom_inv_id, Action.id_hom, @@ -110,9 +111,11 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree ModuleCat.MonoidalCategory.associator_hom_apply] rw [prod_tensor] change ((_ ◁ (S.F.map (equivToIso finSumFinEquiv).hom)) ≫ - Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm))).hom + Functor.LaxMonoidal.μ S.F (OverColor.mk c) + (OverColor.mk (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm))).hom (t.tensor ⊗ₜ[S.k] - ((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c3)).hom (t2.tensor ⊗ₜ[S.k] t3.tensor))) = _ + ((Functor.LaxMonoidal.μ S.F + (OverColor.mk c2) (OverColor.mk c3)).hom (t2.tensor ⊗ₜ[S.k] t3.tensor))) = _ rw [Functor.LaxMonoidal.μ_natural_right] simp only [Action.instMonoidalCategory_tensorObj_V, Action.comp_hom, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean index ec687262..7526f17f 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean @@ -49,7 +49,8 @@ theorem prod_comm (t : TensorTree S c) (t2 : TensorTree S c2) : rw [perm_tensor] nth_rewrite 2 [prod_tensor] change _ = (S.F.map (equivToIso finSumFinEquiv).hom ≫ S.F.map (braidPerm c c2)).hom - ((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c)).hom (t2.tensor ⊗ₜ[S.k] t.tensor)) + ((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c)).hom + (t2.tensor ⊗ₜ[S.k] t.tensor)) rw [← S.F.map_comp] rw [finSumFinEquiv_comp_braidPerm] rw [S.F.map_comp] diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean index 0e416d25..df7f736e 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean @@ -172,7 +172,8 @@ lemma contrMap_prod_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c).left) → (q' : (i : (𝟭 Type).obj (OverColor.mk c1).left) → CoeSort.coe (S.FD.obj { as := (OverColor.mk c1).hom i })) : (S.F.map (equivToIso finSumFinEquiv).hom).hom - ((Functor.LaxMonoidal.μ S.F (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) (OverColor.mk c1)).hom + ((Functor.LaxMonoidal.μ S.F + (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) (OverColor.mk c1)).hom ((q.contrMap.hom (PiTensorProduct.tprod S.k p)) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) q')) = (S.F.map (mkIso (by exact leftContr_map_eq q)).hom).hom (q.leftContr.contrMap.hom @@ -288,7 +289,8 @@ lemma contr_prod q.leftContr.h (perm (OverColor.equivToIso ContrPair.leftContrEquivSuccSucc).hom (prod t t1)))).tensor) := by simp only [contr_tensor, perm_tensor, prod_tensor] - change ((q.contrMap ▷ S.F.obj (OverColor.mk c1)) ≫ (Functor.LaxMonoidal.μ S.F _ ((OverColor.mk c1))) ≫ + change ((q.contrMap ▷ S.F.obj (OverColor.mk c1)) ≫ + (Functor.LaxMonoidal.μ S.F _ ((OverColor.mk c1))) ≫ S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom (t.tensor ⊗ₜ[S.k] t1.tensor) = _ rw [contrMap_prod] simp only [Nat.succ_eq_add_one, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, @@ -405,7 +407,8 @@ lemma prod_contrMap_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c1).left) → (q' : (i : (𝟭 Type).obj (OverColor.mk c).left) → CoeSort.coe (S.FD.obj { as := (OverColor.mk c).hom i })) : (S.F.map (equivToIso finSumFinEquiv).hom).hom - ((Functor.LaxMonoidal.μ S.F (OverColor.mk c1) (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))).hom + ((Functor.LaxMonoidal.μ S.F (OverColor.mk c1) + (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))).hom ((PiTensorProduct.tprod S.k) p ⊗ₜ[S.k] (q.contrMap.hom (PiTensorProduct.tprod S.k q')))) = (S.F.map (mkIso (by exact (rightContr_map_eq q))).hom).hom (q.rightContr.contrMap.hom @@ -530,7 +533,8 @@ lemma prod_contr (t1 : TensorTree S c1) (t : TensorTree S c) : (contr (q.rightContrI n1) (q.rightContrJ n1) q.rightContr.h (prod t1 t))).tensor) := by simp only [contr_tensor, perm_tensor, prod_tensor] - change ((S.F.obj (OverColor.mk c1) ◁ q.contrMap) ≫ (Functor.LaxMonoidal.μ S.F ((OverColor.mk c1)) _) ≫ + change ((S.F.obj (OverColor.mk c1) ◁ q.contrMap) ≫ + (Functor.LaxMonoidal.μ S.F ((OverColor.mk c1)) _) ≫ S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom (t1.tensor ⊗ₜ[S.k] t.tensor) = _ rw [prod_contrMap] simp only [Nat.succ_eq_add_one, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, diff --git a/scripts/lint_all.lean b/scripts/lint_all.lean index 34e22eff..bd02b41e 100644 --- a/scripts/lint_all.lean +++ b/scripts/lint_all.lean @@ -11,15 +11,15 @@ import HepLean.Meta.Informal.Post import ImportGraph.RequiredModules def main (_: List String) : IO UInt32 := do + println! "Style lint ... " + let styleLint ← IO.Process.output {cmd := "lake", args := #["exe", "hepLean_style_lint"]} + println! styleLint.stdout println! "Building ... " let build ← IO.Process.output {cmd := "lake", args := #["build"]} println! build.stdout println! "File imports ... " let importCheck ← IO.Process.output {cmd := "lake", args := #["exe", "check_file_imports"]} println! importCheck.stdout - println! "Style lint ... " - let styleLint ← IO.Process.output {cmd := "lake", args := #["exe", "hepLean_style_lint"]} - println! styleLint.stdout println! "Doc check ..." let docCheck ← IO.Process.output {cmd := "lake", args := #["exe", "no_docs"]} println! docCheck.stdout From 0595ceddfff4c367944fb2d3762da39b288e6acb Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 10 Dec 2024 14:05:41 +0000 Subject: [PATCH 3/5] refactor: free_simps --- HepLean/Tensors/OverColor/Lift.lean | 3 ++- HepLean/Tensors/TensorSpecies/UnitTensor.lean | 4 +++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean index 7a314ff3..e9765a4b 100644 --- a/HepLean/Tensors/OverColor/Lift.lean +++ b/HepLean/Tensors/OverColor/Lift.lean @@ -707,7 +707,8 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ LaxBraidedFunctor (OverCol simp only [lift.map'] refine LaxMonoidalFunctor.hom_ext ?_ ext X : 2 - simp + simp only [LaxBraidedFunctor.toLaxMonoidalFunctor_toFunctor, LaxBraidedFunctor.of_toFunctor, + LaxMonoidalFunctor.homMk_hom, LaxBraidedFunctor.id_hom, NatTrans.id_app] ext x refine PiTensorProduct.induction_on' x ?_ (by intro x y hx hy diff --git a/HepLean/Tensors/TensorSpecies/UnitTensor.lean b/HepLean/Tensors/TensorSpecies/UnitTensor.lean index 0c5d4f42..a7c93f9b 100644 --- a/HepLean/Tensors/TensorSpecies/UnitTensor.lean +++ b/HepLean/Tensors/TensorSpecies/UnitTensor.lean @@ -56,7 +56,9 @@ lemma unitTensor_eq_dual_perm (c : S.C) : {S.unitTensor c | μ ν}ᵀ.tensor = ({S.unitTensor (S.τ c) | ν μ }ᵀ |> perm (OverColor.equivToHomEq (finMapToEquiv ![1,0] ![1, 0]) (fun x => match x with | 0 => by rfl | 1 => (S.τ_involution c).symm))).tensor := by - simp [unitTensor, tensorNode_tensor, perm_tensor] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, unitTensor, + Action.instMonoidalCategory_tensorObj_V, Monoidal.tensorUnit_obj, + Action.instMonoidalCategory_tensorUnit_V, tensorNode_tensor, Fin.isValue, perm_tensor] have h1 := S.unit_symm c erw [h1] have hg : (Discrete.pairIsoSep S.FD).hom.hom ∘ₗ (S.FD.obj { as := S.τ c } ◁ From d8bac41b1b6d085cac897e38bf51224627996b69 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 10 Dec 2024 14:06:56 +0000 Subject: [PATCH 4/5] chore: Change name from hep_lean to HepLean --- lakefile.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.toml b/lakefile.toml index 4f09c806..f223dc76 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,4 +1,4 @@ -name = "hep_lean" +name = "HepLean" defaultTargets = ["HepLean"] # -- Optional inclusion for LeanCopilot #moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"] From a0e951fc1662285efc2c6f0891f5936b7b854d5b Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 10 Dec 2024 14:13:09 +0000 Subject: [PATCH 5/5] Update lake-manifest.json --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 8f020b7b..e444a4b3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -131,5 +131,5 @@ "inputRev": "v4.14.0", "inherited": true, "configFile": "lakefile.toml"}], - "name": "hep_lean", + "name": "HepLean", "lakeDir": ".lake"}