feat(algebra/jordan/triple): Introduce Jordan triples

[mans0954]

Introduces Jordan triples and establishes some basic properties.

This is a sibling PR to #11073, which introduces Jordan rings. A subsequent PR will show that all Jordan rings also have a Jordan triple product. Conversely, every element a of a Jordan triple A induces a Jordan ring multiplication on A (the a-homotope).

---

[YaelDillies]

This is a pretty bad name! Isn't there anything more explicit in the literature?

[mans0954]

It's usually written $D(a,b)$ in LaTeX (occasionally $L(a,b)$ or $a \Box b$). Normally it isn't introduced with a name, I got the term "multiplication operator" from N.A. Altwaijry and C.M. Edwards, The Banach-Lie algebra of multiplication operators on a JBW∗ -triple. J. Funct. Anal. 254 (2008), 2866-2892.

[YaelDillies]

mul or mult would already be a better name. You can't just use a letter.

[mans0954]

Fully it's is_tp.D. If a symbol like +, * etc can represent a bilinear map, why not D?

[kbuzzard]

+ and * are notation; feel free to introduce D as local notation or an abbreviation. But the convention is that the name is descriptive.

[YaelDillies]

@kbuzzard, you say this, but we have algebraic_geometry.AffineScheme.Γ! I think that one is due a rename to .Gamma or something.

[alreadydone]

We also have polynomial.C, polynomial.X.

[YaelDillies]

etc... but we need to decide on the naming convention for the middle argument.

[mans0954]

etc... but we need to decide on the naming convention for the middle argument.

*_mid?

[mans0954]

etc... but we need to decide on the naming convention for the middle argument.

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Middle.20argument

Was a convention agreed for this?

[mans0954]

I've redefined the triple product along the lines discussed in #11575. I still haven't managed to redefine the Q operator along the lines @eric-wieser suggests.

[eric-wieser]

This is (or should be) add_monoid_hom.map_add₂

[mans0954]

I'm not sure there is a add_monoid_hom.map_add₂? Perhaps there should be? Did you mean linear_map.map_add₂?

mathlib/src/linear_algebra/bilinear_map.lean

Line 124 in e37daad

theorem map_add₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y :=

[mans0954]

@eric-wieser I guess the next step would be to define something like this:

class is_jordan_triple (R : Type u) [comm_ring R] (ρ : R →+* R)
(A : Type v) [add_comm_group A] [module R A]
  extends is_jordan_tp A :=
(triple_smul₁ : ∀ (r : R) (a b c : A), ⦃r•a, b, c⦄ = r • ⦃a, b, c⦄)
(triple_smul₂ : ∀ (r : R) (a b c : A), ⦃a, r•b, c⦄ = (ρ r) • ⦃a, b, c⦄)

But we then need to show that thetp is an instance of A →ₛₗ[ring_hom.id] A →ₛₗ[ρ] A →ₛₗ[ring_hom.id] A, and it's not immediately clear to me how to formulate that statement.

[mans0954]

Something along these lines, perhaps?

class is_jordan_triple (S : Type u) [comm_semiring S] [star_ring S]
(A : Type v) [add_comm_group A] [module S A]
  extends is_jordan_tp A :=
(triple_smul₁ : ∀ (s : S) (a b c : A), ⦃s•a, b, c⦄ = s • ⦃a, b, c⦄)
(triple_smul₂ : ∀ (s : S) (a b c : A), ⦃a, s•b, c⦄ = (star s) • ⦃a, b, c⦄)

variables (S : Type u) [comm_semiring S] [star_ring S]
variables {A : Type v} [add_comm_group A] [module S A]

def sesterlinear [is_jordan_triple S A] : A →ₗ[S] A →ₛₗ[star_ring_end S] A →ₗ[S] A := {
  to_fun := λ a, {
    to_fun := λ b, {
      to_fun := λ c, ⦃a, b, c⦄,
      map_add' := λ c₁ c₂, sorry,
      map_smul' := sorry,
    },
    map_add' := sorry,
    map_smul':= sorry,
  },
  map_add' := λ a₁ a₂, sorry,
  map_smul' := sorry,
}

[mans0954]

Trying something like this:

import algebra.lie.of_associative

universes u v

/-- An additive commutative monoid with a trilinear triple product -/
class has_triadditive_tp (A : Type*) [add_comm_group A] := (tp : A →+ A →+ A →+ A )

localized "notation ⦃a, b, c⦄ := has_triadditive_tp.tp a b c" in triple

class has_sesterlinear_tp (R : Type u) [comm_semiring R] [star_ring R] (A : Type*)
[add_comm_group A] [module R A] :=
(tp : A →ₗ[R] A →ₛₗ[star_ring_end R] A →ₗ[R] A )

instance : star_ring ℤ := star_ring_of_comm


lemma add_left {A : Type*} [add_comm_group A] [has_triadditive_tp A] (a₁ a₂ b c : A) :
  ⦃a₁ + a₂, b, c⦄ = ⦃a₁, b, c⦄ + ⦃a₂, b, c⦄ :=
by rw [map_add, add_monoid_hom.add_apply, add_monoid_hom.add_apply]

instance has_triadditive_tp_to_has_sesterlinear_tp {A : Type v} [add_comm_group A] 
[has_triadditive_tp A] :  has_sesterlinear_tp ℤ A := {
  tp := {
    to_fun := λ a, {
    to_fun := λ b, {
      to_fun := λ c, ⦃a, b, c⦄,
      map_add' := λ c₁ c₂, sorry,
      map_smul' := sorry,
    },
    map_add' := sorry,
    map_smul':= sorry,
  },
  map_add' := λ a₁ a₂, λ b, linear_map.ext (λ c, add_left a₁ a₂ b c)
  map_smul' := sorry,
  }
}

But it doesn't quite meet up in the middle

mvp.lean:33:28
type mismatch at application
  linear_map.ext (λ (c : A), add_left a₁ a₂ b c)
term
  λ (c : A), add_left a₁ a₂ b c
has type
  ∀ (c : A),
    ⇑(⇑(⇑has_triadditive_tp.tp (a₁ + a₂)) b) c =
      ⇑(⇑(⇑has_triadditive_tp.tp a₁) b) c + ⇑(⇑(⇑has_triadditive_tp.tp a₂) b) c
but is expected to have type
  ∀ (x : A), ⇑?m_10 x = ⇑?m_11 x

[mans0954]

There's a discrepancy here that my brain can't quite unpick at the moment. →+ is a add_monoid_hom, whereas →ₛₗ[star_ring_end R] is an instance of add_monoid_hom_class. So it is not quite right in lean to say that →ₛₗ[star_ring_end R] is an instance of →+ - which seems a bit unsatisfactory.

[YaelDillies]

That's the point of add_monoid_hom_class: you don't have to use add_monoid_hom to talk about additive monoid homs.

[mans0954]

So why is the definition of →+

infixr ` →+ `:25 := add_monoid_hom

and not

infixr ` →+ `:25 := add_monoid_hom_class

?

[YaelDillies]

add_monoid_hom A B is the type of additive monoid homomorphisms from A to B. add_monoid_hom_class F A B states that an already existing type F is a type of additive monoid homomorphisms from A to B. So for example add_monoid_hom is an add_monoid_hom_class, but so is add_equiv, ring_hom, continuous_add_monoid_hom...

Put another way, add_monoid_hom is here to be studied as an object on its own, by giving it an algebraic structure, an order, a topology... while add_monoid_hom_class is a way to talk about additive monoid homs individually.