CocycleBasis.lean

1 import PaperXI.CocycleCommutator
2 import Mathlib.LinearAlgebra.Basis.SMul
3 import Mathlib.Algebra.Algebra.Basic
4 
5 /-! Paper XI, Proposition 8.1: the coefficient change in an actual algebra basis. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CocycleCommutator
9 open Module
10 
11 variable {A K B : Type*} [CommGroup A] [CommRing K] [Ring B] [Algebra K B]
12 
13 /-- Rescaling the actual basis, not merely a coefficient function, gives the
14 coboundary formula for its multiplication table. -/
15 theorem rescaled_basis_mul (c : Cocycle A Kˣ) (u : Basis A K B)
16     (hu : ∀ a b, u a * u b = (c.coeff a b : K) • u (a * b))
17     (s : A → Kˣ) (a b : A) :
18     u.unitsSMul s a * u.unitsSMul s b =
19       ((rescale c s).coeff a b : K) • u.unitsSMul s (a * b) := by
20   simp only [Basis.unitsSMul_apply, Units.smul_def, smul_mul_assoc, mul_smul_comm,
21     hu, smul_smul, rescale, div_eq_mul_inv, Units.val_mul]
22   congr 1
23   exact congrArg (fun t : Kˣ => (t : K)) (show
24     s b * (s a * c.coeff a b) =
25       (s a * s b * (s (a * b))⁻¹ * c.coeff a b) * s (a * b) by
26     simp [mul_assoc, mul_comm, mul_left_comm])
27 
28 /-- After the actual basis change, the scalar commutator is unchanged. -/
29 theorem rescaled_basis_commutator (c : Cocycle A Kˣ) (s : A → Kˣ) (a b : A) :
30     (rescale c s).coeff a b / (rescale c s).coeff b a =
31       c.coeff a b / c.coeff b a := commutator_rescale c s a b
32 
33 end PaperXI.CocycleCommutator

Back to source controls