hom approach of tensor of type p q

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

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

BrauerGroup/GaloisDescent/Basic.lean

@@ -0,0 +1,57 @@
+import BrauerGroup.TensorOfTypePQ.VectorSpaceWithTensorOfTypePQ
+
+suppress_compilation
+
+open TensorProduct PiTensorProduct
+
+variable {k K : Type*} {p q : ℕ} [Field k] [Field K] [Algebra k K]
+variable {V W : VectorSpaceWithTensorOfType k p q}
+variable {ιV ιW : Type*} (bV : Basis ιV k V) (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
+
+def inducedByGal (σ : 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

BrauerGroup/LinearMap.lean

@@ -0,0 +1,107 @@
+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]
+
+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
+
+end