Nontrivial algebras

Stream: new members

[Richard Copley]

[Edit: rewrite] What is the classy proof of this example? (Is there an NeZero (1) instance for the algebra?)

import Mathlib.Data.Real.Basic
import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

open ExteriorAlgebra

variable (V : Type*) [AddCommGroup V] [Module ℝ V]

example : (1 : ExteriorAlgebra ℝ V) ≠ 0 := by
  let f := algebraMap ℝ (ExteriorAlgebra ℝ V)
  intro h
  rw [← RingHom.map_one f, ← RingHom.map_zero f, algebraMap_inj] at h
  exact one_ne_zero h

[Damiano Testa]

Maybe Nontrivial?

[Eric Rodriguez]

@loogle Nontrivial, ExteriorAlgebra

[loogle]

:search: ExteriorAlgebra.ι_ne_one

[Eric Rodriguez]

I'm now confused about the maths going on here [why are iota and algebraMap completely different?) but I think it's totally fine to put a Nontrivial instance on ExteriorAlgebra depending on R being nontrivial, which should give this result for free? Or maybe it needs to be a lemma, as R isn't an outparam based on V....

[Eric Rodriguez]

It could be added for R/C explicitly, of course

[Richard Copley]

CliffordAlgebra.ι is from the module (V), Algebra.algebraMap from the base ring (ℝ)

[Eric Wieser]

I thought I added this result...

[Eric Wieser]

It should be trivial from docs#ExteriorAlgebra.algebraMap_leftInverse

[Eric Wieser]

.injective.nontrivial should do it

[Richard Copley]

Is there something broken with casting? Shouldn't the following work, by Algebra.cast?

#check ((1 : ℝ) : ExteriorAlgebra ℝ V)
-- type mismatch
--   1
-- has type
--   ℝ : Type
-- but is expected to have type
--   ExteriorAlgebra ℝ V : Type u_1

[Eric Wieser]

I think Eric is confused, this would be fine as an instance (please PR it!)

[Eric Wieser]

I thought we eliminated docs#Algebra.cast during porting

[Eric Wieser]

Ah, we just de-instanced it

[Eric Wieser]

The correct spelling is unfortunately the rather clunky algebraMap _ _ (1 : ℝ)

[Richard Copley]

Eric Wieser said:

I think Eric is confused, this would be fine as an instance (please PR it!)

instance (V : Type*) [AddCommGroup V] [CommRing R] [Module R V]
: NeZero (1 : ExteriorAlgebra R V) := sorry

?

[Richard Copley]

No,

instance (V : Type*) [AddCommGroup V] [CommRing R] [Nontrivial R] [Module R V] :
  Nontrivial (ExteriorAlgebra R V) := sorry

[Eric Rodriguez]

Eric Wieser said:

I think Eric is confused, this would be fine as an instance (please PR it!)

ah, as R and V are explicit in the definition of exterior algebra... clearly low on the awakeness part :)

[Eric Rodriguez]

Richard Copley said:

Eric Wieser said:

I think Eric is confused, this would be fine as an instance (please PR it!)

instance (V : Type*) [AddCommGroup V] [CommRing R] [Module R V]
: NeZero (1 : ExteriorAlgebra R V) := sorry

?

this will come from docs#NeZero.one

[Richard Copley]

Ugh, is this true in a CliffordAlgebra too? I'll think about that.

[Eric Wieser]

In characteristic not two, yes

[Eric Wieser]

(go via docs#CliffordAlgebra.equivExterior)

[Eric Wieser]

Or even more generally when you can write Q as B.toQuadraticForm (which would be easy to generalize to, but maybe isn't worth the awkwardness it creates)

[Eric Wieser]

You might find #6657 interesting

[Richard Copley]

Richard Copley said:

Ugh, is this true in a CliffordAlgebra too? I'll think about that.

@Eric Wieser, thank you for not letting me start thinking about that :sweat_smile:

[Richard Copley]

Eric Wieser said:

I think Eric is confused, this would be fine as an instance (please PR it!)

#7985

[Eric Wieser]

Thanks!

[Richard Copley]

Thank you for the help and encouragement. Works for me:

import Mathlib.Data.Real.Basic
import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

variable (V : Type*) [AddCommGroup V] [Module ℝ V]

example : (1 : ExteriorAlgebra ℝ V) ≠ 0 := by
  exact? says exact one_ne_zero

example (Q : QuadraticForm ℝ V) : (1 : CliffordAlgebra Q) ≠ 0 := by
  haveI : Invertible (2 : ℝ) := invertibleOfNonzero two_ne_zero
  exact? says exact one_ne_zero

[Eric Wieser]

Nice! I'd be curious to know what applications of docs#CliffordAlgebra you have in mind; especially since I might have some results in other branches that I could try to prioritize.

[Richard Copley]

It's a bit round-about. I want the inner product on the exterior algebra (which you will recall is defined in terms of the Gram determinant), so I can define the Hodge star operator, because I want the cross product on a real inner product space, because I want to check an old draft of a (fairly silly) argument about rotations in three-dimensional space. Low-brow stuff, ultimately, but I'd like to do it nicely.

I might one day try to get some of the theory of spinors clear in my mind, for which Clifford algebra will be needed. But I'm not about to start that soon.

[Eric Wieser]

I think the inner product on the exterior algebra is probably hiding in Mathlib.LinearAlgebra.CliffordAlgebra.Contraction somewhere

[Eric Wieser]

Note that we have docs#crossProduct already, but I assume you want to stay in general n-dimensional space as long as possible

[Richard Copley]

Yes, I saw that, thanks. That and a few positively oriented orthonormal bases would almost certainly do everything I need. I suppose I just feel it's less expressive, and not as much fun.

[Heather Macbeth]

Richard Copley said:

I want the inner product on the exterior algebra (which you will recall is defined in terms of the Gram determinant), so I can define the Hodge star operator, because I want the cross product on a real inner product space,

@Richard Copley I did the cross product for the sphere eversion project but it didn't make it to mathlib yet. It is morally by the method you describe, although not literally. You can see the code (it's only ~100 lines) at
https://github.com/leanprover-community/sphere-eversion/blob/lean4/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean

[Richard Copley]

Lovely! I think that is all I need.

Under those appropriate hypotheses (for instance, if E is an oriented three-dimensional real inner product space), the map f=crossProduct taking u∈E to an element f(u)=(u × ·) of 𝔰𝔬(E) is not only an isomorphism of Lie algebras, but also an equivalence of representations from the standard representation id of the Lie algebra 𝔰𝔬(E)to the adjoint representation: f(f(u)v) = (ad_{f(u)})(f(v)) = f(u)f(v)-f(v)f(u) (the Jacobi identity).

Just wanted to get that off my chest :smile:

[Richard Copley]

(f(u×v)=[f(u),f(v)] is a nicer way to put it.)