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,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