English
The graded multiplication on tensor powers is associative: (a ₜ* b) ₜ* c = a ₜ* (b ₜ* c) up to the corresponding cast along add_assoc.
Русский
Градуированное умножение на тензорные степени ассоциативно: (a ₜ* b) ₜ* c = a ₜ* (b ₜ* c) с учётом композиции индексов.
LaTeX
$$cast R M (add_assoc _ _ _) (gMul.mul (gMul.mul a b) c) = gMul.mul a (gMul.mul b c)$$
Lean4
theorem mul_assoc {na nb nc} (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M) :
cast R M (add_assoc _ _ _) (a ₜ* b ₜ* c) = a ₜ* (b ₜ* c) :=
by
let mul : ∀ n m : ℕ, ⨂[R]^n M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M := fun n m =>
(TensorProduct.mk R _ _).compr₂
↑(mulEquiv : _ ≃ₗ[R] (⨂[R]^(n + m)) M)
-- replace `a`, `b`, `c` with `tprod R a`, `tprod R b`, `tprod R c`
let e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (add_assoc _ _ _)
let lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
(LinearMap.llcomp R _ _ _ ((mul _ nc).compr₂ e.toLinearMap)).comp (mul na nb)
have lhs_eq : ∀ a b c, lhs a b c = e (a ₜ* b ₜ* c) := fun _ _ _ => rfl
let rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
(LinearMap.llcomp R _ _ _ (LinearMap.lflip (R := R)).toLinearMap <|
(LinearMap.llcomp R _ _ _ (mul na _).flip).comp (mul nb nc)).flip
have rhs_eq : ∀ a b c, rhs a b c = a ₜ* (b ₜ* c) := fun _ _ _ => rfl
suffices lhs = rhs from LinearMap.congr_fun (LinearMap.congr_fun (LinearMap.congr_fun this a) b) c
ext a b c
simp only [e, LinearMap.compMultilinearMap_apply, lhs_eq, rhs_eq, tprod_mul_tprod, cast_tprod]
congr 1 with j
rw [Fin.append_assoc]
refine congr_arg (Fin.append a (Fin.append b c)) (Fin.ext ?_)
rw [Fin.coe_cast, Fin.coe_cast]
-- for now we just use the default for the `gnpow` field as it's easier.
