diff --git a/BrauerGroup.lean b/BrauerGroup.lean index 6626b90..850f250 100644 --- a/BrauerGroup.lean +++ b/BrauerGroup.lean @@ -5,10 +5,12 @@ import BrauerGroup.Composition import BrauerGroup.Con import BrauerGroup.Dual import BrauerGroup.GaloisDescent.Basic +import BrauerGroup.LinearMap import BrauerGroup.MoritaEquivalence import BrauerGroup.PiTensorProduct import BrauerGroup.QuadraticExtension import BrauerGroup.QuatBasic import BrauerGroup.Quaternion import BrauerGroup.TensorOfTypePQ.Basic +import BrauerGroup.TensorOfTypePQ.VectorSpaceWithTensorOfTypePQ import BrauerGroup.Wedderburn diff --git a/BrauerGroup/BAK/eagle.lean.bak b/BrauerGroup/BAK/eagle.lean.bak new file mode 100644 index 0000000..e5bf69f --- /dev/null +++ b/BrauerGroup/BAK/eagle.lean.bak @@ -0,0 +1,155 @@ + + +-- #exit +-- section PiTensorProduct.fin + +-- variable {n : ℕ} (k K : Type*) [CommSemiring k] [CommSemiring K] [Algebra k K] +-- variable (V : Fin (n + 1) → Type*) [Π i, AddCommMonoid (V i)] [Π i, Module k (V i)] +-- variable (W : Fin (n + 1) → Type*) [Π i, AddCommMonoid (W i)] [Π i, Module k (W i)] + +-- def PiTensorProduct.succ : (⨂[k] i, V i) ≃ₗ[k] V 0 ⊗[k] (⨂[k] i : Fin n, V i.succ) := +-- LinearEquiv.ofLinear +-- (PiTensorProduct.lift +-- { toFun := fun v => v 0 ⊗ₜ[k] tprod k fun i => v i.succ +-- map_add' := by +-- intro _ v i x y +-- simp only +-- by_cases h : i = 0 +-- · subst h +-- simp only [Function.update_same] +-- rw [add_tmul] +-- congr 3 <;> +-- · ext i +-- rw [Function.update_noteq (h := Fin.succ_ne_zero i), +-- Function.update_noteq (h := Fin.succ_ne_zero i)] + +-- rw [Function.update_noteq (Ne.symm h), Function.update_noteq (Ne.symm h), +-- Function.update_noteq (Ne.symm h), ← tmul_add] +-- congr 1 +-- have eq1 : (fun j : Fin n ↦ Function.update v i (x + y) j.succ) = +-- Function.update (fun i : Fin n ↦ v i.succ) (i.pred h) +-- (cast (by simp) x + cast (by simp) y):= by +-- ext j +-- simp only [Function.update, eq_mpr_eq_cast] +-- aesop +-- rw [eq1, (tprod k).map_add] +-- congr 2 <;> +-- ext j <;> +-- simp only [Function.update] <;> +-- have eq : (j = i.pred h) = (j.succ = i) := by +-- rw [← iff_eq_eq] +-- constructor +-- · rintro rfl +-- exact Fin.succ_pred i h +-- · rintro rfl +-- simp only [Fin.pred_succ] +-- · simp_rw [eq] <;> aesop +-- · simp_rw [eq] <;> aesop +-- map_smul' := by +-- intro _ v i a x +-- simp only +-- rw [smul_tmul', smul_tmul] +-- by_cases h : i = 0 +-- · subst h +-- simp only [Function.update_same, tmul_smul] +-- rw [smul_tmul'] +-- congr 2 +-- ext j +-- rw [Function.update_noteq (Fin.succ_ne_zero j), +-- Function.update_noteq (Fin.succ_ne_zero j)] +-- · rw [Function.update_noteq (Ne.symm h), Function.update_noteq (Ne.symm h)] +-- congr 1 +-- have eq1 : (fun j : Fin n ↦ Function.update v i (a • x) j.succ) = +-- Function.update (fun i : Fin n ↦ v i.succ) (i.pred h) +-- (a • cast (by simp) x):= by +-- ext j +-- simp only [Function.update, eq_mpr_eq_cast] +-- aesop +-- rw [eq1, (tprod k).map_smul] +-- congr +-- ext j +-- simp only [Function.update] +-- have eq : (j = i.pred h) = (j.succ = i) := by +-- rw [← iff_eq_eq] +-- constructor +-- · rintro rfl +-- exact Fin.succ_pred i h +-- · rintro rfl +-- simp only [Fin.pred_succ] +-- simp_rw [eq] <;> aesop }) +-- (TensorProduct.lift +-- { toFun := fun v₀ => PiTensorProduct.lift +-- { toFun := fun v => tprod k $ Fin.cases v₀ v +-- map_add' := sorry +-- map_smul' := sorry } +-- map_add' := sorry +-- map_smul' := sorry }) sorry sorry + +-- end PiTensorProduct.fin + + +-- section PiTensorProduct.fin + +-- variable {k K : Type*} [Field k] [Field K] [Algebra k K] +-- variable {V W : Type*} [AddCommGroup V] [AddCommGroup W] [Module k V] [Module k W] + +-- variable (k) in +-- def zeroPower (ι : Type*) (V : ι → Type*) [hι: IsEmpty ι] +-- [∀ i, AddCommGroup $ V i] [∀ i, Module k $ V i]: (⨂[k] i : ι, V i) ≃ₗ[k] k := +-- LinearEquiv.ofLinear +-- (PiTensorProduct.lift +-- { toFun := fun _ ↦ 1 +-- map_add' := by +-- intros; exact hι.elim (by assumption) +-- map_smul' := by +-- intros; exact hι.elim (by assumption) }) +-- { toFun := fun a ↦ a • tprod k fun x ↦ hι.elim x +-- map_add' := by +-- intro x y +-- simp only [self_eq_add_right, add_smul] +-- map_smul' := by +-- intro m x +-- simp [mul_smul] +-- } +-- (by +-- refine LinearMap.ext_ring ?h +-- simp only [LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, one_smul, +-- lift.tprod, MultilinearMap.coe_mk, LinearMap.id_coe, id_eq]) +-- (by +-- ext x +-- simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearMap.coe_mk, +-- AddHom.coe_mk, Function.comp_apply, lift.tprod, MultilinearMap.coe_mk, one_smul, +-- LinearMap.id_coe, id_eq] +-- refine MultilinearMap.congr_arg (tprod k) ?_ +-- ext y +-- exact hι.elim y) + +-- variable (k) in +-- def PiTensorProduct.tensorCommutes (n : ℕ) : +-- ∀ (V W : Fin n → Type*) +-- [∀ i, AddCommGroup (V i)] [∀ i, Module k (V i)] +-- [∀ i, AddCommGroup (W i)] [∀ i, Module k (W i)], +-- (⨂[k] i : Fin n, V i) ⊗[k] (⨂[k] i : Fin n, W i) ≃ₗ[k] +-- ⨂[k] i : Fin n, (V i ⊗[k] W i) := +-- n.recOn +-- (fun V W _ _ _ _ ↦ LinearEquiv.symm $ zeroPower k (Fin 0) (fun i : (Fin 0) ↦ V i ⊗[k] W i) ≪≫ₗ +-- (TensorProduct.lid k k).symm ≪≫ₗ TensorProduct.congr (zeroPower k (Fin 0) _).symm +-- (zeroPower k (Fin 0) _).symm) +-- (fun m em V W _ _ _ _ ↦ +-- (TensorProduct.congr (PiTensorProduct.succ k (fun i : Fin (m+1) ↦ V i)) +-- (PiTensorProduct.succ k (fun i : Fin (m+1) ↦ W i))) ≪≫ₗ +-- (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm k k _ _ _ _) ≪≫ₗ +-- LinearEquiv.symm +-- ((PiTensorProduct.succ (n := m) k (V := fun i : Fin (m.succ) ↦ (V i ⊗[k] W i))) ≪≫ₗ +-- TensorProduct.congr (LinearEquiv.refl _ _) +-- (em (fun i => V i.succ) (fun i => W i.succ)).symm)) + +-- theorem PiTensorProduct.tensorCommutes_apply (n : ℕ) (V W : Fin n → Type*) +-- [hi1 : ∀ i, AddCommGroup (V i)] [hi2 : ∀ i, Module k (V i)] +-- [hi1' : ∀ i, AddCommGroup (W i)] [hi2' : ∀ i, Module k (W i)] +-- (v : Π i : Fin n, V i) (w : Π i : Fin n, W i) : +-- PiTensorProduct.tensorCommutes k n V W ((tprod k v) ⊗ₜ (tprod k w)) = +-- tprod k (fun i ↦ v i ⊗ₜ w i) := by +-- sorry + +-- end PiTensorProduct.fin \ No newline at end of file diff --git a/BrauerGroup/junqi.lean.bak b/BrauerGroup/BAK/junqi.lean.bak similarity index 100% rename from BrauerGroup/junqi.lean.bak rename to BrauerGroup/BAK/junqi.lean.bak diff --git a/BrauerGroup/GaloisDescent/Basic.lean b/BrauerGroup/GaloisDescent/Basic.lean index e69de29..37907d9 100644 --- a/BrauerGroup/GaloisDescent/Basic.lean +++ b/BrauerGroup/GaloisDescent/Basic.lean @@ -0,0 +1,171 @@ +import BrauerGroup.TensorOfTypePQ.VectorSpaceWithTensorOfTypePQ + +import Mathlib.RepresentationTheory.GroupCohomology.LowDegree +import Mathlib.FieldTheory.Galois + +suppress_compilation + +universe u v w + +open TensorProduct PiTensorProduct CategoryTheory + +variable {k K : Type u} {p q : ℕ} [Field k] [Field K] [Algebra k K] +variable {V W W' : VectorSpaceWithTensorOfType.{u, u} k p q} +variable {ιV ιW ιW' : Type*} (bV : Basis ιV k V) (bW : Basis ιW k W) (bW' : Basis ιW' k W') + +open VectorSpaceWithTensorOfType + +set_option maxHeartbeats 500000 in + +lemma indeucedByGalAux_comm (σ : K ≃ₐ[k] K) + (f : V.extendScalars K bV ⟶ W.extendScalars K bW) : + (TensorOfType.extendScalars K bW W.tensor ∘ₗ + PiTensorProduct.map fun _ ↦ LinearMap.galAct σ f.toLinearMap) = + (PiTensorProduct.map fun _ ↦ LinearMap.galAct σ f.toLinearMap) ∘ₗ + TensorOfType.extendScalars K bV V.tensor := by + apply_fun LinearMap.restrictScalars k using LinearMap.restrictScalars_injective k + rw [LinearMap.restrictScalars_comp, LinearMap.restrictScalars_comp, + VectorSpaceWithTensorOfType.galAct_tensor_power_eq, ← LinearMap.comp_assoc, + VectorSpaceWithTensorOfType.galAct_tensor_power_eq] + have := VectorSpaceWithTensorOfType.oneTMulPow_comm_sq bW σ.toAlgHom + simp only [extendScalars_carrier, extendScalars_tensor, AlgEquiv.toAlgHom_eq_coe] at this + set lhs := _; change lhs = _ + rw [show lhs = (AlgHom.oneTMulPow p bW ↑σ ∘ₗ LinearMap.restrictScalars k (TensorOfType.extendScalars K bW W.tensor)) ∘ₗ + LinearMap.restrictScalars k (PiTensorProduct.map fun _ ↦ f.toLinearMap) ∘ₗ + AlgHom.oneTMulPow q bV σ.symm.toAlgHom by + simp only [AlgEquiv.toAlgHom_eq_coe, extendScalars_carrier, lhs] + rw [this]] + clear lhs + rw [LinearMap.comp_assoc, ← LinearMap.comp_assoc (f := AlgHom.oneTMulPow q bV _)] + have eq := congr(LinearMap.restrictScalars k $f.comm) + simp only [extendScalars_carrier, extendScalars_tensor, LinearMap.restrictScalars_comp] at eq + rw [eq] + rw [LinearMap.comp_assoc] + have := VectorSpaceWithTensorOfType.oneTMulPow_comm_sq bV σ.symm.toAlgHom + simp only [extendScalars_carrier, extendScalars_tensor, AlgEquiv.toAlgHom_eq_coe] at this + set lhs := _; change lhs = _ + rw [show lhs = AlgHom.oneTMulPow p bW ↑σ ∘ₗ + LinearMap.restrictScalars k (PiTensorProduct.map fun _ ↦ f.toLinearMap) ∘ₗ + AlgHom.oneTMulPow p bV ↑σ.symm ∘ₗ + LinearMap.restrictScalars k (TensorOfType.extendScalars K bV V.tensor) by + simp only [AlgEquiv.toAlgHom_eq_coe, extendScalars_carrier, lhs] + rw [this]] + clear lhs + simp only [extendScalars_carrier, ← LinearMap.comp_assoc] + rfl + +variable {bV bW} in +def homInducedByGal (σ : K ≃ₐ[k] K) (f : V.extendScalars K bV ⟶ W.extendScalars K bW) : + V.extendScalars K bV ⟶ W.extendScalars K bW where + __ := LinearMap.galAct σ f.toLinearMap + comm := by + simp only [extendScalars_carrier, extendScalars_tensor] + apply indeucedByGalAux_comm + +instance : SMul (K ≃ₐ[k] K) (V.extendScalars K bV ⟶ W.extendScalars K bW) where + smul σ f := homInducedByGal σ f + +@[simp] +lemma homInducedByGal_toLinearMap + (σ : K ≃ₐ[k] K) (f : V.extendScalars K bV ⟶ W.extendScalars K bW) : + (homInducedByGal σ f).toLinearMap = LinearMap.galAct σ f.toLinearMap := rfl + +lemma homInducedByGal_comp (σ : K ≃ₐ[k] K) + (f : V.extendScalars K bV ⟶ W.extendScalars K bW) + (g : W.extendScalars K bW ⟶ W'.extendScalars K bW') : + homInducedByGal σ (f ≫ g) = + homInducedByGal σ f ≫ homInducedByGal σ g := + Hom.toLinearMap_injective _ _ $ by + simp only [extendScalars_carrier, homInducedByGal_toLinearMap, comp_toLinearMap] + rw [LinearMap.galAct_comp] + +@[simp] +lemma homInducedByGal_one (σ : K ≃ₐ[k] K) : homInducedByGal σ (𝟙 (V.extendScalars K bV)) = 𝟙 _ := + Hom.toLinearMap_injective _ _ $ by + simp only [extendScalars_carrier, homInducedByGal_toLinearMap, id_toLinearMap] + rw [LinearMap.galAct_id] + +variable {bV bW} in +@[simps] +def isoInducedByGal (σ : K ≃ₐ[k] K) (f : V.extendScalars K bV ≅ W.extendScalars K bW) : + V.extendScalars K bV ≅ W.extendScalars K bW where + hom := homInducedByGal σ f.hom + inv := homInducedByGal σ f.inv + hom_inv_id := Hom.toLinearMap_injective _ _ $ by + simp only [extendScalars_carrier, comp_toLinearMap, homInducedByGal_toLinearMap, id_toLinearMap] + rw [← LinearMap.galAct_comp, ← comp_toLinearMap, f.hom_inv_id, id_toLinearMap, + LinearMap.galAct_id] + inv_hom_id := Hom.toLinearMap_injective _ _ $ by + simp only [extendScalars_carrier, comp_toLinearMap, homInducedByGal_toLinearMap, id_toLinearMap] + rw [← LinearMap.galAct_comp, ← comp_toLinearMap, f.inv_hom_id, id_toLinearMap, + LinearMap.galAct_id] + +variable {bV} in +abbrev autInducedByGal (σ : K ≃ₐ[k] K) (f : V.extendScalars K bV ≅ V.extendScalars K bV) : + V.extendScalars K bV ≅ V.extendScalars K bV := + isoInducedByGal σ f + +lemma autoInducedByGal_id (σ : K ≃ₐ[k] K) : + autInducedByGal σ (Iso.refl $ V.extendScalars K bV) = Iso.refl _ := by + ext + simp only [autInducedByGal, isoInducedByGal_hom, Iso.refl_hom, homInducedByGal_one] + +lemma autInducedByGal_trans (σ : K ≃ₐ[k] K) (f g : V.extendScalars K bV ≅ V.extendScalars K bV) : + autInducedByGal σ (f ≪≫ g) = + autInducedByGal σ f ≪≫ autInducedByGal σ g := by + ext + simp only [autInducedByGal, isoInducedByGal_hom, Iso.trans_hom, homInducedByGal_comp] + +variable (K) in +@[simps] +def act : Action (Type u) (MonCat.of $ K ≃ₐ[k] K) where + V := Aut (V.extendScalars K bV) + ρ := + { toFun := fun σ => autInducedByGal σ + map_one' := funext fun i => Iso.ext $ Hom.toLinearMap_injective _ _ $ + AlgebraTensorModule.curry_injective $ LinearMap.ext_ring $ LinearMap.ext fun x ↦ by + simp [show (1 : K →ₗ[k] K) = LinearMap.id by rfl] + map_mul' := fun σ τ => funext fun i => Iso.ext $ Hom.toLinearMap_injective _ _ $ + AlgebraTensorModule.curry_injective $ LinearMap.ext_ring $ LinearMap.ext fun x ↦ by + change _ = (autInducedByGal _ _).hom.toLinearMap (1 ⊗ₜ x) + simp only [extendScalars_carrier, autInducedByGal, MonCat.mul_of, isoInducedByGal_hom, + homInducedByGal_toLinearMap, AlgebraTensorModule.curry_apply, curry_apply, + LinearMap.coe_restrictScalars, LinearMap.galAct_extendScalars_apply, + show (AlgEquiv.toLinearMap (σ * τ)) = σ.toLinearMap ∘ₗ τ.toLinearMap by rfl, + LinearMap.rTensor_comp, _root_.map_one, LinearMap.coe_comp, Function.comp_apply] } + +variable (K) in +def rep : Rep (ULift ℤ) (K ≃ₐ[k] K) := Rep.linearization _ _ |>.obj $ act K bV + +section + +variable [IsGalois k K] (g : V.extendScalars K bV ⟶ W.extendScalars K bW) + +lemma homInducedByGal_extendScalarsMap_eq (f : V ⟶ W) (σ : K ≃ₐ[k] K) : + homInducedByGal σ (extendScalarsMap f bV bW) = extendScalarsMap f bV bW := by + apply Hom.toLinearMap_injective + simp only [extendScalars_carrier, homInducedByGal_toLinearMap, extendScalarsMap_toLinearMap] + ext v + simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars, + LinearMap.galAct_extendScalars_apply, _root_.map_one, LinearMap.extendScalars_apply, + LinearMap.rTensor_tmul, AlgEquiv.toLinearMap_apply] + +-- this is weird, we need non-abelian group cohomology +example (n : ℤ) (e : Aut V) : + Finsupp.single (autExtendScalars (K := K) e bV) ⟨n⟩ ∈ groupCohomology.H0 (rep K bV) := by + classical + simp only [rep, Representation.mem_invariants] + intro σ + erw [Rep.linearization_obj_ρ] + simp only [Finsupp.lmapDomain_apply, Finsupp.mapDomain_single] + simp only [act_V, act_ρ_apply] + ext f + have eq : autInducedByGal σ (autExtendScalars e bV) = autExtendScalars e bV := by + ext + simp only [isoInducedByGal_hom, autExtendScalars_hom] + apply homInducedByGal_extendScalarsMap_eq + rw [eq] + + + +end diff --git a/BrauerGroup/LinearMap.lean b/BrauerGroup/LinearMap.lean new file mode 100644 index 0000000..e414c6b --- /dev/null +++ b/BrauerGroup/LinearMap.lean @@ -0,0 +1,138 @@ +import Mathlib.RingTheory.TensorProduct.Basic +import Mathlib.LinearAlgebra.TensorPower + +suppress_compilation + +open TensorProduct + +section + +variable (k K V W W' : Type*) +variable {p q : ℕ} +variable [CommSemiring k] [Semiring K] [Algebra k K] +variable [AddCommMonoid V] [Module k V] +variable [AddCommMonoid W] [Module k W] +variable [AddCommMonoid W'] [Module k W'] + +variable {k V W} in +def _root_.LinearMap.extendScalars (f : V →ₗ[k] W) : K ⊗[k] V →ₗ[K] K ⊗[k] W := + { f.lTensor K with + map_smul' := fun a x => by + simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, RingHom.id_apply] + induction x using TensorProduct.induction_on with + | zero => simp + | tmul b v => + simp only [smul_tmul', smul_eq_mul, LinearMap.lTensor_tmul] + | add => aesop } + +variable {k V W} in +@[simp] +lemma _root_.LinearMap.extendScalars_apply (f : V →ₗ[k] W) (a : K) (v : V) : + LinearMap.extendScalars K f (a ⊗ₜ v) = a ⊗ₜ f v := by + simp only [LinearMap.extendScalars, LinearMap.coe_mk, LinearMap.coe_toAddHom, + LinearMap.lTensor_tmul] + +@[simp] +lemma _root_.LinearMap.extendScalars_id : + LinearMap.extendScalars K (LinearMap.id : V →ₗ[k] V) = LinearMap.id := by + ext + simp + +lemma _root_.LinearMap.extendScalars_comp (f : V →ₗ[k] W) (g : W →ₗ[k] W') : + (g ∘ₗ f).extendScalars K = g.extendScalars K ∘ₗ f.extendScalars K := by + ext v + simp + +variable {k K V W} in +def _root_.LinearMap.galAct (σ : K ≃ₐ[k] K) (f : K ⊗[k] V →ₗ[K] K ⊗[k] W) : + K ⊗[k] V →ₗ[K] K ⊗[k] W where + toFun := LinearMap.rTensor W σ.toLinearMap ∘ f ∘ LinearMap.rTensor V σ.symm.toLinearMap + map_add' := by aesop + map_smul' a x := by + simp only [Function.comp_apply, RingHom.id_apply] + induction x using TensorProduct.induction_on with + | zero => simp + | tmul b x => + simp only [smul_tmul', smul_eq_mul, LinearMap.rTensor_tmul, AlgEquiv.toLinearMap_apply, + _root_.map_mul] + rw [show (σ.symm a * σ.symm b) ⊗ₜ[k] x = σ.symm (a * b) • ((1 : K) ⊗ₜ x) by + simp [smul_tmul'], map_smul] + have mem : f (1 ⊗ₜ[k] x) ∈ (⊤ : Submodule k _):= ⟨⟩ + rw [← span_tmul_eq_top k K W, mem_span_set] at mem + obtain ⟨c, hc, (eq1 : (∑ i in c.support, _ • _) = _)⟩ := mem + choose xᵢ yᵢ hxy using hc + have eq1 : f (1 ⊗ₜ[k] x) = ∑ i in c.support.attach, (c i.1 • xᵢ i.2) ⊗ₜ[k] yᵢ i.2 := by + rw [← eq1, ← Finset.sum_attach] + refine Finset.sum_congr rfl fun i _ => ?_ + rw [← smul_tmul', hxy i.2] + rw [eq1, Finset.smul_sum, map_sum] + simp_rw [smul_tmul', LinearMap.rTensor_tmul, smul_eq_mul, AlgEquiv.toLinearMap_apply, + _root_.map_mul, AlgEquiv.apply_symm_apply] + rw [show σ.symm b ⊗ₜ[k] x = σ.symm b • (1 ⊗ₜ x) by simp [smul_tmul'], map_smul, eq1, + Finset.smul_sum, map_sum] + simp_rw [smul_tmul', LinearMap.rTensor_tmul, AlgEquiv.toLinearMap_apply, smul_eq_mul, + _root_.map_mul, AlgEquiv.apply_symm_apply] + rw [Finset.smul_sum] + simp_rw [smul_tmul', smul_eq_mul, mul_assoc] + | add => aesop + +lemma _root_.LinearMap.galAct_restrictScalars (σ : K ≃ₐ[k] K) (f : K ⊗[k] V →ₗ[K] K ⊗[k] W) : + (f.galAct σ).restrictScalars k = + σ.toLinearMap.rTensor W ∘ₗ f.restrictScalars k ∘ₗ σ.symm.toLinearMap.rTensor V := + rfl + +@[simp] +lemma _root_.LinearMap.galAct_extendScalars_apply + (σ : K ≃ₐ[k] K) (f : K ⊗[k] V →ₗ[K] K ⊗[k] W) (a : K) (v : V) : + LinearMap.galAct σ f (a ⊗ₜ v) = + LinearMap.rTensor W σ.toLinearMap (f $ σ.symm a ⊗ₜ v) := by + simp only [LinearMap.galAct, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, + LinearMap.rTensor_tmul, AlgEquiv.toLinearMap_apply] + +@[simp] +lemma _root_.LinearMap.galAct_extendScalars_apply' + (σ : K ≃ₐ[k] K) (f : V →ₗ[k] W) (a : K) (v : V) : + LinearMap.galAct σ (f.extendScalars K) (a ⊗ₜ v) = a ⊗ₜ f v := by + simp only [LinearMap.galAct, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, + LinearMap.rTensor_tmul, AlgEquiv.toLinearMap_apply, LinearMap.extendScalars_apply, + AlgEquiv.apply_symm_apply] + +lemma _root_.LinearMap.restrictScalars_comp + {k K : Type*} [Semiring k] [Semiring K] + {V W W' : Type*} [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid W'] + [Module k V] [Module k W] [Module k W'] + [Module K V] [Module K W] [Module K W'] + [LinearMap.CompatibleSMul V W k K] [LinearMap.CompatibleSMul W W' k K] + [LinearMap.CompatibleSMul V W' k K] + (f : V →ₗ[K] W) (g : W →ₗ[K] W') : + (LinearMap.restrictScalars k (g ∘ₗ f)) = + LinearMap.restrictScalars k g ∘ₗ LinearMap.restrictScalars k f := by + ext; rfl + +lemma _root_.LinearMap.galAct_comp + (σ : K ≃ₐ[k] K) (f : K ⊗[k] V →ₗ[K] K ⊗[k] W) (g : K ⊗[k] W →ₗ[K] K ⊗[k] W') : + (LinearMap.galAct σ (g ∘ₗ f)) = LinearMap.galAct σ g ∘ₗ LinearMap.galAct σ f := + LinearMap.restrictScalars_injective k $ by + simp only [LinearMap.galAct_restrictScalars, LinearMap.restrictScalars_comp, + LinearMap.comp_assoc] + conv_rhs => rw [← LinearMap.comp_assoc (f := f.restrictScalars k ∘ₗ _), + ← LinearMap.rTensor_comp, + show σ.symm.toLinearMap = σ.toLinearEquiv.symm.toLinearMap from rfl, + show σ.toLinearMap = σ.toLinearEquiv.toLinearMap from rfl, + show σ.toLinearEquiv.symm.toLinearMap ∘ₗ σ.toLinearEquiv.toLinearMap = LinearMap.id by aesop] + simp + +lemma _root_.LinearMap.galAct_id (σ : K ≃ₐ[k] K) : + (LinearMap.id : K ⊗[k] V →ₗ[K] K ⊗[k] V).galAct σ = LinearMap.id := + LinearMap.restrictScalars_injective k $ by + simp only [LinearMap.galAct_restrictScalars] + rw [show (LinearMap.id : K ⊗[k] V →ₗ[K] K ⊗[k] V).restrictScalars k = + LinearMap.id by ext; rfl] + simp only [LinearMap.id_comp] + rw [← LinearMap.rTensor_comp, + show σ.symm.toLinearMap = σ.toLinearEquiv.symm.toLinearMap from rfl, + show σ.toLinearMap = σ.toLinearEquiv.toLinearMap from rfl, + show σ.toLinearEquiv.toLinearMap ∘ₗ σ.toLinearEquiv.symm.toLinearMap = LinearMap.id by aesop, + LinearMap.rTensor_id] + +end diff --git a/BrauerGroup/LinearMap.lean.bak b/BrauerGroup/LinearMap.lean.bak new file mode 100644 index 0000000..485ab0a --- /dev/null +++ b/BrauerGroup/LinearMap.lean.bak @@ -0,0 +1,95 @@ +import Mathlib.RingTheory.TensorProduct.Basic +import Mathlib.LinearAlgebra.TensorPower + +suppress_compilation + +open TensorProduct + +section + +variable (k K V W W' : Type*) +variable {p q : ℕ} +variable [CommSemiring k] [Semiring K] [Algebra k K] +variable [AddCommMonoid V] [Module k V] +variable [AddCommMonoid W] [Module k W] +variable [AddCommMonoid W'] [Module k W'] + +variable {k V W} in +def _root_.LinearMap.extendScalars (f : V →ₗ[k] W) : K ⊗[k] V →ₗ[K] K ⊗[k] W := + { f.lTensor K with + map_smul' := fun a x => by + simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, RingHom.id_apply] + induction x using TensorProduct.induction_on with + | zero => simp + | tmul b v => + simp only [smul_tmul', smul_eq_mul, LinearMap.lTensor_tmul] + | add => aesop } + +variable {k V W} in +@[simp] +lemma _root_.LinearMap.extendScalars_apply (f : V →ₗ[k] W) (a : K) (v : V) : + LinearMap.extendScalars K f (a ⊗ₜ v) = a ⊗ₜ f v := by + simp only [LinearMap.extendScalars, LinearMap.coe_mk, LinearMap.coe_toAddHom, + LinearMap.lTensor_tmul] + +@[simp] +lemma _root_.LinearMap.extendScalars_id : + LinearMap.extendScalars K (LinearMap.id : V →ₗ[k] V) = LinearMap.id := by + ext + simp + +lemma _root_.LinearMap.extendScalars_comp (f : V →ₗ[k] W) (g : W →ₗ[k] W') : + (g ∘ₗ f).extendScalars K = g.extendScalars K ∘ₗ f.extendScalars K := by + ext v + simp + +variable {k K V W} in +def _root_.LinearMap.galAct (σ : K ≃ₐ[k] K) (f : K ⊗[k] V →ₗ[K] K ⊗[k] W) : + K ⊗[k] V →ₗ[K] K ⊗[k] W where + toFun := LinearMap.rTensor W σ.toLinearMap ∘ f ∘ LinearMap.rTensor V σ.symm.toLinearMap + map_add' := by aesop + map_smul' a x := by + simp only [Function.comp_apply, RingHom.id_apply] + induction x using TensorProduct.induction_on with + | zero => simp + | tmul b x => + simp only [smul_tmul', smul_eq_mul, LinearMap.rTensor_tmul, AlgEquiv.toLinearMap_apply, + _root_.map_mul] + rw [show (σ.symm a * σ.symm b) ⊗ₜ[k] x = σ.symm (a * b) • ((1 : K) ⊗ₜ x) by + simp [smul_tmul'], map_smul] + have mem : f (1 ⊗ₜ[k] x) ∈ (⊤ : Submodule k _):= ⟨⟩ + rw [← span_tmul_eq_top k K W, mem_span_set] at mem + obtain ⟨c, hc, (eq1 : (∑ i in c.support, _ • _) = _)⟩ := mem + choose xᵢ yᵢ hxy using hc + have eq1 : f (1 ⊗ₜ[k] x) = ∑ i in c.support.attach, (c i.1 • xᵢ i.2) ⊗ₜ[k] yᵢ i.2 := by + rw [← eq1, ← Finset.sum_attach] + refine Finset.sum_congr rfl fun i _ => ?_ + rw [← smul_tmul', hxy i.2] + rw [eq1, Finset.smul_sum, map_sum] + simp_rw [smul_tmul', LinearMap.rTensor_tmul, smul_eq_mul, AlgEquiv.toLinearMap_apply, + _root_.map_mul, AlgEquiv.apply_symm_apply] + rw [show σ.symm b ⊗ₜ[k] x = σ.symm b • (1 ⊗ₜ x) by simp [smul_tmul'], map_smul, eq1, + Finset.smul_sum, map_sum] + simp_rw [smul_tmul', LinearMap.rTensor_tmul, AlgEquiv.toLinearMap_apply, smul_eq_mul, + _root_.map_mul, AlgEquiv.apply_symm_apply] + rw [Finset.smul_sum] + simp_rw [smul_tmul', smul_eq_mul, mul_assoc] + | add => aesop + +@[simp] +lemma _root_.LinearMap.galAct_extendScalars_apply + (σ : K ≃ₐ[k] K) (f : K ⊗[k] V →ₗ[K] K ⊗[k] W) (a : K) (v : V) : + LinearMap.galAct σ f (a ⊗ₜ v) = + LinearMap.rTensor W σ.toLinearMap (f $ σ.symm a ⊗ₜ v) := by + simp only [LinearMap.galAct, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, + LinearMap.rTensor_tmul, AlgEquiv.toLinearMap_apply] + +@[simp] +lemma _root_.LinearMap.galAct_extendScalars_apply' + (σ : K ≃ₐ[k] K) (f : V →ₗ[k] W) (a : K) (v : V) : + LinearMap.galAct σ (f.extendScalars K) (a ⊗ₜ v) = a ⊗ₜ f v := by + simp only [LinearMap.galAct, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, + LinearMap.rTensor_tmul, AlgEquiv.toLinearMap_apply, LinearMap.extendScalars_apply, + AlgEquiv.apply_symm_apply] + +end diff --git a/BrauerGroup/PiTensorProduct.lean b/BrauerGroup/PiTensorProduct.lean index f24f877..1cf3026 100644 --- a/BrauerGroup/PiTensorProduct.lean +++ b/BrauerGroup/PiTensorProduct.lean @@ -1,16 +1,20 @@ import Mathlib.LinearAlgebra.PiTensorProduct +import BrauerGroup.LinearMap import BrauerGroup.Dual +import Mathlib.Data.Finset.Finsupp +import Mathlib.Data.Finsupp.Notation suppress_compilation open TensorProduct PiTensorProduct + +namespace PiTensorProduct + variable {ι : Type*} (k K : Type*) [CommSemiring k] [CommSemiring K] [Algebra k K] variable (V : ι → Type*) [Π i : ι, AddCommMonoid (V i)] [Π i : ι, Module k (V i)] variable (W : ι → Type*) [Π i : ι, AddCommMonoid (W i)] [Π i : ι, Module k (W i)] -namespace PiTensorProduct - def extendScalars : (⨂[k] i, V i) →ₗ[k] ⨂[K] i, (K ⊗[k] V i) := PiTensorProduct.lift { toFun := fun v => tprod _ fun i => 1 ⊗ₜ v i @@ -85,3 +89,604 @@ lemma span_simple_tensor_eq_top [Fintype ι] : | add => aesop end PiTensorProduct + +section PiTensorProduct.Basis + +variable (n k : Type*) [CommSemiring k] [Nontrivial k] [NoZeroDivisors k] +variable [Fintype n] [DecidableEq n] +variable (ι : n → Type*) +variable (V : n → Type*) [Π i, AddCommMonoid (V i)] [Π i, Module k (V i)] +variable (B : (i : n) → Basis (ι i) k (V i)) + +lemma prod_mul_tprod (x : n → k) (v : (i : n) → V i) : + (∏ i, x i) • tprod k v = tprod k fun i => x i • v i := by + exact Eq.symm (MultilinearMap.map_smul_univ (tprod k) x v) + +open Finsupp in +def finsuppPiTensorFinsupp : + (⨂[k] (i : n), ι i →₀ k) ≃ₗ[k] ((i : n) → ι i) →₀ k := + LinearEquiv.ofLinear + (PiTensorProduct.lift + { toFun := fun f => + { support := Fintype.piFinset fun i => (f i).support + toFun := fun x => ∏ i : n, f i (x i) + mem_support_toFun := fun x => by + simp only [Fintype.mem_piFinset, mem_support_iff, ne_eq] + rw [Finset.prod_eq_zero_iff] + simp only [Finset.mem_univ, true_and, not_exists] } + map_add' := by + intro _ f i a b + ext v + simp only [Finsupp.coe_mk, Finsupp.coe_add, Pi.add_apply] + calc ∏ j : n, (Function.update f i (a + b) j) (v j) + _ = ∏ j : n, if j = i then a (v i) + b (v i) else f j (v j) := by + refine Finset.prod_congr rfl fun j _ => ?_ + simp only [Function.update] + aesop + simp only [Finset.prod_ite, Finset.prod_const, Finset.filter_eq'] + rw [if_pos (by simp)] + simp only [Finset.card_singleton, pow_one, add_mul] + rw [calc ∏ j : n, (Function.update f i a j) (v j) + _ = ∏ j : n, if j = i then a (v i) else f j (v j) := by + refine Finset.prod_congr rfl fun j _ => ?_ + simp only [Function.update] + aesop, + calc ∏ j : n, (Function.update f i b j) (v j) + _ = ∏ j : n, if j = i then b (v i) else f j (v j) := by + refine Finset.prod_congr rfl fun j _ => ?_ + simp only [Function.update] + aesop] + simp only [Finset.prod_ite, Finset.prod_const, Finset.filter_eq'] + rw [if_pos (by simp)] + simp only [Finset.card_singleton, pow_one, add_mul] + map_smul' := by + intro _ f i a x + ext v + simp only [Finsupp.coe_mk, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul] + calc ∏ j : n, (Function.update f i (a • x) j) (v j) + _ = ∏ j : n, if j = i then a * x (v i) else f j (v j) := by + refine Finset.prod_congr rfl fun j _ => ?_ + simp only [Function.update] + aesop + simp only [Finset.prod_ite, Finset.prod_const, Finset.filter_eq'] + rw [if_pos (by simp)] + simp only [Finset.card_singleton, pow_one, mul_pow] + rw [calc ∏ j : n, (Function.update f i x j) (v j) + _ = ∏ j : n, if j = i then x (v i) else f j (v j) := by + refine Finset.prod_congr rfl fun j _ => ?_ + simp only [Function.update] + aesop] + simp only [Finset.prod_ite, Finset.prod_const, Finset.filter_eq'] + rw [if_pos (by simp)] + simp only [Finset.card_singleton, pow_one, mul_pow, mul_assoc] }) + (Finsupp.llift (⨂[k] (i : n), ι i →₀ k) k k ((i : n) → ι i) fun x => + tprod k $ fun i => fun₀ | x i => 1) + (by + ext v₁ v₂ + simp only [LinearMap.coe_comp, Function.comp_apply, lsingle_apply, llift_apply, lift_apply, + zero_smul, sum_single_index, one_smul, lift.tprod, MultilinearMap.coe_mk, coe_mk, + LinearMap.id_comp] + if h : v₁ = v₂ then subst h; aesop + else + rw [Finsupp.single_eq_of_ne h] + replace h := Function.funext_iff.not.1 h + push_neg at h + obtain ⟨j, hj⟩ := h + rw [Finset.prod_eq_zero (i := j) (hi := by simp)] + rwa [Finsupp.single_eq_of_ne]) + (by + ext x + simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, Function.comp_apply, + lift.tprod, MultilinearMap.coe_mk, llift_apply, lift_apply, LinearMap.id_coe, id_eq] + simp only [sum, coe_mk, Finset.sum_map, Function.Embedding.coeFn_mk] + change ∑ z ∈ _, (∏ i : n, _) • (⨂ₜ[k] _, _) = _ + have (z : (a : n) → ι a) : + (∏ i : n, (x i) (z i)) • + (tprod k fun j ↦ fun₀ | z j => (1 : k)) = + tprod k fun j ↦ fun₀ | z j => (x j) (z j) := by + rw [← (tprod k).map_smul_univ] + congr! with j + simp only [smul_single, smul_eq_mul, mul_one] + simp_rw [this] + rw [← (tprod k : MultilinearMap k _ (⨂[k] (i : n), ι i →₀ k)).map_sum_finset + (A := fun i ↦ (x i).support) (g := fun j z ↦ fun₀ | z => x j z)] + congr! with j + conv_rhs => rw [← Finsupp.sum_single (x j)] + rw [Finsupp.sum]) + +def piTensorBasis : Basis (Π i, ι i) k (⨂[k] i, V i) := + Finsupp.basisSingleOne.map $ + LinearEquiv.symm $ PiTensorProduct.congr (fun i => (B i).repr) ≪≫ₗ finsuppPiTensorFinsupp n k ι + +@[simp] +lemma piTensorBasis_apply (x : Π i, ι i) : + piTensorBasis n k ι V B x = tprod k fun i => (B i) (x i) := by + simp only [piTensorBasis, PiTensorProduct.congr, Basis.coe_repr_symm, finsuppPiTensorFinsupp, + LinearEquiv.trans_symm, Basis.map_apply, Finsupp.coe_basisSingleOne, LinearEquiv.trans_apply, + LinearEquiv.ofLinear_symm_apply, Finsupp.llift_apply, Finsupp.lift_apply, zero_smul, + Finsupp.sum_single_index, one_smul, map_tprod, Finsupp.total_single] + +end PiTensorProduct.Basis + +section extendScalars + +variable (k K V W W' : Type*) +variable {p q : ℕ} +variable [CommSemiring k] [Nontrivial k] [NoZeroDivisors k] +variable [CommSemiring K] [Nontrivial K] [NoZeroDivisors K] [Algebra k K] +variable [AddCommMonoid V] [Module k V] +variable [AddCommMonoid W] [Module k W] +variable [AddCommMonoid W'] [Module k W'] + +variable {k V} (p) in +def _root_.Basis.extendScalarsTensorPower {ι : Type*} (b : Basis ι k V) : + Basis (Fin p → ι) K (K ⊗[k] (⨂[k]^p V)) := +Algebra.TensorProduct.basis K (piTensorBasis _ _ _ _ (fun _ => b)) + +@[simp] +lemma _root_.Basis.extendScalarsTensorPower_apply {ι : Type*} (b : Basis ι k V) (i : Fin p → ι) : + Basis.extendScalarsTensorPower K p b i = 1 ⊗ₜ tprod k fun j => b (i j) := by + simp only [Basis.extendScalarsTensorPower, Algebra.TensorProduct.basis_apply, piTensorBasis_apply] + +variable {k V} (p) in +def _root_.Basis.tensorPowerExtendScalars {ι : Type*} (b : Basis ι k V) : + Basis (Fin p → ι) K (⨂[K]^p $ K ⊗[k] V) := + piTensorBasis _ _ _ _ fun _ => Algebra.TensorProduct.basis K b + +@[simp] +lemma _root_.Basis.tensorPowerExtendScalars_apply {ι : Type*} (b : Basis ι k V) (i : Fin p → ι) : + Basis.tensorPowerExtendScalars K p b i = tprod K fun j => 1 ⊗ₜ[k] b (i j) := by + simp only [Basis.tensorPowerExtendScalars, piTensorBasis_apply, Algebra.TensorProduct.basis_apply] + +variable {k V} (p) in +def _root_.Basis.extendScalarsTensorPowerEquiv {ι : Type*} (b : Basis ι k V) : + K ⊗[k] (⨂[k]^p V) ≃ₗ[K] (⨂[K]^p $ K ⊗[k] V) := + (b.extendScalarsTensorPower K p).equiv (b.tensorPowerExtendScalars K p) (Equiv.refl _) + +@[simp] +lemma _root_.Basis.extendScalarsTensorPowerEquiv_apply {ι : Type*} (b : Basis ι k V) + (i : Fin p → ι) : + b.extendScalarsTensorPowerEquiv K p (1 ⊗ₜ tprod k fun j => b (i j)) = + tprod K fun j => 1 ⊗ₜ[k] b (i j) := by + simp only [Basis.extendScalarsTensorPowerEquiv] + have := (b.extendScalarsTensorPower K p).equiv_apply (b' := b.tensorPowerExtendScalars K p) i + (Equiv.refl _) + simp only [Basis.extendScalarsTensorPower_apply, Equiv.refl_apply, + Basis.tensorPowerExtendScalars_apply] at this + exact this + +@[simp] +lemma _root_.Basis.extendScalarsTensorPowerEquiv_symm_apply {ι : Type*} (b : Basis ι k V) + (i : Fin p → ι) : + (b.extendScalarsTensorPowerEquiv K p).symm (tprod K fun j => 1 ⊗ₜ[k] b (i j)) = + 1 ⊗ₜ[k] tprod k fun j => b (i j) := by + simp only [Basis.extendScalarsTensorPowerEquiv, Basis.equiv_symm, Equiv.refl_symm] + have := (b.tensorPowerExtendScalars K p).equiv_apply (b' := b.extendScalarsTensorPower K p) i + (Equiv.refl _) + simp only [Basis.tensorPowerExtendScalars_apply, Equiv.refl_apply, + Basis.extendScalarsTensorPower_apply] at this + exact this + +@[simp] +lemma _root_.Basis.extendScalarsTensorPowerEquiv_apply' {ιV ιW : Type*} + (bV : Basis ιV k V) (bW : Basis ιW k W) + (iV : Fin p → ιV) (f : V →ₗ[k] W) : + bW.extendScalarsTensorPowerEquiv K p (1 ⊗ₜ tprod k fun j => f $ bV (iV j)) = + tprod K fun j => (1 : K) ⊗ₜ[k] (f $ bV (iV j)) := by + have eq (j : Fin p) := bW.total_repr (f $ bV (iV j)) + dsimp only [Finsupp.total, Finsupp.lsum, Finsupp.sum, LinearEquiv.coe_mk, LinearMap.coe_smulRight, + LinearMap.id_coe, id_eq, LinearMap.coe_mk, AddHom.coe_mk] at eq + have eq' : (tprod k fun j ↦ f (bV $ iV j)) = tprod k fun j => + ∑ a ∈ (bW.repr (f (bV $ iV j))).support, (bW.repr (f (bV (iV j)))) a • bW a := by + congr + simp_rw [eq] + rw [eq', MultilinearMap.map_sum_finset, tmul_sum, map_sum] + simp_rw [MultilinearMap.map_smul_univ (tprod k), tmul_smul] + have eq'' : ((tprod K) fun j ↦ (1 : K) ⊗ₜ[k] f (bV (iV j))) = tprod K fun j => + 1 ⊗ₜ ∑ a ∈ (bW.repr (f (bV $ iV j))).support, (bW.repr (f (bV (iV j)))) a • bW a := by + congr + simp_rw [eq] + rw [eq''] + simp_rw [tmul_sum] + rw [MultilinearMap.map_sum_finset] + refine Finset.sum_congr rfl fun x _ => ?_ + rw [algebra_compatible_smul K, map_smul, map_prod] + simp only [Basis.extendScalarsTensorPowerEquiv_apply, tmul_smul] + rw [← MultilinearMap.map_smul_univ (tprod K)] + congr 1 + ext i + simp + +@[simp] +lemma _root_.Basis.extendScalarsTensorPowerEquiv_symm_apply' {ιV ιW : Type*} + (bV : Basis ιV k V) (bW : Basis ιW k W) + (iV : Fin p → ιV) (f : V →ₗ[k] W) : + (bW.extendScalarsTensorPowerEquiv K p).symm (tprod K fun j => (1 : K) ⊗ₜ[k] (f $ bV (iV j))) = + (1 ⊗ₜ tprod k fun j => f $ bV (iV j)) := by + apply_fun (bW.extendScalarsTensorPowerEquiv K p) using + (bW.extendScalarsTensorPowerEquiv K p).injective + simp only [LinearEquiv.apply_symm_apply, Basis.extendScalarsTensorPowerEquiv_apply'] + +lemma _root_.Basis.extendScalarsTensorPowerEquiv_zero {ι : Type*} (b : Basis ι k V) : + b.extendScalarsTensorPowerEquiv K 0 = + ({ TensorProduct.congr (LinearEquiv.refl k K) (PiTensorProduct.isEmptyEquiv (ι := Fin 0) (s := fun _ => V)) with + map_smul' := fun a x => by + simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe, + RingHom.id_apply] + induction x using TensorProduct.induction_on with + | zero => simp + | tmul x y => simp [smul_tmul'] + | add x y hx hy => + simp only [smul_add, map_add, hx, hy, mul_add] } : (K ⊗[k] ⨂[k]^0 V) ≃ₗ[K] K ⊗[k] k) ≪≫ₗ + { TensorProduct.rid k K with + map_smul' := fun a x => by + simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe, + RingHom.id_apply, smul_eq_mul] + induction x using TensorProduct.induction_on with + | zero => simp + | tmul x y => simp [smul_tmul'] + | add x y hx hy => + simp only [smul_add, map_add, hx, hy, mul_add] } ≪≫ₗ + (PiTensorProduct.isEmptyEquiv _).symm := by + apply_fun LinearEquiv.toLinearMap using LinearEquiv.toLinearMap_injective + fapply Basis.ext (b := b.extendScalarsTensorPower K 0) + intro v + simp only [Basis.extendScalarsTensorPower_apply, LinearEquiv.coe_coe, + Basis.extendScalarsTensorPowerEquiv_apply, LinearEquiv.invFun_eq_symm, LinearEquiv.trans_apply, + isEmptyEquiv_symm_apply] + erw [LinearMap.coe_mk] + simp only [LinearMap.coe_toAddHom, LinearEquiv.coe_coe] + erw [TensorProduct.rid_tmul] + simp only [LinearEquiv.coe_coe, isEmptyEquiv_apply_tprod, LinearEquiv.refl_toLinearMap, + LinearMap.id_coe, id_eq, one_smul] + congr 1 + ext i + exact i.elim0 + +lemma _root_.Basis.extendScalarsTensorPowerEquiv_zero_apply {ι : Type*} (b : Basis ι k V) + (a : K) (x : ⨂[k]^0 V) : + b.extendScalarsTensorPowerEquiv K 0 (a ⊗ₜ x) = + (PiTensorProduct.isEmptyEquiv _).symm (PiTensorProduct.isEmptyEquiv _ x • a) := by + induction x using PiTensorProduct.induction_on with + | smul_tprod x v => + simp only [Basis.extendScalarsTensorPowerEquiv_zero, LinearEquiv.invFun_eq_symm, tmul_smul, + smul_tmul', LinearEquiv.trans_apply, isEmptyEquiv_symm_apply, map_smul, + isEmptyEquiv_apply_tprod, smul_eq_mul, mul_one, smul_assoc] + erw [LinearMap.coe_mk] + simp only [LinearMap.coe_toAddHom, LinearEquiv.coe_coe] + erw [TensorProduct.rid_tmul] + simp only [LinearEquiv.coe_coe, isEmptyEquiv_apply_tprod, LinearEquiv.refl_toLinearMap, + LinearMapClass.map_smul, LinearMap.id_coe, id_eq, one_smul, smul_assoc] + | add x y hx hy => + simp only [tmul_add, map_add, hx, isEmptyEquiv_symm_apply, smul_assoc, hy, add_smul] + +@[simp] +lemma _root_.Basis.extendScalarsTensorPowerEquiv_zero_symm_apply {ι : Type*} (b : Basis ι k V) + (a : K) : + (b.extendScalarsTensorPowerEquiv K 0).symm (a • tprod K isEmptyElim) = + a ⊗ₜ tprod k isEmptyElim := by + apply_fun b.extendScalarsTensorPowerEquiv K 0 using LinearEquiv.injective + (Basis.extendScalarsTensorPowerEquiv K 0 b) + simp only [LinearMapClass.map_smul, LinearEquiv.apply_symm_apply, + Basis.extendScalarsTensorPowerEquiv_zero_apply, isEmptyEquiv_apply_tprod, one_smul, + isEmptyEquiv_symm_apply] + +@[simp] +lemma _root_.Basis.extendScalarsTensorPowerEquiv_zero_symm_apply' {ι : Type*} (b : Basis ι k V) : + (b.extendScalarsTensorPowerEquiv K 0).symm (tprod K isEmptyElim) = + 1 ⊗ₜ tprod k isEmptyElim := by + apply_fun b.extendScalarsTensorPowerEquiv K 0 using LinearEquiv.injective + (Basis.extendScalarsTensorPowerEquiv K 0 b) + simp only [LinearMapClass.map_smul, LinearEquiv.apply_symm_apply, + Basis.extendScalarsTensorPowerEquiv_zero_apply, isEmptyEquiv_apply_tprod, one_smul, + isEmptyEquiv_symm_apply] + + +set_option maxHeartbeats 500000 in +lemma _root_.Basis.extendScalarsTensorPowerEquiv_comp_extendScalars + {ιV ιW : Type*} + (bV : Basis ιV k V) (bW : Basis ιW k W) + (f : V →ₗ[k] W) : + (bW.extendScalarsTensorPowerEquiv K p).toLinearMap ∘ₗ + (LinearMap.extendScalars K (PiTensorProduct.map fun _ => f)) = + (PiTensorProduct.map fun _ => f.extendScalars K) ∘ₗ + (bV.extendScalarsTensorPowerEquiv K p).toLinearMap := by + ext v + simp only [AlgebraTensorModule.curry_apply, LinearMap.compMultilinearMap_apply, curry_apply, + LinearMap.coe_restrictScalars, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, + LinearMap.extendScalars_apply, map_tprod] + have eq (j : Fin p) := bW.total_repr (f $ v j) + dsimp only [Finsupp.total, Finsupp.lsum, Finsupp.sum, LinearEquiv.coe_mk, LinearMap.coe_smulRight, + LinearMap.id_coe, id_eq, LinearMap.coe_mk, AddHom.coe_mk] at eq + have eq' : (tprod k fun j ↦ f (v j)) = tprod k fun j => + ∑ a ∈ (bW.repr (f (v j))).support, (bW.repr (f (v j))) a • bW a := by + congr + simp_rw [eq] + rw [eq'] + rw [MultilinearMap.map_sum_finset, tmul_sum, map_sum] + simp_rw [MultilinearMap.map_smul_univ (tprod k), tmul_smul] + rw [show ∑ x ∈ Fintype.piFinset fun j ↦ (bW.repr (f (v j))).support, + (Basis.extendScalarsTensorPowerEquiv K p bW) + ((∏ i : Fin p, (bW.repr (f (v i))) (x i)) • 1 ⊗ₜ[k] (tprod k) fun i ↦ bW (x i)) = + ∑ x ∈ Fintype.piFinset fun j ↦ (bW.repr (f (v j))).support, + (Basis.extendScalarsTensorPowerEquiv K p bW) + (algebraMap k K (∏ i : Fin p, (bW.repr (f (v i))) (x i)) • + 1 ⊗ₜ[k] (tprod k) fun i ↦ bW (x i)) from Finset.sum_congr rfl fun _ _ => by + rw [algebra_compatible_smul K, map_smul, map_prod]] + simp_rw [map_smul] + have eq''' (x : Fin p → ιW) : + Basis.extendScalarsTensorPowerEquiv K p bW (1 ⊗ₜ[k] (tprod k) fun i ↦ bW (x i)) = + tprod K fun i => 1 ⊗ₜ[k] bW (x i) := by + rw [Basis.extendScalarsTensorPowerEquiv_apply] + simp_rw [eq'''] + have eq₄ : (tprod k) v = + tprod k fun i => ∑ a ∈ (bV.repr (v i)).support, bV.repr (v i) a • bV a := by + congr + ext j + have := bV.total_repr (v j) + simpa [Eq.comm, Finsupp.total] using this + conv_rhs => rw [eq₄, MultilinearMap.map_sum_finset, tmul_sum, map_sum, map_sum] + simp_rw [MultilinearMap.map_smul_univ (tprod k), tmul_smul] + have eq₅ (x : Fin p → ιV) : + Basis.extendScalarsTensorPowerEquiv K p bV + ((∏ i : Fin p, (bV.repr (v i)) (x i)) • 1 ⊗ₜ[k] (tprod k) fun i ↦ bV (x i)) = + algebraMap k K (∏ i : Fin p, (bV.repr (v i)) (x i)) • tprod K fun i => 1 ⊗ₜ[k] bV (x i) := by + rw [algebra_compatible_smul K, map_smul, Basis.extendScalarsTensorPowerEquiv_apply] + simp_rw [eq₅, map_smul, PiTensorProduct.map_tprod] + simp only [LinearMap.extendScalars_apply, algebraMap_smul] + have eq₆ (x : Fin p → ιW) : + (∏ i : Fin p, (bW.repr (f (v i))) (x i)) • ((tprod K) fun i ↦ (1 : K) ⊗ₜ[k] bW (x i)) = + tprod K fun i => (1 : K) ⊗ₜ[k] ((bW.repr (f (v i))) (x i) • bW (x i)) := by + rw [algebra_compatible_smul K, map_prod, ← (tprod K).map_smul_univ] + congr + ext j + simp + simp_rw [eq₆] + have eq₇ (x : Fin p → ιV) : + (∏ i : Fin p, (bV.repr (v i)) (x i)) • ((tprod K) fun i ↦ (1 : K) ⊗ₜ[k] f (bV (x i))) = + tprod K fun i => 1 ⊗ₜ[k] ((bV.repr (v i)) (x i) • f (bV (x i))):= by + rw [algebra_compatible_smul K, map_prod, ← (tprod K).map_smul_univ] + congr + ext j + simp + simp_rw [eq₇] + have eq₈ : (tprod K fun j ↦ (1 : K) ⊗ₜ[k] f (v j)) = tprod K fun j => + ∑ a ∈ (bW.repr (f (v j))).support, 1 ⊗ₜ ((bW.repr (f (v j))) a • bW a) := by + simp_rw [← tmul_sum] + congr + ext j + simp_rw [eq] + rw [MultilinearMap.map_sum_finset] at eq₈ + rw [← eq₈] + have eq₉ : (tprod K fun j ↦ (1 : K) ⊗ₜ[k] f (v j)) = tprod K fun j => + ∑ a ∈ (bV.repr (v j)).support, 1 ⊗ₜ (bV.repr (v j) a • f (bV a)) := by + simp_rw [← tmul_sum] + congr + ext j + have := bV.total_repr (v j) + conv_lhs => erw [← this] + erw [map_sum] + congr + ext i + simp + rw [MultilinearMap.map_sum_finset] at eq₉ + rw [← eq₉] + +end extendScalars + +section + + +lemma PiTensorProduct.isEmptyEquiv_comp_algebraMap + {k K : Type*} [CommSemiring k] [CommSemiring K] [Algebra k K] (ι : Type*) [emp : IsEmpty ι] + (V : ι → Type*) [∀ i, AddCommMonoid (V i)] [∀ i, Module k (V i)] : + (Algebra.ofId k K).toLinearMap ∘ₗ + (PiTensorProduct.isEmptyEquiv ι : (⨂[k] i : ι, V i) ≃ₗ[k] k).toLinearMap = + (PiTensorProduct.isEmptyEquiv ι : + (⨂[K] i : ι, K ⊗[k] V i) ≃ₗ[K] K).toLinearMap.restrictScalars k ∘ₗ + PiTensorProduct.lift + { toFun := fun v => tprod K fun i => 1 ⊗ₜ v i + map_add' := fun v i => emp.elim i + map_smul' := fun v i => emp.elim i } := by + ext x + simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply, isEmptyEquiv_apply_tprod, AlgHom.toLinearMap_apply, _root_.map_one, + LinearMap.coe_restrictScalars, lift.tprod, MultilinearMap.coe_mk] + +lemma PiTensorProduct.isEmptyEquiv_comp_algebraMap_elementwise + {k K : Type*} [CommSemiring k] [CommSemiring K] [Algebra k K] (ι : Type*) [emp : IsEmpty ι] + (V : ι → Type*) [∀ i, AddCommMonoid (V i)] [∀ i, Module k (V i)] : + algebraMap k K (PiTensorProduct.isEmptyEquiv ι + (tprod k isEmptyElim : ⨂[k] i : ι, V i)) = 1 := by + have := congr($(PiTensorProduct.isEmptyEquiv_comp_algebraMap ι V (k := k) (K := K)) + (tprod k isEmptyElim)) + dsimp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, + AlgHom.toLinearMap_apply, LinearMap.coe_restrictScalars] at this + erw [this] + simp + +end + +section gal +variable {ι k K V : Type*} +variable {q : ℕ} +variable [CommSemiring k] [Nontrivial k] [NoZeroDivisors k] +variable [CommSemiring K] [Nontrivial K] [NoZeroDivisors K] [Algebra k K] +variable [AddCommMonoid V] [Module k V] (b : Basis ι k V) + +variable (q) in +def _root_.AlgHom.oneTMulPow (σ : K →ₐ[k] K) : + (⨂[K]^q (K ⊗[k] V)) →ₗ[k] ⨂[K]^q (K ⊗[k] V) := + (Basis.extendScalarsTensorPowerEquiv K q b).toLinearMap.restrictScalars k ∘ₗ + σ.toLinearMap.rTensor _ ∘ₗ + (Basis.extendScalarsTensorPowerEquiv K q b).symm.toLinearMap.restrictScalars k + +@[simp] +lemma _root_.AlgHom.oneTMulPow_apply (σ : K →ₐ[k] K) (a : Fin q → K) (v : Fin q → ι) : + σ.oneTMulPow q b (tprod K fun i => a i ⊗ₜ b (v i)) = + (∏ i : Fin q, σ (a i)) • tprod K fun i => 1 ⊗ₜ b (v i) := by + simp only [AlgHom.oneTMulPow, LinearMap.coe_comp, LinearMap.coe_restrictScalars, + LinearEquiv.coe_coe, Function.comp_apply] + rw [show (tprod K fun i => a i ⊗ₜ b (v i)) = + (tprod K fun i => a i • 1 ⊗ₜ b (v i)) by simp_rw [smul_tmul', smul_eq_mul, mul_one], + MultilinearMap.map_smul_univ, map_smul] + simp only [Basis.extendScalarsTensorPowerEquiv_symm_apply] + rw [smul_tmul', smul_eq_mul, mul_one, LinearMap.rTensor_tmul, + show (σ.toLinearMap (∏ i : Fin q, a i) ⊗ₜ[k] (tprod k) fun j ↦ b (v j)) = + (σ.toLinearMap (∏ i : Fin q, a i) • 1 ⊗ₜ[k] (tprod k) fun j ↦ b (v j)) by + rw [smul_tmul', smul_eq_mul, mul_one], map_smul] + simp + +lemma _root_.AlgHom.oneTMulPow_apply_q_zero (σ : K →ₐ[k] K) : + σ.oneTMulPow 0 b = + (PiTensorProduct.isEmptyEquiv _).symm.toLinearMap.restrictScalars k ∘ₗ + σ.toLinearMap ∘ₗ + (PiTensorProduct.isEmptyEquiv _).toLinearMap.restrictScalars k := by + ext x + simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, + Function.comp_apply, AlgHom.toLinearMap_apply, isEmptyEquiv_symm_apply] + have mem : x ∈ (⊤ : Submodule K _) := ⟨⟩ + rw [← PiTensorProduct.span_tprod_eq_top, mem_span_set] at mem + obtain ⟨a, ha, rfl⟩ := mem + choose x hx using ha + simp only [Finsupp.sum, map_sum, LinearMapClass.map_smul, smul_eq_mul, _root_.map_mul] + rw [Finset.sum_smul] + refine Finset.sum_congr rfl fun z hz => ?_ + specialize hx hz + have hz' : z = tprod K isEmptyElim := by + rw [← hx]; congr; ext i; simpa using i.2 + rw [hz'] + simp only [isEmptyEquiv_apply_tprod, _root_.map_one, mul_one] + simp only [AlgHom.oneTMulPow, LinearMap.coe_comp, LinearMap.coe_restrictScalars, + LinearEquiv.coe_coe, Function.comp_apply, LinearMapClass.map_smul] + have eq : ((tprod K) isEmptyElim : ⨂[K] (_ : Fin 0), K ⊗[k] V) = + tprod K fun a => 1 ⊗ₜ b a.elim0 := by + congr; ext i; exact i.elim0 + rw [eq] + simp only [Basis.extendScalarsTensorPowerEquiv_symm_apply, smul_tmul', smul_eq_mul, mul_one, + LinearMap.rTensor_tmul, AlgHom.toLinearMap_apply] + rw [show (σ (a ((tprod K) fun a ↦ 1 ⊗ₜ[k] b a.elim0)) ⊗ₜ[k] + (tprod k) fun j : Fin 0 ↦ b j.elim0) = + σ (a ((tprod K) fun a ↦ 1 ⊗ₜ[k] b a.elim0)) • ((1 : K) ⊗ₜ (tprod k) fun j ↦ b j.elim0) by + rw [smul_tmul', smul_eq_mul, mul_one], map_smul] + simp + +@[simp] +lemma _root_.AlgHom.oneTMulPow_apply'_aux1 (σ : K →ₐ[k] K) (a : K) (v : Fin q → ι) [NeZero q] : + σ.oneTMulPow q b (a • tprod K fun i => 1 ⊗ₜ b (v i)) = + σ a • tprod K fun i => 1 ⊗ₜ b (v i) := by + rw [show (a • tprod K fun i => (1 : K) ⊗ₜ b (v i)) = + (∏ i : Fin q, if i = 0 then a else 1) • tprod K fun i => 1 ⊗ₜ b (v i) by simp, + ← MultilinearMap.map_smul_univ] + simp_rw [smul_tmul'] + rw [AlgHom.oneTMulPow_apply] + simp only [smul_eq_mul, mul_one] + congr + rw [show ∏ x : Fin q, σ (if x = 0 then a else 1) = ∏ x : Fin q, if x = 0 then σ a else 1 from + Finset.prod_congr rfl fun i _ => by split_ifs <;> simp] + simp + +@[simp] +lemma _root_.AlgHom.oneTMulPow_apply'_aux2 (σ : K →ₐ[k] K) (a : K) (v : Fin 0 → ι) : + σ.oneTMulPow 0 b (a • tprod K fun i => 1 ⊗ₜ b (v i)) = + σ a • tprod K fun i => 1 ⊗ₜ b (v i) := by + rw [AlgHom.oneTMulPow_apply_q_zero] + simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, + Function.comp_apply, LinearMapClass.map_smul, isEmptyEquiv_apply_tprod, smul_eq_mul, mul_one, + AlgHom.toLinearMap_apply, isEmptyEquiv_symm_apply] + congr + ext i + exact i.elim0 + +@[simp] +lemma _root_.AlgHom.oneTMulPow_apply' (σ : K →ₐ[k] K) (a : K) (v : Fin q → ι) : + σ.oneTMulPow q b (a • tprod K fun i => 1 ⊗ₜ b (v i)) = + σ a • tprod K fun i => 1 ⊗ₜ b (v i) := by + by_cases h : q = 0 + · subst h + apply AlgHom.oneTMulPow_apply'_aux2 + · haveI : NeZero q := ⟨h⟩ + apply AlgHom.oneTMulPow_apply'_aux1 + +@[simp] +lemma _root_.AlgHom.oneTMulPow_apply''_aux1 [NeZero q] (σ : K →ₐ[k] K) (a : K) + (x : Fin q → K) (v : Fin q → ι) : + σ.oneTMulPow q b (a • tprod K fun i => x i ⊗ₜ b (v i)) = + σ a • (∏ y : Fin q, σ (x y)) • tprod K fun i => 1 ⊗ₜ b (v i) := by + rw [show (a • tprod K fun i => x i ⊗ₜ b (v i)) = + (∏ i : Fin q, if i = 0 then a else 1) • tprod K fun i => x i ⊗ₜ b (v i) by simp, + ← MultilinearMap.map_smul_univ] + simp_rw [smul_tmul'] + rw [AlgHom.oneTMulPow_apply] + simp only [smul_eq_mul, ite_mul, one_mul] + rw [← smul_assoc] + congr 1 + change ∏ y : _, _ = _ + rw [show (∏ y : Fin q, σ (if y = 0 then a * x y else x y)) = + ∏ y : Fin q, if y = 0 then (σ a) * (σ $ x y) else σ (x y) from + Finset.prod_congr rfl fun i _ => by split_ifs <;> simp] + conv_rhs => rw [show σ a = ∏ i : Fin q, if i = 0 then σ a else 1 by simp, smul_eq_mul] + rw [← Finset.prod_mul_distrib] + refine Finset.prod_congr rfl fun i _ => ?_; split_ifs <;> simp + +lemma _root_.AlgHom.oneTMulPow_apply''_aux2 (σ : K →ₐ[k] K) (a : K) + (x : Fin 0 → K) (v : Fin 0 → ι) : + σ.oneTMulPow 0 b (a • tprod K fun i => x i ⊗ₜ b (v i)) = + σ a • (∏ y : Fin 0, σ (x y)) • tprod K fun i => 1 ⊗ₜ b (v i) := by + simp only [Finset.univ_eq_empty, Finset.prod_empty, one_smul] + rw [AlgHom.oneTMulPow_apply_q_zero] + simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, + Function.comp_apply, LinearMapClass.map_smul, isEmptyEquiv_apply_tprod, smul_eq_mul, mul_one, + AlgHom.toLinearMap_apply, isEmptyEquiv_symm_apply] + congr + ext i + exact i.elim0 + +lemma _root_.AlgHom.oneTMulPow_apply'' (σ : K →ₐ[k] K) (a : K) + (x : Fin q → K) (v : Fin q → ι) : + σ.oneTMulPow q b (a • tprod K fun i => x i ⊗ₜ b (v i)) = + σ a • (∏ y : Fin q, σ (x y)) • tprod K fun i => 1 ⊗ₜ b (v i) := by + by_cases h : q = 0 + · subst h + apply AlgHom.oneTMulPow_apply''_aux2 + · haveI : NeZero q := ⟨h⟩ + apply AlgHom.oneTMulPow_apply''_aux1 + +end gal + +section PiTensorProduct.fin + +variable {k K : Type*} [CommSemiring k] [Semiring K] [Algebra k K] + +variable (k) in +def PiTensorProduct.emptyEquivBaseRing (ι : Type*) (V : ι → Type*) [hι: IsEmpty ι] + [∀ i, AddCommGroup $ V i] [∀ i, Module k $ V i]: (⨂[k] i : ι, V i) ≃ₗ[k] k := + LinearEquiv.ofLinear + (PiTensorProduct.lift + { toFun := fun _ ↦ 1 + map_add' := by + intros; exact hι.elim (by assumption) + map_smul' := by + intros; exact hι.elim (by assumption) }) + { toFun := fun a ↦ a • tprod k fun x ↦ hι.elim x + map_add' := by + intro x y + simp only [self_eq_add_right, add_smul] + map_smul' := by + intro m x + simp [mul_smul] + } + (by + refine LinearMap.ext_ring ?h + simp only [LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, one_smul, + lift.tprod, MultilinearMap.coe_mk, LinearMap.id_coe, id_eq]) + (by + ext x + simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearMap.coe_mk, + AddHom.coe_mk, Function.comp_apply, lift.tprod, MultilinearMap.coe_mk, one_smul, + LinearMap.id_coe, id_eq] + refine MultilinearMap.congr_arg (tprod k) ?_ + ext y + exact hι.elim y) + +end PiTensorProduct.fin diff --git a/BrauerGroup/TensorOfTypePQ/Basic.lean b/BrauerGroup/TensorOfTypePQ/Basic.lean index 095919a..2855bb6 100644 --- a/BrauerGroup/TensorOfTypePQ/Basic.lean +++ b/BrauerGroup/TensorOfTypePQ/Basic.lean @@ -1,6 +1,7 @@ import Mathlib.LinearAlgebra.TensorPower import BrauerGroup.Dual import BrauerGroup.PiTensorProduct +import BrauerGroup.LinearMap suppress_compilation @@ -8,674 +9,160 @@ suppress_compilation open TensorProduct PiTensorProduct abbrev TensorOfType (k V : Type*) [CommSemiring k] [AddCommMonoid V] [Module k V] (p q : ℕ) := - (⨂[k]^p V) ⊗[k] (⨂[k]^q $ Module.Dual k V) + (⨂[k]^q V) →ₗ[k] (⨂[k]^p V) namespace TensorOfType -section basic - -variable {k K V W V₁ V₂ V₃} {p q : ℕ} +section extendScalars -variable [CommSemiring k] [CommSemiring K] [Algebra k K] +variable (k K V W W' : Type*) +variable {p q : ℕ} +variable [CommSemiring k] [Nontrivial k] [NoZeroDivisors k] +variable [CommSemiring K] [Nontrivial K] [NoZeroDivisors K] [Algebra k K] variable [AddCommMonoid V] [Module k V] -variable [AddCommMonoid V₁] [Module k V₁] -variable [AddCommMonoid V₂] [Module k V₂] -variable [AddCommMonoid V₃] [Module k V₃] variable [AddCommMonoid W] [Module k W] - -@[elab_as_elim] -lemma induction_on (x : TensorOfType k V p q) - {motive : TensorOfType k V p q → Prop} - (zero : motive 0) - (tprod_tmul_tprod : ∀ (v : Fin p → V) (f : Fin q → Module.Dual k V), - motive (tprod k v ⊗ₜ tprod k f)) - (smul : ∀ (a : k) (x : TensorOfType k V p q), motive x → motive (a • x)) - (add : ∀ (x y : TensorOfType k V p q), motive x → motive y → motive (x + y)) : motive x := by - induction x using TensorProduct.induction_on with - | zero => assumption - | tmul v f => - induction v using PiTensorProduct.induction_on with - | smul_tprod a v => - induction f using PiTensorProduct.induction_on with - | smul_tprod b f => - rw [← smul_tmul, ← mul_smul, ← smul_tmul'] - exact smul _ _ (tprod_tmul_tprod _ _) - | add => rw [tmul_add]; aesop - | add => rw [add_tmul]; aesop - | add x y hx hy => exact add x y hx hy - +variable [AddCommMonoid W'] [Module k W'] + +variable {k V} in +def extendScalarsLinearMapToFun {ι : Type*} (b : Basis ι k V) (f : TensorOfType k V p q) : + TensorOfType K (K ⊗[k] V) p q := + (b.extendScalarsTensorPowerEquiv K p).toLinearMap ∘ₗ f.extendScalars K ∘ₗ + (b.extendScalarsTensorPowerEquiv K q).symm.toLinearMap + +lemma extendScalarsLinearMapToFun_apply_tmul + {ι : Type*} (b : Basis ι k V) (f : TensorOfType k V p q) + (a : Fin q → K) (v : Fin q → ι) : + extendScalarsLinearMapToFun K b f (tprod K fun i => a i ⊗ₜ b (v i)) = + (b.extendScalarsTensorPowerEquiv K p).toLinearMap + ((∏ i : Fin q, a i) ⊗ₜ f (tprod k fun i => b (v i))) := by + simp only [extendScalarsLinearMapToFun, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply, EmbeddingLike.apply_eq_iff_eq] + have eq₁ (i : Fin q) : a i ⊗ₜ[k] b (v i) = a i • (1 ⊗ₜ[k] b (v i)) := by simp [smul_tmul'] + simp_rw [eq₁] + rw [MultilinearMap.map_smul_univ, map_smul, map_smul] + simp only [Basis.extendScalarsTensorPowerEquiv_symm_apply, LinearMap.extendScalars_apply, + smul_tmul', smul_eq_mul, mul_one] + +lemma extendScalarsLinearMapToFun_apply_one_tmul + {ι : Type*} (b : Basis ι k V) (f : TensorOfType k V p q) + (v : Fin q → ι) : + extendScalarsLinearMapToFun K b f (tprod K fun i => 1 ⊗ₜ b (v i)) = + (b.extendScalarsTensorPowerEquiv K p).toLinearMap + (1 ⊗ₜ f (tprod k fun i => b (v i))) := by + have := extendScalarsLinearMapToFun_apply_tmul k K V b f (fun _ : Fin q => 1) v + simpa using this + + +variable {k V} in +lemma extendScalarsLinearMapToFun_add {ι : Type*} (b : Basis ι k V) (f g : TensorOfType k V p q) : + extendScalarsLinearMapToFun K b (f + g) = + extendScalarsLinearMapToFun K b f + extendScalarsLinearMapToFun K b g := by + simp only [extendScalarsLinearMapToFun, LinearMap.lTensor_add] + ext + simp only [LinearMap.extendScalars, LinearMap.lTensor_add, LinearMap.compMultilinearMap_apply, + LinearMap.coe_comp, LinearEquiv.coe_coe, LinearMap.coe_mk, LinearMap.coe_toAddHom, + Function.comp_apply, LinearMap.add_apply, map_add] + +variable {k V} in +lemma extendScalarsLinearMapToFun_smul {ι : Type*} (b : Basis ι k V) + (a : k) (f : TensorOfType k V p q) : + extendScalarsLinearMapToFun K b (a • f) = a • extendScalarsLinearMapToFun K b f := by + simp only [extendScalarsLinearMapToFun, LinearMap.lTensor_smul, RingHom.id_apply] + fapply Basis.ext (b := b.tensorPowerExtendScalars K q) + intro i + simp only [Basis.tensorPowerExtendScalars_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, + LinearMap.coe_mk, LinearMap.coe_toAddHom, Function.comp_apply, LinearMap.smul_apply, + Basis.extendScalarsTensorPowerEquiv, Basis.equiv_symm] + have := (b.tensorPowerExtendScalars K q).equiv_apply (b' := b.extendScalarsTensorPower K q) + (i := i) (Equiv.refl _) + simp only [Basis.tensorPowerExtendScalars_apply, Equiv.refl_apply, + Basis.extendScalarsTensorPower_apply] at this + erw [this] + simp only [LinearMap.extendScalars_apply, LinearMap.smul_apply, tmul_smul] + rw [algebra_compatible_smul K a, map_smul, algebraMap_smul] + +variable {k V} in @[simps] -noncomputable def toHomAux (v : ⨂[k]^p V) (f : ⨂[k]^q (Module.Dual k V)) : - ⨂[k]^q V →ₗ[k] ⨂[k]^p V where - toFun v' := dualTensorPower k V q f v' • v - map_add' v₁ v₂ := by simp only [map_add, add_smul] - map_smul' a v' := by simp only [LinearMapClass.map_smul, smul_eq_mul, mul_smul, RingHom.id_apply] - -noncomputable def toHom : TensorOfType k V p q →ₗ[k] ⨂[k]^q V →ₗ[k] ⨂[k]^p V := -TensorProduct.lift -{ toFun := fun v => - { toFun := fun f => toHomAux v f - map_add' := by - intros f₁ f₂ - ext v' - simp only [LinearMap.compMultilinearMap_apply, toHomAux_apply, map_add, LinearMap.add_apply, - add_smul] - map_smul' := by - intros a f - ext v' - simp only [LinearMap.compMultilinearMap_apply, toHomAux_apply, map_smul, LinearMap.smul_apply, - smul_eq_mul, mul_smul, RingHom.id_apply] } - map_add' := by - intros v₁ v₂ - ext f w - simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_mk, AddHom.coe_mk, toHomAux_apply, - dualTensorPower_tprod, smul_add, LinearMap.add_apply] - map_smul' := by - intros a v - ext f w - simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_mk, AddHom.coe_mk, toHomAux_apply, - dualTensorPower_tprod, RingHom.id_apply, LinearMap.smul_apply] - rw [smul_comm] } - -@[simp] -lemma toHom_tprod_tmul_tprod_apply - (v : Fin p → V) (f : Fin q → Module.Dual k V) (x : Fin q → V) : - toHom (tprod k v ⊗ₜ[k] tprod k f) (tprod k x) = - (∏ i : Fin q, f i (x i)) • tprod k v := by - simp only [toHom, lift.tmul, LinearMap.coe_mk, AddHom.coe_mk, toHomAux_apply, - dualTensorPower_tprod] - -noncomputable def inducedLinearMap (e : V ≃ₗ[k] W) : TensorOfType k V p q →ₗ[k] TensorOfType k W p q := - TensorProduct.map - (PiTensorProduct.map fun _ => e) - (PiTensorProduct.map fun _ => Module.Dual.transpose e.symm) - -def induced (v : TensorOfType k V p q) (e : V ≃ₗ[k] W) : TensorOfType k W p q := - inducedLinearMap e v - -@[simp] -lemma induced_zero (e : V ≃ₗ[k] W) : (0 : TensorOfType k V p q).induced e = 0 := - (inducedLinearMap e).map_zero - -@[simp] -lemma induced_smul (v : TensorOfType k V p q) (e : V ≃ₗ[k] W) (a : k) : - (a • v).induced e = a • v.induced e := - (inducedLinearMap e).map_smul a v - -lemma induced_add (v₁ v₂ : TensorOfType k V p q) (e : V ≃ₗ[k] W) : - (v₁ + v₂).induced e = v₁.induced e + v₂.induced e := - (inducedLinearMap e).map_add v₁ v₂ - -@[simp] -lemma inducedLinearMap_tprod_tmul_tprod - (e : V ≃ₗ[k] W) (v : Fin p → V) (f : Fin q → Module.Dual k V) : - inducedLinearMap e (tprod k v ⊗ₜ[k] tprod k f) = - tprod k (fun i => e (v i)) ⊗ₜ[k] tprod k (fun i => Module.Dual.transpose e.symm (f i)) := by - simp only [inducedLinearMap, map_tmul, map_tprod, LinearEquiv.coe_coe] - -@[simp] -lemma induced_tprod_tmul_tprod (v : Fin p → V) (f : Fin q → Module.Dual k V) (e : V ≃ₗ[k] W) : - induced (tprod k v ⊗ₜ[k] tprod k f : TensorOfType k V p q) e = - tprod k (fun i => e (v i)) ⊗ₜ[k] tprod k (fun i => Module.Dual.transpose e.symm (f i)) := - inducedLinearMap_tprod_tmul_tprod e v f - -@[simp] -lemma inducedLinearMap_refl : - inducedLinearMap (p := p) (q := q) (LinearEquiv.refl k V) = LinearMap.id := by - ext v f - simp only [inducedLinearMap, LinearEquiv.refl_toLinearMap, PiTensorProduct.map_id, Module.Dual.transpose, - LinearEquiv.refl_symm, LinearMap.compMultilinearMap_apply, AlgebraTensorModule.curry_apply, - curry_apply, LinearMap.coe_restrictScalars, map_tmul, LinearMap.id_coe, id_eq, map_tprod, - LinearMap.flip_apply] - congr 2 - -@[simp] lemma induced_refl (v : TensorOfType k V p q) : v.induced (LinearEquiv.refl k V) = v := - congr($inducedLinearMap_refl v) - -lemma inducedLinearMap_trans (e : V₁ ≃ₗ[k] V₂) (f : V₂ ≃ₗ[k] V₃) : - inducedLinearMap (p := p) (q := q) (e ≪≫ₗ f) = - inducedLinearMap (p := p) (q := q) f ∘ₗ inducedLinearMap (p := p) (q := q) e := by - ext v g - simp only [LinearMap.compMultilinearMap_apply, AlgebraTensorModule.curry_apply, curry_apply, - LinearMap.coe_restrictScalars, inducedLinearMap_tprod_tmul_tprod, LinearEquiv.trans_apply, - Module.Dual.transpose, LinearEquiv.trans_symm, LinearMap.flip_apply, LinearMap.coe_comp, - Function.comp_apply] - congr 2 - -lemma induced_trans (v : TensorOfType k V₁ p q) (e : V₁ ≃ₗ[k] V₂) (f : V₂ ≃ₗ[k] V₃) : - v.induced (e ≪≫ₗ f) = (v.induced e).induced f := - congr($(inducedLinearMap_trans e f) v) - -noncomputable def congr (e : V ≃ₗ[k] W) : TensorOfType k V p q ≃ₗ[k] TensorOfType k W p q := -LinearEquiv.ofLinear - (inducedLinearMap e) (inducedLinearMap e.symm) (by - ext w fw - simp only [LinearMap.compMultilinearMap_apply, AlgebraTensorModule.curry_apply, curry_apply, - LinearMap.coe_restrictScalars, LinearMap.coe_comp, Function.comp_apply, - inducedLinearMap_tprod_tmul_tprod, Module.Dual.transpose, LinearEquiv.symm_symm, LinearMap.flip_apply, - LinearEquiv.apply_symm_apply, LinearMap.id_coe, id_eq] - congr 2 - ext i x - simp only [LinearMap.llcomp_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply]) (by - ext w fw - simp only [LinearMap.compMultilinearMap_apply, AlgebraTensorModule.curry_apply, curry_apply, - LinearMap.coe_restrictScalars, LinearMap.coe_comp, Function.comp_apply, - inducedLinearMap_tprod_tmul_tprod, Module.Dual.transpose, LinearMap.flip_apply, - LinearEquiv.symm_apply_apply, LinearEquiv.symm_symm, LinearMap.id_coe, id_eq] - congr 2 - ext i x - simp only [LinearMap.llcomp_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply]) - -@[simp] -lemma congr_apply (e : V ≃ₗ[k] W) (v : TensorOfType k V p q) : - congr e v = inducedLinearMap e v := rfl - -@[simp] -lemma congr_symm_apply (e : V ≃ₗ[k] W) (w : TensorOfType k W p q) : - (congr e).symm w = inducedLinearMap e.symm w := rfl - -end basic - -section extendScalars - -variable (k K V W : Type*) -variable {p q : ℕ} -variable [CommRing k] [CommRing K] [Algebra k K] -variable [AddCommGroup V] [Module k V] - -def extendScalarsLinearMap : TensorOfType k V p q →ₗ[k] TensorOfType K (K ⊗[k] V) p q := - let f1 : (⨂[k]^p V) →ₗ[k] ⨂[K]^p (K ⊗[k] V) := PiTensorProduct.extendScalars k K _ - let f2 : (⨂[k]^q (Module.Dual k V)) →ₗ[k] ⨂[K]^q (Module.Dual K (K ⊗[k] V)) := - { PiTensorProduct.map fun _ => Module.Dual.extendScalars k K V with - map_smul' := fun k hk => by - simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.map_smul_of_tower, - RingHom.id_apply] } ∘ₗ - PiTensorProduct.extendScalars k K _ - TensorProduct.lift $ - { toFun := fun vp => - { toFun := fun fq => vp ⊗ₜ[K] f2 fq - map_add' := fun fq₁ fq₂ => by - simp only [map_add, tmul_add] - map_smul' := fun a fq => by - simp only [LinearMapClass.map_smul, tmul_smul, RingHom.id_apply] } - map_add' := fun vp₁ vp₂ => by - simp only - ext fq - simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_mk, AddHom.coe_mk, - LinearMap.add_apply, add_tmul] - map_smul' := fun a vp => by - simp only [RingHom.id_apply] - ext fq - simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_mk, AddHom.coe_mk, - LinearMap.smul_apply] - rw [smul_tmul'] } ∘ₗ f1 +def extendScalarsLinearMap {ι : Type*} (b : Basis ι k V) : + TensorOfType k V p q →ₗ[k] TensorOfType K (K ⊗[k] V) p q where + toFun f := extendScalarsLinearMapToFun K b f + map_add' := extendScalarsLinearMapToFun_add K b + map_smul' := extendScalarsLinearMapToFun_smul K b variable {k V} +variable{ι : Type*} (b : Basis ι k V) + def extendScalars (v : TensorOfType k V p q) : TensorOfType K (K ⊗[k] V) p q := - extendScalarsLinearMap k K V v + extendScalarsLinearMap K b v @[simp] -lemma extendScalars_zero : (0 : TensorOfType k V p q).extendScalars K = 0 := - (extendScalarsLinearMap k K V).map_zero +lemma extendScalars_zero : (0 : TensorOfType k V p q).extendScalars K b = 0 := + (extendScalarsLinearMap K b).map_zero lemma extendScalars_smul (v : TensorOfType k V p q) (a : k) : - (a • v).extendScalars K = a • v.extendScalars K := - (extendScalarsLinearMap k K V).map_smul a v + (a • v).extendScalars K b = a • v.extendScalars K b := + (extendScalarsLinearMap K b).map_smul a v lemma extendScalars_add (v₁ v₂ : TensorOfType k V p q) : - (v₁ + v₂).extendScalars K = v₁.extendScalars K + v₂.extendScalars K := - (extendScalarsLinearMap k K V).map_add v₁ v₂ - -@[simp] -lemma extendScalarsLinearMap_tprod_tmul_tprod (v : Fin p → V) (f : Fin q → Module.Dual k V) : - extendScalarsLinearMap k K V ((tprod k v) ⊗ₜ (tprod k f)) = - (tprod K ((1 : K) ⊗ₜ v ·)) ⊗ₜ - (tprod K $ fun i => Module.Dual.extendScalars k K V (1 ⊗ₜ f i)) := by - simp only [extendScalarsLinearMap, LinearMap.coe_comp, LinearMap.coe_mk, LinearMap.coe_toAddHom, - Function.comp_apply, lift.tmul, AddHom.coe_mk, extendScalars_tprod, map_tprod] - -@[simp] -lemma extendScalars_tprod_tmul_tprod (v : Fin p → V) (f : Fin q → Module.Dual k V) : - extendScalars K ((tprod k v) ⊗ₜ[k] (tprod k f) : TensorOfType k V p q) = - (tprod K ((1 : K) ⊗ₜ v ·)) ⊗ₜ - (tprod K $ fun i => Module.Dual.extendScalars k K V (1 ⊗ₜ f i)) := - extendScalarsLinearMap_tprod_tmul_tprod _ _ _ - -lemma extendScalarsLinearMap_tprod_tmul_tprod_toHom_apply - (v : Fin p → V) (f : Fin q → Module.Dual k V) (w : Fin q → V) : - toHom (extendScalarsLinearMap k K V ((tprod k v) ⊗ₜ (tprod k f))) (tprod K (1 ⊗ₜ w ·)) = - (∏ x : Fin q, (f x) (w x)) • (tprod K) (1 ⊗ₜ v ·) := by - simp only [extendScalarsLinearMap_tprod_tmul_tprod, toHom_tprod_tmul_tprod_apply, - Module.Dual.extendScalars_tmul_apply_tmul, mul_one] - simp_rw [← Algebra.algebraMap_eq_smul_one] - rw [← map_prod] - rw [algebraMap_smul] + (v₁ + v₂).extendScalars K b = v₁.extendScalars K b + v₂.extendScalars K b:= + (extendScalarsLinearMap K b).map_add v₁ v₂ + +lemma extendScalars_apply_tmul + {ι : Type*} (b : Basis ι k V) (f : TensorOfType k V p q) + (a : Fin q → K) (v : Fin q → ι) : + f.extendScalars K b (tprod K fun i => a i ⊗ₜ b (v i)) = + (b.extendScalarsTensorPowerEquiv K p).toLinearMap + ((∏ i : Fin q, a i) ⊗ₜ f (tprod k fun i => b (v i))) := by + apply extendScalarsLinearMapToFun_apply_tmul + +lemma extendScalars_apply_one_tmul + {ι : Type*} (b : Basis ι k V) (f : TensorOfType k V p q) + (v : Fin q → ι) : + f.extendScalars K b (tprod K fun i => 1 ⊗ₜ b (v i)) = + (b.extendScalarsTensorPowerEquiv K p).toLinearMap + (1 ⊗ₜ f (tprod k fun i => b (v i))) := by + apply extendScalarsLinearMapToFun_apply_one_tmul + +lemma extendScalarsTensorPowerEquiv_comp {ιV : Type*} (bV : Basis ιV k V) + (f : TensorOfType k V p q) : + ((Basis.extendScalarsTensorPowerEquiv K p bV).toLinearMap ∘ₗ LinearMap.extendScalars K f) = + ((f.extendScalars K bV) ∘ₗ (Basis.extendScalarsTensorPowerEquiv K q bV).toLinearMap) := by + fapply Basis.ext (b := Basis.extendScalarsTensorPower K q bV) + intro v + simp only [Basis.extendScalarsTensorPower_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply, LinearMap.extendScalars_apply, Basis.extendScalarsTensorPowerEquiv_apply] + set B := piTensorBasis (Fin p) k (fun _ => ιV) (fun _ => V) (fun _ => bV) with B_eq + have eq₁ := B.total_repr (f ((tprod k) fun j ↦ bV (v j))) + rw [← eq₁] + dsimp only [Finsupp.total, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, + Finsupp.sum] + rw [tmul_sum, map_sum] + set lhs := _; change lhs = _ + rw [show lhs = + ∑ x ∈ (B.repr (f ((tprod k) fun j ↦ bV (v j)))).support, + (B.repr (f ((tprod k) fun j ↦ bV (v j)))) x • (Basis.extendScalarsTensorPowerEquiv K p bV) + (1 ⊗ₜ[k] B x) by + refine Finset.sum_congr rfl fun x _ => ?_ + rw [tmul_smul, algebra_compatible_smul K, map_smul, algebraMap_smul]] + clear lhs + simp only [piTensorBasis_apply, Basis.extendScalarsTensorPowerEquiv_apply, B] + simp only [← B_eq] + rw [extendScalars_apply_one_tmul] + conv_rhs => rw [← eq₁] + dsimp only [Finsupp.total, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, + Finsupp.sum] + rw [tmul_sum, map_sum] + refine Finset.sum_congr rfl fun x _ => ?_ + simp only [piTensorBasis_apply, tmul_smul, LinearMap.map_smul_of_tower, LinearEquiv.coe_coe, + Basis.extendScalarsTensorPowerEquiv_apply, B] + +lemma extendScalarsTensorPowerEquiv_comp_elementwise {ιV : Type*} (bV : Basis ιV k V) + (f : TensorOfType k V p q) (x) : + (Basis.extendScalarsTensorPowerEquiv K p bV).toLinearMap (LinearMap.extendScalars K f x) = + (f.extendScalars K bV) (Basis.extendScalarsTensorPowerEquiv K q bV x) := by + rw [← LinearMap.comp_apply, extendScalarsTensorPowerEquiv_comp, LinearMap.comp_apply] + simp end extendScalars end TensorOfType - -structure VectorSpaceWithTensorOfType (k : Type*) (p q : ℕ) [CommRing k] where -(carrier : Type*) -[ab : AddCommGroup carrier] -[mod : Module k carrier] -(tensor : TensorOfType k carrier p q) - -namespace VectorSpaceWithTensorOfType - -section basic - -variable {p q : ℕ} -variable {k : Type*} [CommRing k] (V V₁ V₂ V₃ W : VectorSpaceWithTensorOfType k p q) - -instance : CoeSort (VectorSpaceWithTensorOfType k p q) Type* := ⟨carrier⟩ -instance : AddCommGroup V := V.ab -instance : Module k V := V.mod - -noncomputable def hom := TensorOfType.toHom V.tensor - - -structure Equiv extends V ≃ₗ[k] W where - map_tensor : V.tensor.induced toLinearEquiv = W.tensor - -instance : EquivLike (Equiv V W) V W where - coe e x := e.toLinearEquiv x - inv e x := e.toLinearEquiv.symm x - left_inv e x := by simp - right_inv e x := by simp - coe_injective' := by - rintro ⟨e, he⟩ ⟨f, hf⟩ h _ - simp only [DFunLike.coe_fn_eq, Equiv.mk.injEq] - simpa using h - -instance : LinearEquivClass (Equiv V W) k V W where - map_add e := e.toLinearEquiv.map_add - map_smulₛₗ e := e.toLinearEquiv.map_smul - -@[refl, simps toLinearEquiv] -def Equiv.refl : Equiv V V where - __ := LinearEquiv.refl k V - map_tensor := by - simp only [TensorOfType.induced_refl] - -@[simp] -lemma Equiv.refl_apply (v : V) : (Equiv.refl V) v = v := rfl - -variable {V W} -@[symm, simps toLinearEquiv] -def Equiv.symm (e : Equiv V W) : Equiv W V where - __ := e.toLinearEquiv.symm - map_tensor := by - simp only - rw [← congr(($e.map_tensor).induced e.toLinearEquiv.symm)] - rw [← TensorOfType.induced_trans] - simp only [LinearEquiv.self_trans_symm, TensorOfType.induced_refl] - -variable {V₁ V₂ V₃} in -@[trans, simps toLinearEquiv] -def Equiv.trans (e : Equiv V₁ V₂) (f : Equiv V₂ V₃) : Equiv V₁ V₃ where - __ := (e.toLinearEquiv.trans f.toLinearEquiv) - map_tensor := by - simp only [TensorOfType.induced_trans, e.map_tensor, f.map_tensor] - -lemma Equiv.trans_apply (e : Equiv V₁ V₂) (f : Equiv V₂ V₃) (v : V₁) : - (e.trans f) v = f (e v) := by rfl - -end basic - -section extendScalars - -variable {p q : ℕ} -variable {k : Type*} (K : Type*) -variable [CommRing k] [CommRing K] [Algebra k K] - -@[simps tensor] -def extendScalars (V : VectorSpaceWithTensorOfType k p q) : - VectorSpaceWithTensorOfType K p q where - carrier := K ⊗[k] V - ab := inferInstance - mod := inferInstance - tensor := V.tensor.extendScalars K - -instance (V : VectorSpaceWithTensorOfType k p q) : Module k (V.extendScalars K) := - inferInstanceAs $ Module k (K ⊗[k] V) - -instance (V : VectorSpaceWithTensorOfType k p q) : IsScalarTower k K (V.extendScalars K) where - smul_assoc a b x := by - simp only [algebra_compatible_smul K, smul_eq_mul, Algebra.id.map_eq_id, _root_.map_mul, - RingHomCompTriple.comp_apply, RingHom.id_apply, mul_smul] - simp only [Algebra.id.map_eq_id, RingHomCompTriple.comp_apply, smul_eq_mul, _root_.map_mul, - RingHom.id_apply, mul_smul] - induction x using TensorProduct.induction_on - · simp - · rw [smul_tmul', smul_tmul', smul_tmul'] - congr - simp only [smul_eq_mul] - rw [algebra_compatible_smul K, smul_eq_mul] - · aesop - -def Equiv.extendScalarsAux {V W : VectorSpaceWithTensorOfType k p q} (e : Equiv V W) : - (V.extendScalars K) ≃ₗ[K] (W.extendScalars K) := - LinearEquiv.ofLinear - { LinearMap.lTensor K e.toLinearEquiv.toLinearMap with - map_smul' := fun a x => - show LinearMap.lTensor K e.toLinearEquiv.toLinearMap _ = - a • LinearMap.lTensor K e.toLinearEquiv.toLinearMap _ by - induction x using TensorProduct.induction_on with - | zero => - simp only [smul_zero, map_zero] - | tmul x y => - rw [smul_tmul'] - simp only [smul_eq_mul, LinearMap.lTensor_tmul, LinearEquiv.coe_coe, smul_tmul'] - | add x y hx hy => - rw [smul_add, map_add, hx, hy, map_add, smul_add] - } - { LinearMap.lTensor K e.symm.toLinearEquiv.toLinearMap with - map_smul' := fun a x => - show LinearMap.lTensor K e.symm.toLinearEquiv.toLinearMap _ = - a • LinearMap.lTensor K e.symm.toLinearEquiv.toLinearMap _ by - induction x using TensorProduct.induction_on with - | zero => - simp only [smul_zero, map_zero] - | tmul x y => - rw [smul_tmul'] - simp only [smul_eq_mul, LinearMap.lTensor_tmul, LinearEquiv.coe_coe, smul_tmul'] - | add x y hx hy => - rw [smul_add, map_add, hx, hy, map_add, smul_add] } - (by - ext x - change (LinearMap.lTensor _ _) (LinearMap.lTensor _ _ _) = _ - rw [← LinearMap.comp_apply, ← LinearMap.lTensor_comp] - simp only [symm_toLinearEquiv, LinearEquiv.comp_coe, LinearEquiv.symm_trans_self, - LinearEquiv.refl_toLinearMap, LinearMap.lTensor_id, LinearMap.id_coe, id_eq]) - (by - ext x - change (LinearMap.lTensor _ _) (LinearMap.lTensor _ _ _) = _ - rw [← LinearMap.comp_apply, ← LinearMap.lTensor_comp] - simp only [symm_toLinearEquiv, LinearEquiv.comp_coe, LinearEquiv.self_trans_symm, - LinearEquiv.refl_toLinearMap, LinearMap.lTensor_id, LinearMap.id_coe, id_eq]) - -@[simp] -lemma Equiv.extendScalarsAux_apply_tmul - {V W : VectorSpaceWithTensorOfType k p q} (e : Equiv V W) - (a : K) (v : V) : - e.extendScalarsAux K (a ⊗ₜ v) = a ⊗ₜ e v := by rfl - -@[simp] -lemma Equiv.extendScalarsAux_refl - (V : VectorSpaceWithTensorOfType k p q) : - (Equiv.refl V).extendScalarsAux K = Equiv.refl (V.extendScalars K) := by - ext x - induction x using TensorProduct.induction_on - · simp - · rfl - · aesop - -lemma Equiv.extendScalarsAux_symm - {V W : VectorSpaceWithTensorOfType k p q} (e : Equiv V W) : - e.symm.extendScalarsAux K = - (e.extendScalarsAux K).symm := by - ext x - induction x using TensorProduct.induction_on - · simp - · rfl - · aesop - -lemma Equiv.extendScalarsAux_trans - {V₁ V₂ V₃ : VectorSpaceWithTensorOfType k p q} (e : Equiv V₁ V₂) (f : Equiv V₂ V₃) : - (e.trans f).extendScalarsAux K = - (e.extendScalarsAux K).trans (f.extendScalarsAux K) := by - ext x - induction x using TensorProduct.induction_on - · simp - · rfl - · aesop - -lemma Equiv.extendScalarsAux_map_tensor_aux - {V W : VectorSpaceWithTensorOfType k p q} (e : Equiv V W) - (x : TensorOfType k V p q) : - (x.extendScalars K).induced (e.extendScalarsAux K) = - (x.induced e.toLinearEquiv).extendScalars K := by - induction x using TensorProduct.induction_on with - | zero => - simp only [TensorOfType.extendScalars_zero, TensorOfType.induced_zero] - | tmul v f => - induction v using PiTensorProduct.induction_on with - | smul_tprod a v => - induction f using PiTensorProduct.induction_on with - | smul_tprod b f => - simp only [tmul_smul, ← smul_tmul', TensorOfType.extendScalars_smul, - TensorOfType.induced_smul, TensorOfType.induced_tprod_tmul_tprod, ← mul_smul, - TensorOfType.extendScalars_tprod_tmul_tprod] - rw [algebra_compatible_smul (A := K), TensorOfType.induced_smul, - TensorOfType.induced_tprod_tmul_tprod, algebraMap_smul] - congr - ext i w - induction w using TensorProduct.induction_on with - | zero => simp only [map_zero] - | tmul a w => - simp only [Module.Dual.transpose, LinearMap.flip_apply, LinearMap.llcomp_apply, - LinearEquiv.coe_coe] - rw [← Equiv.extendScalarsAux_symm] - erw [extendScalarsAux_apply_tmul (e := e.symm) K a w] - simp only [Module.Dual.extendScalars_tmul_apply_tmul, one_mul, LinearMap.llcomp, - LinearMap.flip, LinearMap.mk₂'ₛₗ, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.lcomp, - LinearMap.id_coe, id_eq, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe] - erw [Module.Dual.extendScalars_tmul_apply_tmul] - simp only [LinearMap.coe_mk, AddHom.coe_mk, one_mul] - rfl - | add w₁ w₂ h₁ h₂ => - simp only [map_add, h₁, h₂] - | add x y hx hy => - simp only [tmul_add, TensorOfType.extendScalars_add, TensorOfType.induced_add, hx, hy] - | add x y hx hy => - simp only [add_tmul, TensorOfType.extendScalars_add, TensorOfType.induced_add, hx, hy] - | add x y hx hy => - simp only [TensorOfType.extendScalars_add, TensorOfType.induced_add, hx, hy] - -def Equiv.extendScalars {V W : VectorSpaceWithTensorOfType k p q} (e : Equiv V W) : - Equiv (V.extendScalars K) (W.extendScalars K) where - toLinearEquiv := e.extendScalarsAux K - map_tensor := by - simp only [symm_toLinearEquiv, extendScalars_tensor] - rw [extendScalarsAux_map_tensor_aux, e.map_tensor] - -lemma Equiv.extendScalars_apply_tmul - {V W : VectorSpaceWithTensorOfType k p q} (e : Equiv V W) (a : K) (v : V) : - e.extendScalars K (a ⊗ₜ v) = a ⊗ₜ e v := by rfl - -lemma Equiv.induced_extendScalars - {V W : VectorSpaceWithTensorOfType k p q} (e : Equiv V W) - (x : TensorOfType k V p q) : - (x.extendScalars K).induced (e.extendScalars K).toLinearEquiv = - (x.induced e.toLinearEquiv).extendScalars K := - Equiv.extendScalarsAux_map_tensor_aux _ _ _ - -lemma Equiv.extendScalars_refl - (V : VectorSpaceWithTensorOfType k p q) : - (Equiv.refl V).extendScalars K = Equiv.refl (V.extendScalars K) := - DFunLike.ext _ _ fun x => congr($(Equiv.extendScalarsAux_refl K V) x) - -lemma Equiv.extendScalars_symm - {V W : VectorSpaceWithTensorOfType k p q} (e : Equiv V W) : - e.symm.extendScalars K = (e.extendScalars K).symm := - DFunLike.ext _ _ fun x => congr($(Equiv.extendScalarsAux_symm K e) x) - -lemma Equiv.extendScalars_trans - {V₁ V₂ V₃ : VectorSpaceWithTensorOfType k p q} (e : Equiv V₁ V₂) (f : Equiv V₂ V₃) : - (e.trans f).extendScalars K = (e.extendScalars K).trans (f.extendScalars K) := - DFunLike.ext _ _ fun x => congr($(Equiv.extendScalarsAux_trans K e f) x) - -variable {K} in -def auxExtendAlgEquiv (V : VectorSpaceWithTensorOfType k p q) (σ : K ≃ₐ[k] K) : - V.extendScalars K ≃ₗ[k] V.extendScalars K := - LinearEquiv.ofLinear - (LinearMap.rTensor V σ.toLinearMap) - (LinearMap.rTensor V σ.symm.toLinearMap) - (by - apply TensorProduct.ext - ext a v - simp only [LinearMap.compr₂_apply, mk_apply, LinearMap.coe_comp, Function.comp_apply] - erw [LinearMap.rTensor_tmul] - aesop) - (by - apply TensorProduct.ext - ext a v - simp only [LinearMap.compr₂_apply, mk_apply, LinearMap.coe_comp, Function.comp_apply] - erw [LinearMap.rTensor_tmul] - aesop) - -@[simp] -lemma auxExtendAlgEquiv_tmul (V : VectorSpaceWithTensorOfType k p q) (σ : K ≃ₐ[k] K) - (a : K) (v : V) : - auxExtendAlgEquiv V σ (a ⊗ₜ v) = σ a ⊗ₜ v := rfl - -variable {K} in -def auxRestrict {V W : VectorSpaceWithTensorOfType k p q} - (f : Equiv (V.extendScalars K) (W.extendScalars K)) : - V.extendScalars K ≃ₗ[k] W.extendScalars K where - toFun := f - map_add' := f.map_add - map_smul' a x := by - simp only [RingHom.id_apply] - rw [algebra_compatible_smul K, map_smul, algebraMap_smul] - invFun := f.symm - left_inv := f.left_inv - right_inv := f.right_inv - -@[simp] -lemma auxRestrict_apply {V W : VectorSpaceWithTensorOfType k p q} - (f : Equiv (V.extendScalars K) (W.extendScalars K)) (x : V.extendScalars K) : - auxRestrict f x = f x := rfl - -variable {K} in -def Equiv.algEquivActAux - {V W : VectorSpaceWithTensorOfType k p q} - (σ : K ≃ₐ[k] K) (f : Equiv (V.extendScalars K) (W.extendScalars K)) : - (V.extendScalars K) ≃ₗ[k] (W.extendScalars K) := - auxExtendAlgEquiv V σ ≪≫ₗ auxRestrict f ≪≫ₗ - auxExtendAlgEquiv W σ.symm - -@[simp] -lemma Equiv.algEquivActAux_tmul - {V W : VectorSpaceWithTensorOfType k p q} - (σ : K ≃ₐ[k] K) (f : Equiv (V.extendScalars K) (W.extendScalars K)) - (a : K) (v : V) : - Equiv.algEquivActAux σ f (a ⊗ₜ v) = - (W.auxExtendAlgEquiv σ.symm) (f (σ a ⊗ₜ[k] v)) := by - simp only [algEquivActAux, LinearEquiv.trans_apply, auxExtendAlgEquiv_tmul, auxRestrict_apply] - -variable {K} in -def Equiv.algEquivActAux' - {V W : VectorSpaceWithTensorOfType k p q} - (σ : K ≃ₐ[k] K) (f : Equiv (V.extendScalars K) (W.extendScalars K)) : - (V.extendScalars K) ≃ₗ[K] (W.extendScalars K) where - toFun := Equiv.algEquivActAux σ f - map_add' := map_add _ - map_smul' a x := by - simp only [RingHom.id_apply] - induction x using TensorProduct.induction_on with - | zero => simp only [smul_zero, map_zero, RingHom.id_apply] - | tmul b x => - rw [smul_tmul'] - simp only [algEquivActAux, smul_eq_mul, LinearEquiv.trans_apply, auxExtendAlgEquiv_tmul, - auxRestrict_apply, RingHom.id_apply] - simp only [_root_.map_mul, LinearEquiv.ofLinear_apply] - rw [show (σ a * σ b) ⊗ₜ[k] x = (σ a * σ b) • (1 ⊗ₜ x) by simp only [smul_tmul', - smul_eq_mul, mul_one], map_smul] - have mem : f (1 ⊗ₜ[k] x) ∈ (⊤ : Submodule k _):= ⟨⟩ - rw [← span_tmul_eq_top k K W, mem_span_set] at mem - obtain ⟨c, hc, (eq1 : (∑ i in c.support, _ • _) = _)⟩ := mem - choose xᵢ yᵢ hxy using hc - have eq1 : f (1 ⊗ₜ[k] x) = ∑ i in c.support.attach, (c i.1 • xᵢ i.2) ⊗ₜ[k] yᵢ i.2 := by - rw [← eq1, ← Finset.sum_attach] - refine Finset.sum_congr rfl fun i _ => ?_ - rw [← smul_tmul', hxy i.2] - rw [eq1, Finset.smul_sum, map_sum] - rw [show ∑ i ∈ c.support.attach, (W.auxExtendAlgEquiv σ.symm) - ((σ a * σ b) • (c i.1 • xᵢ i.2) ⊗ₜ[k] yᵢ i.2) = - ∑ i ∈ c.support.attach, (W.auxExtendAlgEquiv σ.symm) - (((σ a * σ b) • c i.1 • xᵢ i.2) ⊗ₜ[k] yᵢ i.2) from Finset.sum_congr rfl fun i _ => by - rw [smul_tmul']] - simp_rw [auxExtendAlgEquiv_tmul] - rw [show ∑ i in c.support.attach, σ.symm ((σ a * σ b) • c i.1 • xᵢ i.2) ⊗ₜ[k] yᵢ i.2 = - ∑ i in c.support.attach, (a * b) • ((c i.1 • σ.symm (xᵢ i.2)) ⊗ₜ[k] yᵢ i.2) from - Finset.sum_congr rfl fun i _ => by - congr 1 - simp only [smul_eq_mul, Algebra.mul_smul_comm, LinearMapClass.map_smul, _root_.map_mul, - AlgEquiv.symm_apply_apply]] - rw [← Finset.smul_sum] - rw [show σ b ⊗ₜ[k] x = σ b • (1 ⊗ₜ x) by simp only [smul_tmul', smul_eq_mul, - mul_one], map_smul, eq1] - conv_rhs => - rw [Finset.smul_sum, map_sum, - show ∑ i in c.support.attach, (W.auxExtendAlgEquiv σ.symm) - (σ b • ((c i.1 • (xᵢ i.2)) ⊗ₜ[k] yᵢ i.2)) = - ∑ i in c.support.attach, (W.auxExtendAlgEquiv σ.symm) - ((σ b • (c i.1 • xᵢ i.2)) ⊗ₜ[k] yᵢ i.2) from Finset.sum_congr rfl fun i _ => by - rw [smul_tmul']] - simp_rw [auxExtendAlgEquiv_tmul] - rw [show ∑ i in c.support.attach, σ.symm (σ b • c i.1 • xᵢ i.2) ⊗ₜ[k] yᵢ i.2 = - ∑ i in c.support.attach, b • (c i.1 • σ.symm (xᵢ i.2) ⊗ₜ[k] yᵢ i.2) from - Finset.sum_congr rfl fun i _ => by - congr 1 - simp only [smul_eq_mul, Algebra.mul_smul_comm, LinearMapClass.map_smul, _root_.map_mul, - AlgEquiv.symm_apply_apply]] - rw [← Finset.smul_sum, ← mul_smul] - congr - | add x y hx hy => aesop - invFun := (Equiv.algEquivActAux σ f).symm - left_inv := (Equiv.algEquivActAux σ f).left_inv - right_inv := (Equiv.algEquivActAux σ f).right_inv - -@[simp] -lemma Equiv.algEquivActAux'_tmul {V W : VectorSpaceWithTensorOfType k p q} - (σ : K ≃ₐ[k] K) (f : Equiv (V.extendScalars K) (W.extendScalars K)) - (a : K) (v : V) : - Equiv.algEquivActAux' σ f (a ⊗ₜ v) = - a • (W.auxExtendAlgEquiv σ.symm) (f (1 ⊗ₜ[k] v)) := by - rw [show a ⊗ₜ v = a • ((1 : K) ⊗ₜ[k] v) by simp only [smul_tmul', smul_eq_mul, mul_one], - map_smul] - simp only [algEquivActAux', LinearEquiv.coe_mk, algEquivActAux_tmul, _root_.map_one] - -lemma Equiv.algEquivActAux'_induced - {V W : VectorSpaceWithTensorOfType k p q} - (σ : K ≃ₐ[k] K) (e : Equiv (V.extendScalars K) (W.extendScalars K)) - (x : TensorOfType K (V.extendScalars K) p q) : - x.induced (Equiv.algEquivActAux' σ e) = - x.induced e := by - induction x using TensorOfType.induction_on with - | zero => simp - | smul a x hx => - rw [TensorOfType.induced_smul, hx, TensorOfType.induced_smul] - | tprod_tmul_tprod v f => - simp only [TensorOfType.induced_tprod_tmul_tprod] - sorry - | add x y hx hy => - rw [TensorOfType.induced_add, hx, hy, TensorOfType.induced_add] - -def Equiv.algEquivAct - {V W : VectorSpaceWithTensorOfType k p q} - (σ : K ≃ₐ[k] K) (f : Equiv (V.extendScalars K) (W.extendScalars K)) : - Equiv (V.extendScalars K) (W.extendScalars K) where - toLinearEquiv := Equiv.algEquivActAux' σ f - map_tensor := by - simp only [extendScalars_tensor] - rw [Equiv.algEquivActAux'_induced] - erw [f.map_tensor] - rfl -end extendScalars - -section twisedForm - -variable (p q : ℕ) -variable {k : Type*} (K : Type*) [CommRing k] [CommRing K] [Algebra k K] -variable (V W : VectorSpaceWithTensorOfType k p q) - -structure twisedForm extends - VectorSpaceWithTensorOfType k p q, - Equiv (V.extendScalars K) (toVectorSpaceWithTensorOfType.extendScalars K) - -end twisedForm - -end VectorSpaceWithTensorOfType diff --git a/BrauerGroup/TensorOfTypePQ/VectorSpaceWithTensorOfTypePQ.lean b/BrauerGroup/TensorOfTypePQ/VectorSpaceWithTensorOfTypePQ.lean new file mode 100644 index 0000000..038a4d5 --- /dev/null +++ b/BrauerGroup/TensorOfTypePQ/VectorSpaceWithTensorOfTypePQ.lean @@ -0,0 +1,606 @@ +import BrauerGroup.TensorOfTypePQ.Basic +import Mathlib.Algebra.Category.ModuleCat.Abelian + +suppress_compilation + +open TensorProduct PiTensorProduct CategoryTheory + +structure VectorSpaceWithTensorOfType (k : Type*) (p q : ℕ) [Field k] where +(carrier : Type*) +[ab : AddCommGroup carrier] +[mod : Module k carrier] +(tensor : TensorOfType k carrier p q) + +namespace VectorSpaceWithTensorOfType + +section basic + +variable {p q : ℕ} +variable {k : Type*} [Field k] (V V₁ V₂ V₃ W : VectorSpaceWithTensorOfType k p q) + +instance : CoeSort (VectorSpaceWithTensorOfType k p q) Type* := ⟨carrier⟩ +instance : AddCommGroup V := V.ab +instance : Module k V := V.mod + +structure Hom extends V →ₗ[k] W where + /-- + ⨂[k]^q V → ⨂[k]^q W + | | + v v + ⨂[k]^p V → ⨂[k]^p W + -/ + comm : + W.tensor ∘ₗ (PiTensorProduct.map fun _ => toLinearMap) = + (PiTensorProduct.map fun _ => toLinearMap) ∘ₗ V.tensor + +instance : FunLike (Hom V W) V W where + coe f := f.toLinearMap + coe_injective' := by + rintro ⟨f, hf⟩ ⟨g, hg⟩ h + aesop + +instance : LinearMapClass (Hom V W) k V W where + map_add f := f.toLinearMap.map_add + map_smulₛₗ f := f.toLinearMap.map_smul + +variable {V W} in +lemma Hom.comm_elementwise (f : Hom V W) (v : ⨂[k]^q V) : + W.tensor ((PiTensorProduct.map fun _ => f.toLinearMap) v) = + (PiTensorProduct.map fun _ => f.toLinearMap) (V.tensor v):= + congr($f.comm v) + +variable {V W} in +@[simp] +lemma Hom.comm_basis {ιV : Type*} (bV : Basis ιV k V) (f : Hom V W) (v : Fin q → ιV) : + (PiTensorProduct.map fun _ => f.toLinearMap) (V.tensor $ tprod k fun i => bV (v i)) = + W.tensor ((tprod k) fun i ↦ f.toLinearMap (bV (v i))) := by + rw [← f.comm_elementwise, PiTensorProduct.map_tprod] + +def Hom.id : Hom V V where + __ := LinearMap.id + comm := by ext; simp + +variable {V₁ V₂ V₃} in +def Hom.comp (f : Hom V₁ V₂) (g : Hom V₂ V₃) : Hom V₁ V₃ where + __ := g.toLinearMap ∘ₗ f.toLinearMap + comm := by + simp only + rw [PiTensorProduct.map_comp, ← LinearMap.comp_assoc, g.comm, LinearMap.comp_assoc, f.comm, + PiTensorProduct.map_comp] + fapply Basis.ext (b := piTensorBasis _ _ _ _ fun _ => Basis.ofVectorSpace k V₁) + intro v + simp only [piTensorBasis_apply, Basis.coe_ofVectorSpace, LinearMap.coe_comp, + Function.comp_apply, map_tprod] + +instance : Category (VectorSpaceWithTensorOfType k p q) where + Hom := Hom + id := Hom.id + comp := Hom.comp + +instance : FunLike (V ⟶ W) V W := + inferInstanceAs (FunLike (Hom V W) V W) + +lemma Hom.toLinearMap_injective : Function.Injective (Hom.toLinearMap : (V ⟶ W) → V →ₗ[k] W) := by + intro f g h + refine DFunLike.ext _ _ ?_ + exact fun x => congr($h x) + +@[simp] +lemma id_toLinearMap : (𝟙 V : Hom V V).toLinearMap = LinearMap.id := rfl + +@[simp] +lemma comp_toLinearMap (f : V ⟶ V₁) (g : V₁ ⟶ V₂) : + (f ≫ g).toLinearMap = g.toLinearMap.comp f.toLinearMap := rfl + +instance : LinearMapClass (V ⟶ W) k V W := + inferInstanceAs (LinearMapClass (Hom V W) k V W) + +end basic + +section extendScalars + +variable {p q : ℕ} +variable {k K : Type*} +variable [Field k] [Field K] [Algebra k K] + +variable (K) in +@[simps tensor carrier] +def extendScalars (V : VectorSpaceWithTensorOfType k p q) {ι : Type*} (b : Basis ι k V) : + VectorSpaceWithTensorOfType K p q where + carrier := K ⊗[k] V + ab := inferInstance + mod := inferInstance + tensor := V.tensor.extendScalars K b + +instance (V : VectorSpaceWithTensorOfType k p q) {ι : Type*} (b : Basis ι k V) : + Module k (V.extendScalars K b):= + inferInstanceAs $ Module k (K ⊗[k] V) + +instance (V : VectorSpaceWithTensorOfType k p q) {ι : Type*} (b : Basis ι k V) : + IsScalarTower k K (V.extendScalars K b) where + smul_assoc a b x := by + simp only [algebra_compatible_smul K, smul_eq_mul, Algebra.id.map_eq_id, _root_.map_mul, + RingHomCompTriple.comp_apply, RingHom.id_apply, mul_smul] + simp only [Algebra.id.map_eq_id, RingHomCompTriple.comp_apply, smul_eq_mul, _root_.map_mul, + RingHom.id_apply, mul_smul] + induction x using TensorProduct.induction_on + · simp + · rw [smul_tmul', smul_tmul', smul_tmul'] + congr + simp only [smul_eq_mul] + rw [algebra_compatible_smul K, smul_eq_mul] + · aesop + +variable (K) in +lemma extendScalars_map_comm + {V W : VectorSpaceWithTensorOfType k p q} (f : V ⟶ W) + {ιV ιW : Type*} (bV : Basis ιV k V) (bW : Basis ιW k W) : + (W.tensor.extendScalars K bW ∘ₗ + PiTensorProduct.map fun _ ↦ f.toLinearMap.extendScalars K) = + (PiTensorProduct.map fun _ ↦ f.toLinearMap.extendScalars K) ∘ₗ + V.tensor.extendScalars K bV := by + have comm' := + congr((bW.extendScalarsTensorPowerEquiv K p).toLinearMap ∘ₗ + $(f.comm).extendScalars K ∘ₗ + (bV.extendScalarsTensorPowerEquiv K q).symm.toLinearMap) + set lhs := _; set rhs := _; change lhs = rhs + set lhs' := _; set rhs' := _; change lhs' = rhs' at comm' + have eql : lhs = lhs' := by + simp only [lhs, lhs'] + fapply Basis.ext (b := Basis.tensorPowerExtendScalars K q bV) + intro v + simp only [Basis.tensorPowerExtendScalars_apply, LinearMap.coe_comp, + Function.comp_apply, map_tprod, LinearMap.extendScalars_apply, LinearEquiv.coe_coe] + have eq1 := bV.extendScalarsTensorPowerEquiv_symm_apply K (p := q) v + rw [eq1] + simp only [LinearMap.extendScalars_apply, LinearMap.coe_comp, Function.comp_apply, map_tprod] + change Basis.extendScalarsTensorPowerEquiv K p bW _ = _ + congr 1 + simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply] + conv_rhs => rw [← LinearMap.extendScalars_apply] + refine DFunLike.congr_arg _ ?_ + simp only [Basis.extendScalarsTensorPowerEquiv_symm_apply'] + have eqr : rhs = rhs' := by + simp only [rhs, rhs'] + fapply Basis.ext (b := Basis.tensorPowerExtendScalars K q bV) + intro v + simp only [Basis.tensorPowerExtendScalars_apply, LinearMap.coe_comp, + Function.comp_apply, LinearEquiv.coe_coe] + have eq1 := bV.extendScalarsTensorPowerEquiv_symm_apply K (p := q) v + rw [eq1] + simp only [LinearMap.extendScalars_apply, LinearMap.coe_comp, + Function.comp_apply] + delta TensorOfType.extendScalars TensorOfType.extendScalarsLinearMap + TensorOfType.extendScalarsLinearMapToFun + dsimp only [LinearMap.coe_mk, AddHom.coe_mk] + simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, + Basis.extendScalarsTensorPowerEquiv_symm_apply, LinearMap.extendScalars_apply] + conv_rhs => rw [← LinearMap.comp_apply, ← LinearMap.extendScalars_apply] + change _ = + ((Basis.extendScalarsTensorPowerEquiv K p bW).toLinearMap ∘ₗ + (LinearMap.extendScalars K ((PiTensorProduct.map fun _ ↦ f.toLinearMap) ∘ₗ V.tensor))) + (1 ⊗ₜ[k] (tprod k) fun j ↦ bV (v j)) + rw [LinearMap.extendScalars_comp, ← LinearMap.comp_assoc, + Basis.extendScalarsTensorPowerEquiv_comp_extendScalars (K := K) (bV := bV) + (bW := bW) (f := f.toLinearMap)] + rfl + rw [eql, eqr, comm'] + +@[simps toLinearMap] +def extendScalarsMap {V W : VectorSpaceWithTensorOfType k p q} (f : V ⟶ W) + {ιV ιW : Type*} (bV : Basis ιV k V) (bW : Basis ιW k W) : + V.extendScalars K bV ⟶ W.extendScalars K bW where + __ := f.extendScalars K + comm := by + simp only [extendScalars_carrier, extendScalars_tensor] + apply extendScalars_map_comm + +@[simps] +def autExtendScalars {V : VectorSpaceWithTensorOfType k p q} + (e : V ≅ V) {ι : Type*} (b : Basis ι k V) : + V.extendScalars K b ≅ V.extendScalars K b where + hom := extendScalarsMap e.hom b b + inv := extendScalarsMap e.inv b b + hom_inv_id := Hom.toLinearMap_injective _ _ $ by + simp only [extendScalars_carrier, comp_toLinearMap, extendScalarsMap_toLinearMap, + id_toLinearMap] + have : e.inv.toLinearMap ∘ₗ e.hom.toLinearMap = _ := congr($(e.hom_inv_id).toLinearMap) + rw [← LinearMap.extendScalars_comp, this] + simp + inv_hom_id := Hom.toLinearMap_injective _ _ $ by + simp only [extendScalars_carrier, comp_toLinearMap, extendScalarsMap_toLinearMap, + id_toLinearMap] + have : e.hom.toLinearMap ∘ₗ e.inv.toLinearMap = _ := congr($(e.inv_hom_id).toLinearMap) + rw [← LinearMap.extendScalars_comp, this] + simp + +variable (k K p q) in +def extendScalarsFunctor : VectorSpaceWithTensorOfType k p q ⥤ VectorSpaceWithTensorOfType K p q where + obj V := V.extendScalars K (Basis.ofVectorSpace k V) + map f := extendScalarsMap f (Basis.ofVectorSpace k _) (Basis.ofVectorSpace k _) + map_id V := Hom.toLinearMap_injective _ _ $ by + simp only [extendScalars_carrier, extendScalarsMap_toLinearMap, id_toLinearMap, + LinearMap.extendScalars_id] + map_comp f g := Hom.toLinearMap_injective _ _ $ by + simp only [extendScalars_carrier, extendScalarsMap_toLinearMap, comp_toLinearMap, + LinearMap.extendScalars_comp] + +end extendScalars + +section gal + +variable {p q : ℕ} {ι k K : Type*} [Field k] [Field K] [Algebra k K] +variable {V : VectorSpaceWithTensorOfType k p q} (b : Basis ι k V) +variable (σ : K →ₐ[k] K) + +set_option maxHeartbeats 500000 in +/-- +(1 ⊗ σ) in general is not `K`-linear, but we have a commutative diagram nevertheless: +``` +⨂[K]^q V_K -(1 ⊗ σ)^q-> ⨂[K]^q V_K + |V_K.tensor |V_K.tensor + v v +⨂[K]^p V_K -(1 ⊗ σ)^p-> ⨂[K]^p V_K +``` +-/ +lemma oneTMulPow_comm_sq_neZero_neZero [NeZero p] [NeZero q] : + (V.extendScalars K b).tensor.restrictScalars k ∘ₗ σ.oneTMulPow q b = + σ.oneTMulPow p b ∘ₗ + (V.extendScalars K b).tensor.restrictScalars k := by + set Bq := b.tensorPowerExtendScalars K q with Bq_eq + set Bp := piTensorBasis (Fin p) k (fun _ => ι) (fun _ => V) (fun _ => b) with Bp_eq + ext v + rw [← Bq.total_repr v, Finsupp.total] + dsimp only [extendScalars_carrier, extendScalars_tensor, Finsupp.coe_lsum, + LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, Finsupp.sum, LinearMap.coe_comp, + LinearMap.coe_restrictScalars, Function.comp_apply] + simp only [Basis.tensorPowerExtendScalars_apply, map_sum, LinearMapClass.map_smul, Bq] + refine Finset.sum_congr rfl fun x _ => ?_ + rw [← Bq_eq, TensorOfType.extendScalars_apply_one_tmul] + simp only [Basis.coe_ofVectorSpace, LinearEquiv.coe_coe] + rw [← (Basis.extendScalarsTensorPowerEquiv K p b).map_smul, smul_tmul', smul_eq_mul, mul_one] + + have eq₁ := (Bp.total_repr $ V.tensor ((tprod k) fun i ↦ b (x i))) + dsimp only [Finsupp.total, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, + Finsupp.sum] at eq₁ + simp only [piTensorBasis_apply, Bp] at eq₁ + simp only [← Bp_eq] at eq₁ + rw [← eq₁, tmul_sum, map_sum, map_sum] + change _ = ∑ z ∈ _, _ + rw [show ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + (AlgHom.oneTMulPow p b σ) + ((Basis.extendScalarsTensorPowerEquiv K p b) + ((Bq.repr v) x ⊗ₜ[k] + ((Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))) z • (tprod k) fun i ↦ b (z i)))) = + ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + AlgHom.oneTMulPow p b σ + (Basis.extendScalarsTensorPowerEquiv K p b $ + (Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • Bq.repr v x) • 1 ⊗ₜ[k] + tprod k fun i => b (z i)) from Finset.sum_congr rfl fun z _ => by + simp only [tmul_smul, smul_tmul', smul_eq_mul, mul_one], + show ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + AlgHom.oneTMulPow p b σ + (Basis.extendScalarsTensorPowerEquiv K p b $ + (Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • Bq.repr v x) • 1 ⊗ₜ[k] + tprod k fun i => b (z i)) = + ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + AlgHom.oneTMulPow p b σ + ((Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • Bq.repr v x) • + Basis.extendScalarsTensorPowerEquiv K p b (1 ⊗ₜ[k] tprod k fun i => b (z i))) from + Finset.sum_congr rfl fun z _ => by rw [map_smul], + show ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + AlgHom.oneTMulPow p b σ + ((Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • Bq.repr v x) • + Basis.extendScalarsTensorPowerEquiv K p b (1 ⊗ₜ[k] tprod k fun i => b (z i))) = + ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + AlgHom.oneTMulPow p b σ + ((Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • Bq.repr v x) • + tprod K fun i => 1 ⊗ₜ[k] b (z i)) from Finset.sum_congr rfl fun z _ => by + rw [Basis.extendScalarsTensorPowerEquiv_apply], + show ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + AlgHom.oneTMulPow p b σ + ((Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • Bq.repr v x) • + tprod K fun i => 1 ⊗ₜ[k] b (z i)) = + ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + (Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • + AlgHom.oneTMulPow p b σ (Bq.repr v x • tprod K fun i => 1 ⊗ₜ[k] b (z i))) from + Finset.sum_congr rfl fun z _ => by rw [← (AlgHom.oneTMulPow p b σ).map_smul, smul_assoc], + show ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + (Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • + AlgHom.oneTMulPow p b σ (Bq.repr v x • tprod K fun i => 1 ⊗ₜ[k] b (z i))) = + ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + (Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • + AlgHom.oneTMulPow p b σ ((∏ i : Fin p, if i = 0 then Bq.repr v x else 1) • + tprod K fun i => 1 ⊗ₜ[k] b (z i))) from Finset.sum_congr rfl fun z _ => by + simp only [Finset.prod_ite_eq', Finset.mem_univ, ↓reduceIte], + show ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + (Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • + AlgHom.oneTMulPow p b σ ((∏ i : Fin p, if i = 0 then Bq.repr v x else 1) • + tprod K fun i => 1 ⊗ₜ[k] b (z i))) = + ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + (Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • + AlgHom.oneTMulPow p b σ + (tprod K fun i => (if i = 0 then Bq.repr v x else 1) ⊗ₜ[k] b (z i))) from + Finset.sum_congr rfl fun z _ => by + rw [← MultilinearMap.map_smul_univ] + simp_rw [smul_tmul', smul_eq_mul, mul_one], + show ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + (Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • + AlgHom.oneTMulPow p b σ (tprod K fun i => (if i = 0 then Bq.repr v x else 1) ⊗ₜ[k] b (z i))) = + ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + (Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • + (σ $ Bq.repr v x) • (tprod K fun i => 1 ⊗ₜ[k] b (z i))) from Finset.sum_congr rfl fun z _ => by + simp only [AlgHom.oneTMulPow_apply, + show + (∏ i : Fin p, σ (if i = 0 then Bq.repr v x else 1)) = + (∏ i : Fin p, if i = 0 then (σ $ Bq.repr v x) else 1) + from Finset.prod_congr rfl fun _ _ => by split_ifs <;> simp, + Finset.prod_ite_eq', Finset.mem_univ, ↓reduceIte], + show ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + (Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • + (σ $ Bq.repr v x) • (tprod K fun i => (1 : K) ⊗ₜ[k] b (z i))) = + ∑ z ∈ (Bp.repr (V.tensor ((tprod k) fun i ↦ b (x i)))).support, + (σ $ Bq.repr v x) • ((Bp.repr (V.tensor $ tprod k fun i => b (x i)) z • + (tprod K fun i => (1 : K) ⊗ₜ[k] b (z i)))) from Finset.sum_congr rfl fun z _ => by + rw [smul_comm], ← Finset.smul_sum] + rw [show ((Bq.repr v) x • (tprod K) fun j ↦ (1 : K) ⊗ₜ[k] b (x j)) = + tprod K fun j ↦ ((if j = 0 then (Bq.repr v) x else 1) ⊗ₜ[k] b (x j)) by + rw [show (Bq.repr v) x = ∏ i : Fin q, if i = 0 then (Bq.repr v) x else 1 by simp, + ← MultilinearMap.map_smul_univ] + congr 2 + ext j + split_ifs with h + · subst h; simp only [smul_tmul', smul_eq_mul, mul_one, Finset.prod_ite_eq', Finset.mem_univ, + ↓reduceIte] + · simp only [one_smul]] + rw [AlgHom.oneTMulPow_apply, map_smul, TensorOfType.extendScalars_apply_tmul] + simp only [Finset.prod_const_one, LinearEquiv.coe_coe] + rw [show (∏ i : Fin q, σ (if i = 0 then (Bq.repr v) x else 1)) = + (∏ i : Fin q, if i = 0 then σ (Bq.repr v x) else 1) from + Finset.prod_congr rfl fun _ _ => by split_ifs <;> simp] + simp only [Finset.prod_ite_eq', Finset.mem_univ, ↓reduceIte] + conv_lhs => rw [← eq₁] + rw [tmul_sum, map_sum] + congr 1 + refine Finset.sum_congr rfl fun z _ => ?_ + rw [tmul_smul, algebra_compatible_smul K, map_smul, algebraMap_smul] + congr 1 + simp only [Basis.extendScalarsTensorPowerEquiv_apply] + +set_option maxHeartbeats 500000 in +lemma oneTMulPow_comm_sq_p_zero + {V : VectorSpaceWithTensorOfType k 0 q} (b : Basis ι k V) [NeZero q] : + (V.extendScalars K b).tensor.restrictScalars k ∘ₗ σ.oneTMulPow q b = + σ.oneTMulPow 0 b ∘ₗ + (V.extendScalars K b).tensor.restrictScalars k := by + have eq₁ := AlgHom.oneTMulPow_apply_q_zero (σ := σ) (K := K) (b := b) + rw [eq₁] + simp only [extendScalars_carrier, extendScalars_tensor] + ext x + simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, + LinearEquiv.coe_coe, AlgHom.toLinearMap_apply, isEmptyEquiv_symm_apply] + set B := b.tensorPowerExtendScalars K q with B_eq + have eq₁ := B.total_repr x |>.symm + conv_lhs => rw [eq₁] + dsimp only [Finsupp.total, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, + Finsupp.sum] + simp only [Basis.tensorPowerExtendScalars_apply, map_sum, B] + simp only [← B_eq, AlgHom.oneTMulPow_apply', LinearMapClass.map_smul] + rw [show (∑ z ∈ (B.repr x).support, + σ ((B.repr x) z) • (TensorOfType.extendScalars K b V.tensor) + ((tprod K) fun i ↦ 1 ⊗ₜ[k] b (z i))) = + ∑ z ∈ (B.repr x).support, + σ ((B.repr x) z) • (b.extendScalarsTensorPowerEquiv K 0) + ((1 : K) ⊗ₜ[k] (V.tensor $ tprod k fun i => b (z i))) from + Finset.sum_congr rfl fun z _ => by + rw [TensorOfType.extendScalars_apply_one_tmul (f := V.tensor) (K := K) (b := b)] + simp] + simp_rw [Basis.extendScalarsTensorPowerEquiv_zero_apply] + simp only [isEmptyEquiv_symm_apply, smul_assoc, one_smul] + change ∑ z ∈ _, _ = _ + rw [show ∑ z ∈ (B.repr x).support, + σ ((B.repr x) z) • (isEmptyEquiv (Fin 0)) (V.tensor ((tprod k) fun i ↦ b (z i))) • (tprod K) isEmptyElim = + ∑ z ∈ (B.repr x).support, + ((isEmptyEquiv (Fin 0)) (V.tensor ((tprod k) fun i ↦ b (z i))) • σ ((B.repr x) z) ) • (tprod K) isEmptyElim from + Finset.sum_congr rfl fun z _ => by + simp only [smul_assoc] + rw [smul_comm]] + rw [← Finset.sum_smul] + congr 1 + simp_rw [← map_smul] + rw [← map_sum] + congr 1 + conv_rhs => rw [eq₁] + dsimp only [Finsupp.total, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, + Finsupp.sum] + simp only [map_sum, map_smul, smul_eq_mul] + refine Finset.sum_congr rfl fun z _ => ?_ + simp only [Basis.tensorPowerExtendScalars_apply, B] + simp only [← B_eq] + rw [algebra_compatible_smul K, smul_eq_mul, mul_comm] + congr 1 + rw [TensorOfType.extendScalars_apply_one_tmul] + simp only [LinearEquiv.coe_coe, EmbeddingLike.apply_eq_iff_eq] + rw [Basis.extendScalarsTensorPowerEquiv_zero_apply] + simp only [isEmptyEquiv_symm_apply, smul_assoc, one_smul] + rw [algebra_compatible_smul K, map_smul] + simp only [isEmptyEquiv_apply_tprod, smul_eq_mul, mul_one] + +lemma oneTMulPow_comm_sq_q_zero + {V : VectorSpaceWithTensorOfType k p 0} (b : Basis ι k V) [NeZero p] : + (V.extendScalars K b).tensor.restrictScalars k ∘ₗ σ.oneTMulPow 0 b = + σ.oneTMulPow p b ∘ₗ + (V.extendScalars K b).tensor.restrictScalars k := by + have eq₁ := AlgHom.oneTMulPow_apply_q_zero (σ := σ) (K := K) (b := b) + rw [eq₁] + simp only [extendScalars_carrier, extendScalars_tensor] + ext x + simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, + Function.comp_apply, AlgHom.toLinearMap_apply, isEmptyEquiv_symm_apply, LinearMapClass.map_smul] + induction x using PiTensorProduct.induction_on with + | smul_tprod a x => + simp only [LinearMapClass.map_smul, isEmptyEquiv_apply_tprod, smul_eq_mul, mul_one] + have eqx : x = isEmptyElim := List.ofFn_inj.mp rfl + subst eqx + unfold TensorOfType.extendScalars TensorOfType.extendScalarsLinearMap + TensorOfType.extendScalarsLinearMapToFun + simp only [LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply, Basis.extendScalarsTensorPowerEquiv_zero_symm_apply', + LinearMap.extendScalars_apply] + set X := V.tensor ((tprod k) fun a ↦ isEmptyElim a) + set B : Basis _ k (⨂[k]^p V.carrier) := piTensorBasis _ _ _ _ (fun _ => b) with B_eq + have eq₁ := B.total_repr X |>.symm + rw [eq₁] + dsimp only [Finsupp.total, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, + Finsupp.sum] + simp only [piTensorBasis_apply, tmul_sum, tmul_smul, map_sum, Finset.smul_sum, B] + simp only [← B_eq] + refine Finset.sum_congr rfl fun z _ => ?_ + conv_lhs => rw [algebra_compatible_smul K (B.repr X z), + (Basis.extendScalarsTensorPowerEquiv K p b).map_smul, algebraMap_smul, smul_comm] + conv_rhs => rw [algebra_compatible_smul K (B.repr X z), + (Basis.extendScalarsTensorPowerEquiv K p b).map_smul, algebraMap_smul, + smul_comm, (AlgHom.oneTMulPow p b σ).map_smul] + refine congr_arg ((B.repr X) z • ·) ?_ + simp only [Basis.extendScalarsTensorPowerEquiv_apply, AlgHom.oneTMulPow_apply'] + | add x y hx hy => + simp only [map_add, add_smul, hx, hy] + +lemma oneTMulPow_comm_sq_p_zero_q_zero + {V : VectorSpaceWithTensorOfType k 0 0} (b : Basis ι k V) : + (V.extendScalars K b).tensor.restrictScalars k ∘ₗ σ.oneTMulPow 0 b = + σ.oneTMulPow 0 b ∘ₗ + (V.extendScalars K b).tensor.restrictScalars k := by + have eq₁ := AlgHom.oneTMulPow_apply_q_zero (σ := σ) (K := K) (b := b) + rw [eq₁] + simp only [extendScalars_carrier, extendScalars_tensor] + ext x + simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, + Function.comp_apply, AlgHom.toLinearMap_apply, isEmptyEquiv_symm_apply, LinearMapClass.map_smul] + induction x using PiTensorProduct.induction_on with + | smul_tprod a v => + have eqv : v = isEmptyElim := List.ofFn_inj.mp rfl + subst eqv + simp only [LinearMapClass.map_smul, isEmptyEquiv_apply_tprod, smul_eq_mul, mul_one, + _root_.map_mul] + unfold TensorOfType.extendScalars TensorOfType.extendScalarsLinearMap + TensorOfType.extendScalarsLinearMapToFun + simp only [LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply, Basis.extendScalarsTensorPowerEquiv_zero_symm_apply', + LinearMap.extendScalars_apply] + simp only [Basis.extendScalarsTensorPowerEquiv_zero_apply, isEmptyEquiv_symm_apply, smul_assoc, + one_smul] + rw [algebra_compatible_smul K ((isEmptyEquiv (Fin 0)) _), ← smul_assoc] + congr 1 + rw [smul_eq_mul] + congr 1 + rw [map_smul] + simp only [isEmptyEquiv_apply_tprod, smul_eq_mul, mul_one, AlgHom.commutes] + | add x y hx hy => + simp only [map_add, add_smul, hx, hy] + +lemma oneTMulPow_comm_sq : + (V.extendScalars K b).tensor.restrictScalars k ∘ₗ σ.oneTMulPow q b = + σ.oneTMulPow p b ∘ₗ + (V.extendScalars K b).tensor.restrictScalars k := by + by_cases hp : p = 0 + · subst hp + by_cases hq : q = 0 + · subst hq + apply oneTMulPow_comm_sq_p_zero_q_zero + · haveI : NeZero q := ⟨hq⟩ + apply oneTMulPow_comm_sq_p_zero + · haveI : NeZero p := ⟨hp⟩ + by_cases hq : q = 0 + · subst hq + apply oneTMulPow_comm_sq_q_zero + · haveI : NeZero q := ⟨hq⟩ + apply oneTMulPow_comm_sq_neZero_neZero + +end gal + +section gal + +variable {n p q : ℕ} {ιV ιW k K : Type*} [Field k] [Field K] [Algebra k K] +variable {V W : VectorSpaceWithTensorOfType k p q} (bV : Basis ιV k V) (bW : Basis ιW k W) +variable (σ : K ≃ₐ[k] K) (f : V.extendScalars K bV ⟶ W.extendScalars K bW) + + + +/-- +⨂[K]^q V_K -(1 ⊗ σ)^q-> ⨂[K]^q V_K -f^q-> ⨂[K]^q W_K -(1 ⊗ σ⁻¹)^q -> ⨂[K]^q W_K + +is equal to + +(σ ∘ f ∘ σ⁻¹)^q +-/ + +lemma galAct_tensor_power_eq : + (PiTensorProduct.map fun _ => f.toLinearMap.galAct σ : + (⨂[K]^n (K ⊗[k] V)) →ₗ[K] (⨂[K]^n (K ⊗[k] W))).restrictScalars k = + σ.toAlgHom.oneTMulPow n bW ∘ₗ + (PiTensorProduct.map fun _ => f.toLinearMap).restrictScalars k ∘ₗ + σ.symm.toAlgHom.oneTMulPow n bV := by + ext x + simp only [LinearMap.coe_restrictScalars, AlgEquiv.toAlgHom_eq_coe, extendScalars_carrier, + LinearMap.coe_comp, Function.comp_apply] + set B := bV.tensorPowerExtendScalars K n with B_eq + have eq₁ := B.total_repr x |>.symm + rw [eq₁] + dsimp only [Finsupp.total, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, + Finsupp.sum] + simp only [map_sum, LinearMapClass.map_smul] + refine Finset.sum_congr rfl fun z _ => ?_ + simp only [Basis.tensorPowerExtendScalars_apply, map_tprod, LinearMap.galAct_extendScalars_apply, + _root_.map_one, AlgHom.oneTMulPow_apply', AlgHom.coe_coe, LinearMapClass.map_smul, B] + simp only [← B_eq] + let X (i : Fin n) := f.toLinearMap (1 ⊗ₜ[k] bV (z i)) + change (B.repr x z) • (tprod K fun i => (LinearMap.rTensor W.carrier σ.toLinearMap) (X i)) = _ + convert_to _ = + (AlgHom.oneTMulPow n bW σ.toAlgHom) (σ.symm ((B.repr x) z) • (tprod K fun i => X i)) + set B' : Basis _ K (K ⊗[k] W) := Algebra.TensorProduct.basis _ bW with B'_eq + have eq₂ (i : Fin n) := B'.total_repr (X i) |>.symm + dsimp only [Finsupp.total, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, + Finsupp.sum] at eq₂ + simp only [Algebra.TensorProduct.basis_apply, smul_tmul', smul_eq_mul, mul_one, B'] at eq₂ + simp only [← B'_eq] at eq₂ + + set lhs := _; set rhs := _; change lhs = rhs + rw [show lhs = B.repr x z • tprod K fun i => (LinearMap.rTensor W.carrier σ.toLinearMap) + (∑ z ∈ (B'.repr (X i)).support, B'.repr (X i) z ⊗ₜ[k] bW z) by + simp only [lhs] + congr; ext i + conv_lhs => rw [eq₂]] + simp only [map_sum, LinearMap.rTensor_tmul, AlgEquiv.toLinearMap_apply] + rw [MultilinearMap.map_sum_finset, Finset.smul_sum] + rw [show rhs = (AlgHom.oneTMulPow n bW ↑σ) (σ.symm ((B.repr x) z) • (tprod K) fun i ↦ + ∑ z ∈ (B'.repr (X i)).support, B'.repr (X i) z ⊗ₜ[k] bW z) by + simp only [rhs] + congr; ext i + conv_lhs => rw [eq₂]] + rw [MultilinearMap.map_sum_finset, Finset.smul_sum] + simp only [map_sum] + refine Finset.sum_congr rfl fun i _ => ?_ + rw [AlgHom.oneTMulPow_apply''] + simp only [AlgHom.coe_coe, AlgEquiv.apply_symm_apply] + congr 1 + rw [← MultilinearMap.map_smul_univ] + simp only [smul_tmul', smul_eq_mul, mul_one] + + +end gal + +section twisedForm + +variable {p q : ℕ} +variable {k : Type*} (K : Type*) [Field k] [Field K] [Algebra k K] +variable (V W : VectorSpaceWithTensorOfType k p q) + +structure TwisedForm where + carrier : VectorSpaceWithTensorOfType k p q + exists_iso : Nonempty $ (V.extendScalars K (Basis.ofVectorSpace k V)) ≅ + (carrier.extendScalars K (Basis.ofVectorSpace k carrier)) + +end twisedForm + +end VectorSpaceWithTensorOfType