mathlib3 documentation

lean-ga / geometric_algebra.from_mathlib.mathoverflow

A formalization of https://mathoverflow.net/questions/60596/clifford-pbw-theorem-for-quadratic-form/87958#87958

Some Zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.F0.9D.94.BD.E2.82.82.5B.CE.B1.2C.20.CE.B2.2C.20.CE.B3.5D.20.2F.20.28.CE.B1.C2.B2.2C.20.CE.B2.C2.B2.2C.20.CE.B3.C2.B2.29/near/222716333.

source
theorem ideal.comap_span_le {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : S →+* R) (g : R →+* S) (h : function.left_inverse ⇑g ⇑f) (s : set R) :
ideal.comap f (ideal.span s) ≤ ideal.span (⇑g '' s)
source
theorem char_p.quotient_iff' (R : Type u_1) [comm_ring R] (n : ℕ) [char_p R n] (I : ideal R) :
char_p (R ⧸ I) n ↔ ∀ (x : ℕ), ↑x ∈ I → ↑x = 0

char_p.quotient' as an iff.

source
theorem ideal.span_le_bot {R : Type u_1} [semiring R] (s : set R) :
ideal.span s ≤ ⊥ ↔ s ≤ {0}
source
theorem char_p.quotient_iff'' (R : Type u_1) [comm_ring R] (n : ℕ) [char_p R n] (I : ideal R) :
char_p (R ⧸ I) n ↔ ideal.comap (nat.cast_ring_hom R) I ≤ ring_hom.ker (nat.cast_ring_hom R)

char_p.quotient' as an iff.

source
theorem finsupp.equiv_fun_on_finite_const {α : Type u_1} {β : Type u_2} [fintype α] [add_comm_monoid β] (b : β) :
⇑(finsupp.equiv_fun_on_finite.symm) (λ (_x : α), b) = finset.univ.sum (λ (i : α), finsupp.single i b)
source
theorem mv_polynomial.support_smul' {S : Type u_1} {R : Type u_2} {σ : Type u_3} [comm_semiring R] [monoid S] [distrib_mul_action S R] {r : S} {p : mv_polynomial σ R} :
(r • p).support ⊆ p.support
source
theorem finsupp.to_multiset_sup {α : Type u_1} [decidable_eq α] (f g : α →₀ ℕ) :
⇑finsupp.to_multiset (f ⊔ g) = ⇑finsupp.to_multiset f ∪ ⇑finsupp.to_multiset g
source
theorem finsupp.to_multiset_inf {α : Type u_1} [decidable_eq α] (f g : α →₀ ℕ) :
⇑finsupp.to_multiset (f ⊓ g) = ⇑finsupp.to_multiset f ∩ ⇑finsupp.to_multiset g
source
def linear_equiv.ulift (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] :
ulift M ≃ₗ[R] M

equiv.ulift as a linear_equiv.

Equations
source
@[simp]
theorem linear_equiv.ulift_symm_apply (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] (ᾰ : M) :
⇑((linear_equiv.ulift R M).symm) ᾰ = equiv.ulift.inv_fun ᾰ
source
@[simp]
theorem linear_equiv.ulift_apply (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] (ᾰ : ulift M) :
⇑(linear_equiv.ulift R M) ᾰ = equiv.ulift.to_fun ᾰ
source
theorem ideal.mem_span_range_iff_exists_fun {ι : Type u_1} {R : Type u_2} [fintype ι] [comm_semiring R] (g : ι → R) (x : R) :
x ∈ ideal.span (set.range g) ↔ ∃ (f : ι → R), finset.univ.sum (λ (i : ι), f i * g i) = x
source
noncomputable def q60596.k_ideal  :
ideal (mv_polynomial (fin 3) (zmod 2))

The monomial ideal generated by terms of the form $x_ix_i$.

Equations
source
theorem q60596.mem_k_ideal_iff (x : mv_polynomial (fin 3) (zmod 2)) :
x ∈ q60596.k_ideal ↔ ∀ (m : fin 3 →₀ ℕ), m ∈ x.support → (∃ (i : fin 3), 2 ≤ ⇑m i)
source
theorem q60596.X0_X1_X2_nmem_k_ideal  :
mv_polynomial.X 0 * mv_polynomial.X 1 * mv_polynomial.X 2 ∉ q60596.k_ideal
source
theorem q60596.mul_self_mem_k_ideal_of_X0_X1_X2_mul_mem {x : mv_polynomial (fin 3) (zmod 2)} (h : mv_polynomial.X 0 * mv_polynomial.X 1 * mv_polynomial.X 2 * x ∈ q60596.k_ideal) :
x * x ∈ q60596.k_ideal
source
@[protected, instance]
noncomputable def q60596.k.add_comm_monoid  :
add_comm_monoid q60596.k
source
@[protected, instance]
noncomputable def q60596.k.add_comm_group  :
add_comm_group q60596.k
source
def q60596.k  :
Type
Equations
Instances for q60596.k
source
@[protected, instance]
noncomputable def q60596.k.ring  :
ring q60596.k
source
@[protected, instance]
noncomputable def q60596.k.comm_semiring  :
comm_semiring q60596.k
source
@[protected, instance]
noncomputable def q60596.k.semiring  :
semiring q60596.k
source
@[protected, instance]
noncomputable def q60596.k.comm_ring  :
comm_ring q60596.k
source
theorem q60596.comap_C_span_le_bot  :
ideal.comap mv_polynomial.C q60596.k_ideal ≤ ⊥
source
@[protected, instance]
def q60596.k.char_p  :
char_p q60596.k 2

k has characteristic 2.

source
@[reducible]
noncomputable def q60596.α  :
q60596.k
source
@[reducible]
noncomputable def q60596.β  :
q60596.k
source
@[reducible]
noncomputable def q60596.γ  :
q60596.k
source
@[simp]
theorem q60596.X_sq (i : fin 3) :
⇑(ideal.quotient.mk q60596.k_ideal) (mv_polynomial.X i) * ⇑(ideal.quotient.mk q60596.k_ideal) (mv_polynomial.X i) = 0

The elements above square to zero

source
theorem q60596.sq_zero_of_αβγ_mul {x : q60596.k} :
q60596.α * q60596.β * q60596.γ * x = 0 → x * x = 0

If an element multiplied by αβγ is zero then it squares to zero.

source
theorem q60596.αβγ_ne_zero  :
q60596.α * q60596.β * q60596.γ ≠ 0

Though αβγ is not itself zero

source
@[simp]
theorem q60596.L_func_apply (ᾰ : fin 3 → q60596.k) :
⇑q60596.L_func ᾰ = q60596.α * ᾰ 0 + q60596.β * ᾰ 1 + q60596.γ * ᾰ 2
source
noncomputable def q60596.L_func  :
(fin 3 → q60596.k) →ₗ[q60596.k] q60596.k
Equations
source
@[protected, instance]
noncomputable def q60596.L.add_comm_group  :
add_comm_group q60596.L
source
@[protected, instance]
noncomputable def q60596.L.module  :
module q60596.k q60596.L
source
def q60596.L  :
Type

The quotient of k^3 by the specified relation

Equations
Instances for q60596.L
source
def q60596.sq {ι : Type u_1} {R : Type u_2} [comm_ring R] (i : ι) :
quadratic_form R (ι → R)
Equations
source
theorem q60596.sq_map_add_char_two {ι : Type u_1} {R : Type u_2} [comm_ring R] [char_p R 2] (i : ι) (a b : ι → R) :
⇑(q60596.sq i) (a + b) = ⇑(q60596.sq i) a + ⇑(q60596.sq i) b
source
theorem q60596.sq_map_sub_char_two {ι : Type u_1} {R : Type u_2} [comm_ring R] [char_p R 2] (i : ι) (a b : ι → R) :
⇑(q60596.sq i) (a - b) = ⇑(q60596.sq i) a - ⇑(q60596.sq i) b
source
noncomputable def q60596.Q'  :
quadratic_form q60596.k (fin 3 → q60596.k)

The quadratic form (metric) is just euclidean

Equations
source
def q60596.Q'_add (x y : fin 3 → q60596.k) :
⇑q60596.Q' (x + y) = ⇑q60596.Q' x + ⇑q60596.Q' y
source
def q60596.Q'_sub (x y : fin 3 → q60596.k) :
⇑q60596.Q' (x - y) = ⇑q60596.Q' x - ⇑q60596.Q' y
source
theorem q60596.Q'_apply (a : fin 3 → q60596.k) :
⇑q60596.Q' a = a 0 * a 0 + a 1 * a 1 + a 2 * a 2
source
theorem q60596.Q'_apply_single (i : fin 3) (x : q60596.k) :
⇑q60596.Q' (pi.single i x) = x * x
source
theorem q60596.Q'_zero_under_ideal (v : fin 3 → q60596.k) (hv : v ∈ linear_map.ker q60596.L_func) :
⇑q60596.Q' v = 0
source
noncomputable def q60596.Q  :
quadratic_form q60596.k q60596.L

Q', lifted to operate on the quotient space L.

Equations
source
@[simp]
theorem q60596.Q_apply (x : q60596.L) :
⇑q60596.Q x = quotient.lift_on' x ⇑q60596.Q' q60596.Q._proof_1

Shorthand for basis vectors in the Clifford algebra

source
@[reducible]
noncomputable def q60596.x'  :
clifford_algebra q60596.Q
source
@[reducible]
noncomputable def q60596.y'  :
clifford_algebra q60596.Q
source
@[reducible]
noncomputable def q60596.z'  :
clifford_algebra q60596.Q
source
@[simp]
theorem q60596.x_mul_x  :
q60596.x' * q60596.x' = 1

The basis vectors square to one

source
theorem q60596.quot_obv  :
q60596.α • q60596.x' - q60596.β • q60596.y' - q60596.γ • q60596.z' = 0

By virtue of the quotient, terms of this form are zero

source
theorem q60596.αβγ_smul_eq_zero  :
(q60596.α * q60596.β * q60596.γ) • 1 = 0

The core of the proof - scaling 1 by α * β * γ gives zero

source
theorem q60596.algebra_map_not_injective  :
¬function.injective ⇑(algebra_map q60596.k (clifford_algebra q60596.Q))

Our final result

source
theorem clifford_algebra.not_forall_algebra_map_injective  :
¬∀ (R : Type) (M : Type v) [_inst_1 : comm_ring R] [_inst_2 : add_comm_group M] [_inst_3 : module R M] (Q : quadratic_form R M), function.injective ⇑(algebra_map R (clifford_algebra Q))