Lean4
/-- If `m₁` and `m₂` are both homogeneous,
and the quadratic spaces `Q₁` and `Q₂` map into
orthogonal subspaces of `Qₙ` (for instance, when `Qₙ = Q₁.prod Q₂`),
then the product of the embedding in `CliffordAlgebra Q` commutes up to a sign factor. -/
nonrec theorem map_mul_map_of_isOrtho_of_mem_evenOdd {i₁ i₂ : ZMod 2} (hm₁ : m₁ ∈ evenOdd Q₁ i₁)
(hm₂ : m₂ ∈ evenOdd Q₂ i₂) : map f₁ m₁ * map f₂ m₂ = (-1 : ℤˣ) ^ (i₂ * i₁) • (map f₂ m₂ * map f₁ m₁) := by
-- the strategy; for each variable, induct on powers of `ι`, then on the exponent of each
-- power.
induction hm₁ using Submodule.iSup_induction' with
| zero => rw [map_zero, zero_mul, mul_zero, smul_zero]
| add _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
| mem i₁' m₁' hm₁ =>
obtain ⟨i₁n, rfl⟩ := i₁'
dsimp only at *
induction hm₁ using Submodule.pow_induction_on_left' with
| algebraMap => rw [AlgHom.commutes, Nat.cast_zero, mul_zero, uzpow_zero, one_smul, Algebra.commutes]
| add _ _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
| mem_mul m₁ hm₁ i x₁ _hx₁ ih₁ =>
obtain ⟨v₁, rfl⟩ := hm₁
rw [map_mul, mul_assoc, ih₁, mul_smul_comm, map_apply_ι, Nat.cast_succ, mul_add_one, uzpow_add, mul_smul, ←
mul_assoc, ← mul_assoc, ← smul_mul_assoc ((-1) ^ i₂)]
clear ih₁
congr 2
induction hm₂ using Submodule.iSup_induction' with
| zero => rw [map_zero, zero_mul, mul_zero, smul_zero]
| add _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
| mem i₂' m₂' hm₂ =>
clear m₂
obtain ⟨i₂n, rfl⟩ := i₂'
dsimp only at *
induction hm₂ using Submodule.pow_induction_on_left' with
| algebraMap => rw [AlgHom.commutes, Nat.cast_zero, uzpow_zero, one_smul, Algebra.commutes]
| add _ _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
| mem_mul m₂ hm₂ i x₂ _hx₂ ih₂ =>
obtain ⟨v₂, rfl⟩ := hm₂
rw [map_mul, map_apply_ι, Nat.cast_succ, ← mul_assoc, ι_mul_ι_comm_of_isOrtho (hf _ _), neg_mul, mul_assoc,
ih₂, mul_smul_comm, ← mul_assoc, ← Units.neg_smul, uzpow_add, uzpow_one, mul_neg_one]
