Lie bracket on endomorphisms of addative commutative group

Stream: maths

[Christopher Hoskin]

I've spent most of the last 24 hours (mostly sleepless night) getting confused by the way the Lie bracket works in Lean. I'm trying to define the concept of a Jordan algebra and then work towards linearising the Jordan axiom. This is what I have so far:

import algebra.ring.basic
import algebra.lie.of_associative
import algebra.group.hom_instances

set_option old_structure_cmd true

variables α : Type*

/-- A not-necessarily-unital, not-necessarily-associative ring. -/
@[protect_proj, ancestor add_comm_group non_unital_non_assoc_semiring ]
class non_unital_non_assoc_ring (α : Type*) extends
  add_comm_group α, non_unital_non_assoc_semiring α

universe u

variables {A : Type u}
def L [has_mul A] (a : A) : A→A := λb, a * b
def R [has_mul A] (a : A) : A→A := λb, b * a

class jordan (A : Type*) [has_mul A] [has_pow (A → A) ℕ] :=
(commL1R1: ∀ a : A, (L a)∘(R a) = (R a)∘(L a) )
(commL1L2: ∀ a : A, (L a)∘(L a^2) = (L a^2)∘(L a) )
(commL1R2: ∀ a : A, (L a)∘(R a^2) = (R a^2)∘(L a) )
(commL2R1: ∀ a : A, (L a^2)∘(R a) = (R a)∘(L a^2) )
--(commL2R2: ∀ a : A, (L a^2)∘(R a^2) = (R a^2)∘(L a^2)) - This follows from commL1R1
(commR1R2: ∀ a : A, (R a)∘(R a^2) = (R a^2)∘(R a))

variables [has_pow (A → A) ℕ]

class comm_jordan (A : Type*) [has_mul A] [has_pow (A → A) ℕ] :=
(comm: ∀ a : A, L a = R a)
(jordan: ∀ a : A, (L a)∘(L a^2) = (L a^2)∘(L a))


-- A (commutative) Jordan multiplication is also a (non-)
instance comm_jordan_is_jordan [has_mul A] [comm_jordan A] : jordan A := {
  commL1R1 := λ _, by rw comm_jordan.comm,
  commL1L2 := λ _, by rw comm_jordan.jordan,
  commL1R2 := λ _, by rw [← comm_jordan.comm, comm_jordan.jordan],
  commL2R1 :=  λ _, by rw [← comm_jordan.comm, comm_jordan.jordan],
  commR1R2 := λ _, by rw [← comm_jordan.comm, comm_jordan.jordan],
}

variables [non_unital_non_assoc_ring A]

def T (a : A) : add_monoid.End A := {
  to_fun := λb, a * b,
  map_zero' := by rw mul_zero,
  map_add' := λ _ _, by rw mul_add,
}

variables [comm_jordan A]

lemma bra (E F : add_monoid.End A) : ⁅E,F⁆ = add_monoid_hom.comp E F - add_monoid_hom.comp F E := by exact rfl

lemma op_jordan (a : A) : ⁅T a, T a^2⁆ = 0 :=
begin
  rw bra,
  unfold add_monoid_hom.comp,
  rw comm_jordan.jordan, -- Goes wrong here
end

lemma mul_op_com1 (a b : A) : 2•⁅T a, T (a*b)⁆ + ⁅T a, T b^2⁆ + ⁅T b, T a^2⁆ + 2•⁅T b, T (a*b)⁆ = 0 := sorry

lemma lin_jordan (a b c : A) : 2•(⁅T a, T (b*c)⁆ + ⁅T b, T (a*c)⁆ + ⁅T c, T (a*b)⁆) = 0 := sorry

For a start, I'm not really sure what the difference between add_monoid.End A and A →+ A. They seem to be almost the same thing, ecept that lean understands the former as having a Lie bracket but not the latter.

Then I'm not sure if I should be defining:

def T (a : A) : add_monoid.End A := {
  to_fun := λb, a * b,
  map_zero' := by rw mul_zero,
  map_add' := λ _ _, by rw mul_add,
}

or whether it should be:

def T (a : A) : A → A := λb, a * b

and then somehow show that this is a add_monoid.End A.

lemma op_jordan comes a cropper because the statement is equivalent to:

{to_fun := ⇑(T a) ∘ ⇑(T a ^ 2), map_zero' := _, map_add' := _} - {to_fun := ⇑(T a ^ 2) ∘ ⇑(T a), map_zero' := _, map_add' := _}

And rewrite can't find the pattern L ?m_3 ∘ (L ?m_3 ^ 2).

Hope this makes some sort of sense?

Thanks,

Christopher

[Christopher Hoskin]

(Written in "normal maths" this is sections 2.4.3-4 on p31 of https://folk.ntnu.no/hanche/joa/joa-m.pdf)

[Eric Wieser]

add_monoid.End is just A →+ A with a monoid structure. The reason they're different is for monoid.End A vs A →* A, where the former has a compositional monoid structure and the latter a pointwise one

[Eric Wieser]

The additive one doesn't need to worry about that ambiguity, but I guess it was easier to be consistent

[Oliver Nash]

If you want some instant gratification, replace rw comm_jordan.jordan with simpa [sub_eq_zero].

[Oliver Nash]

However I think what you really need are a bunch of simp lemmas for the new definitions. Putting simps in front of several of your defs will be a good start.

[Eric Wieser]

Are you looking for docs#add_monoid_hom.mul?

[Eric Wieser]

Or the left and right variants linked from its docstring

[Oliver Nash]

Just to give the idea of a simp-type approach, if you replace the line def T (a : A) : add_monoid.End A := { with @[simps] def T (a : A) : add_monoid.End A := { then the following works:

-- Appears to be missing from Mathlib
@[simp] lemma add_monoid_hom.pow_apply
  {A : Type*} [add_monoid A] (f : add_monoid.End A) (n : ℕ) (a : A) :
  (f^n) a = (f^[n]) a :=
begin
  induction n with n ih,
  { refl, },
  { simp only [pow_succ, ih, function.comp_app, function.iterate_succ', add_monoid.coe_mul], },
end

lemma op_jordan (a : A) : ⁅T a, T a^2⁆ = 0 :=
begin
  ext b,
  simp [bra],
end

[Eric Wieser]

I think we have that first lemma in a file about iterate

[Eric Wieser]

We have docs#monoid_hom.coe_pow

[Eric Wieser]

Do we have docs#add_monoid_hom.coe_pow?

[Eric Wieser]

Added in #10886 as add_monoid.End.coe_pow

[Eric Wieser]

Maybe we should change the monoid structure on add_monoid_hom to make it a rfl lemma in a future PR.

[Christopher Hoskin]

Oops, I made the wrong assumption about the order of precedence. It should be T (a^2) not (T a)^2. Sorry. Thank you for adding add_monoid.End.coe_pow though, as I will need (T a)^2 in the future.

The absence of a unit now creates a problem, as non_unital_non_assoc_ring won't be an instance of [has_pow A ℕ] on account of a^0 not making sense. Is there a type of strictly positive natural numbers? I guess one could create a subtype of ℕ?

I now have:

import algebra.ring.basic
import algebra.lie.of_associative
import algebra.group.hom_instances
import algebra.iterate_hom

set_option old_structure_cmd true

variables α : Type*

/-- A not-necessarily-unital, not-necessarily-associative ring. -/
@[protect_proj, ancestor add_comm_group non_unital_non_assoc_semiring ]
class non_unital_non_assoc_ring (α : Type*) extends
  add_comm_group α, non_unital_non_assoc_semiring α

universe u

variables {A : Type u}
def L [has_mul A] (a : A) : A→A := λb, a * b
def R [has_mul A] (a : A) : A→A := λb, b * a

class jordan (A : Type*) [has_mul A] :=
(commL1R1: ∀ a : A, (L a)∘(R a) = (R a)∘(L a) )
(commL1L2: ∀ a : A, (L a)∘(L (a*a)) = (L (a*a))∘(L a) )
(commL1R2: ∀ a : A, (L a)∘(R (a*a)) = (R (a*a))∘(L a) )
(commL2R1: ∀ a : A, (L (a*a))∘(R a) = (R a)∘(L (a*a)) )
(commR1R2: ∀ a : A, (R a)∘(R (a*a)) = (R (a*a))∘(R a))

class comm_jordan (A : Type*) [has_mul A] :=
(comm: ∀ a : A, L a = R a)
(jordan: ∀ a : A, (L a)∘(L (a*a)) = (L (a*a))∘(L a))


-- A (commutative) Jordan multiplication is also a (non-)
instance comm_jordan_is_jordan [has_mul A] [comm_jordan A] : jordan A := {
  commL1R1 := λ _, by rw comm_jordan.comm,
  commL1L2 := λ _, by rw comm_jordan.jordan,
  commL1R2 := λ _, by rw [← comm_jordan.comm, comm_jordan.jordan],
  commL2R1 :=  λ _, by rw [← comm_jordan.comm, comm_jordan.jordan],
  commR1R2 := λ _, by rw [← comm_jordan.comm, ← comm_jordan.comm, comm_jordan.jordan],
}

variables [non_unital_non_assoc_ring A]

@[simps] def T (a : A) : add_monoid.End A := add_monoid_hom.mul_left a

variables [comm_jordan A]

lemma brackets (E F : add_monoid.End A) : ⁅E,F⁆ = add_monoid_hom.comp E F - add_monoid_hom.comp F E := by exact rfl

lemma op_jordan (a : A) : ⁅T a, T (a*a)⁆ = 0 := sorry

lemma mul_op_com1 (a b : A) : 2•⁅T a, T (a*b)⁆ + ⁅T a, T b^2⁆ + ⁅T b, T a^2⁆ + 2•⁅T b, T (a*b)⁆ = 0 := sorry

lemma lin_jordan (a b c : A) : 2•(⁅T a, T (b*c)⁆ + ⁅T b, T (a*c)⁆ + ⁅T c, T (a*b)⁆) = 0 := sorry

[Yakov Pechersky]

Yes, docs#pnat

[Christopher Hoskin]

@Oliver Nash Re. putting [simps] in front of the definitions, linting then fails with:

error: invalid import: geometry.manifold.algebra.monoid
invalid object declaration, environment already has an object named 'L_apply'

The documentation seems to imply that this name can be overridden with initialize_simps_projections, but the documentation is a bit hard to understand. I'm trying something like this:

set_option trace.simps.verbose true

initialize_simps_projections add_monoid_hom (apply → jordan as_prefix)

But it doesn't seem to have any affect:

lean --run scripts/lint_mathlib.lean
[simps] > Already found projection information for structure add_monoid_hom:
        > Projection apply: λ (M : Type u_7) (N : Type u_8) [_inst_1 : add_zero_class M] [_inst_2 : add_zero_class N], coe_fn
        > No lemmas are generated for the projections: map_zero', map_add'.
[simps] > Already found projection information for structure add_monoid_hom:
        > Projection apply: λ (M : Type u_7) (N : Type u_8) [_inst_1 : add_zero_class M] [_inst_2 : add_zero_class N], coe_fn
        > No lemmas are generated for the projections: map_zero', map_add'.
[simps] > adding projection L_apply:
        > ∀ {A : Type u_1} [_inst_1 : non_unital_non_assoc_ring A] (r : A), ⇑L r = add_monoid_hom.mul_left r
[simps] > Already found projection information for structure add_monoid_hom:
        > Projection apply: λ (M : Type u_7) (N : Type u_8) [_inst_1 : add_zero_class M] [_inst_2 : add_zero_class N], coe_fn
        > No lemmas are generated for the projections: map_zero', map_add'.
[simps] > adding projection R_apply:
        > ∀ {A : Type u_1} [_inst_1 : non_unital_non_assoc_ring A] (r : A), ⇑R r = add_monoid_hom.mul_right r
/home/mans0954/Documents/lean/mathlib_jordan-algebras/src/all.lean:3:0: error: invalid import: geometry.manifold.algebra.monoid
invalid object declaration, environment already has an object named 'L_apply'
/home/mans0954/Documents/lean/mathlib_jordan-algebras/scripts/lint_mathlib.lean:9:0: error: invalid import: geometry.manifold.algebra.monoid
invalid object declaration, environment already has an object named 'L_apply'
<unknown>:1:1: error: invalid object declaration, environment already has an object named 'L_apply'

What am I doing wrong?

Thanks,

Christopher

[Eric Wieser]

Can you give a full mwe?

[Christopher Hoskin]

In src/mwe.lean:

import algebra.group.hom_instances
import algebra.ring.basic

variables {A : Type*} [non_unital_non_assoc_semiring A]

@[simps] def L : A→+add_monoid.End A :=
{ to_fun := add_monoid_hom.mul_left,
  map_zero' := add_monoid_hom.ext $ zero_mul,
  map_add' := λ a b, add_monoid_hom.ext $ add_mul a b }

In src/all.lean:

import mwe
import geometry.manifold.algebra.monoid

Run lean --run scripts/lint_mathlib.lean:

/home/mans0954/Documents/lean/mathlib_jordan-algebras/src/all.lean:2:0: error: invalid import: geometry.manifold.algebra.monoid
invalid object declaration, environment already has an object named 'L_apply'
/home/mans0954/Documents/lean/mathlib_jordan-algebras/scripts/lint_mathlib.lean:9:0: error: invalid import: geometry.manifold.algebra.monoid
invalid object declaration, environment already has an object named 'L_apply'
<unknown>:1:1: error: invalid object declaration, environment already has an object named 'L_apply'

[Eric Wieser]

Does docs#L_apply already exist?

[Eric Wieser]

Yes, it does. I think it should probably be renamed.

[Eric Wieser]

Incidentally, that L is basically docs#module.to_add_monoid_End, but that one requires a unit and associativity

[Christopher Hoskin]

@Eric Wieser yes, the documentation seemed to imply that I could do something like this to rename the projection:

import algebra.group.hom_instances
import algebra.ring.basic

variables {A : Type*} [non_unital_non_assoc_semiring A]

initialize_simps_projections add_monoid_hom (apply → jordan as_prefix)

@[simps] def L : A→+add_monoid.End A :=
{ to_fun := add_monoid_hom.mul_left,
  map_zero' := add_monoid_hom.ext $ zero_mul,
  map_add' := λ a b, add_monoid_hom.ext $ add_mul a b }

But lean --run scripts/lint_mathlib.lean still fails:

[simps] > Already found projection information for structure add_monoid_hom:
        > Projection apply: λ (M : Type u_7) (N : Type u_8) [_inst_1 : add_zero_class M] [_inst_2 : add_zero_class N], coe_fn
        > No lemmas are generated for the projections: map_zero', map_add'.
/home/mans0954/Documents/lean/mathlib_jordan-algebras/src/all.lean:2:0: error: invalid import: geometry.manifold.algebra.monoid
invalid object declaration, environment already has an object named 'L_apply'
/home/mans0954/Documents/lean/mathlib_jordan-algebras/scripts/lint_mathlib.lean:9:0: error: invalid import: geometry.manifold.algebra.monoid
invalid object declaration, environment already has an object named 'L_apply'
<unknown>:1:1: error: invalid object declaration, environment already has an object named 'L_apply'

[Eric Wieser]

You don't want to do that

[Eric Wieser]

What I meant was that the existing L_apply should be renamed

[Eric Wieser]

Alternatively, work in a namespace of your own

[Eric Wieser]

L is an awfully short name to claim globally