Infinite magmas?

Stream: Equational

[Kim Morrison]

Do we have examples of relations X and Y, such that all finite magmas satisfying X also satisfy Y, but some infinite magma satisfies X but not Y? Is that possible?

(I guess the follow up is given X and Y, can one ever show that X=>Y is detected by magmas of some size c(X,Y)?)

[Kim Morrison]

Ooops, I see this has been addressed elsewhere.

[Kevin Buzzard]

The paper in that thread was behind a firewall and apparently about groupoids (I'm not sure if a groupoid there is what I think a groupoid is) and as far as I'm concerned your question is very interesting!

[Daniel Weber]

If I understand the paper correctly a groupoid there is a magma, and the relation (((y ∘ y) ∘ y) ∘ x) ∘ ((y ∘ y) ∘ z) = x has no finite nontrivial model, but there's a fair chance I'm misreading it

[Daniel Weber]

I'll try to formalize it

[Daniel Weber]

I formalized one direction, but when trying to use the Magma typeclass it collides with Mathlib's function composition

import Mathlib.Data.Fintype.Card

example (α : Type*) [Mul α] [Nontrivial α]
    (h : ∀ (x y z : α), (y * y * y * x) * (y * y * z) = x) : Infinite α := by
  by_contra! nh
  rw [not_infinite_iff_finite] at nh
  have : ∀ (y z u : α), y * y * z = y * y * u := by
    intro y
    let f (x : α) := y * y * y * x
    let g (x : α) := x * (y * y * y)
    have : Function.RightInverse f g := by
      intro x
      simp [f, g, h]
    intro z u
    apply this.injective
    obtain ⟨finv, hf⟩ : f.HasRightInverse :=
      (Finite.surjective_of_injective this.injective).hasRightInverse
    let fy := finv (y * y * y)
    replace hf : y * y * y * fy = y * y * y := hf (y * y * y)
    have := h fy y
    simp only [hf] at this
    simp [f, this]
  obtain ⟨x, u, hxy⟩ := Nontrivial.exists_pair_ne (α := α)
  apply hxy
  have y := x
  have z := x
  rw [← h x y z, this y y (y * y), this (y * y) x u, ← this y y (y * y), h]

[Daniel Weber]

Here's the other direction, so I think I understood it correctly

example : ∃ (α : Type) (_ : Mul α) (_ : Nontrivial α),
    ∀ (x y z : α), (y * y * y * x) * (y * y * z) = x := by
  use ℕ+
  letI : Mul ℕ+ := { mul := fun a b ↦ if a = b then 2^a.val else
    if a = 1 then 3^b.val else
    if a = 3 ^ (padicValNat 3 a) then Nat.toPNat' (padicValNat 3 a) else 1}
  use this, ⟨1, 2, nofun⟩
  intro x y z
  unfold HMul.hMul instHMul Mul.mul
  simp only [↓reduceIte, PNat.pow_coe, PNat.val_ofNat]
  have t1 (y : ℕ+) : 2 ^ (y : ℕ) ≠ y := by
    apply_fun PNat.val
    simp only [PNat.pow_coe, PNat.val_ofNat, ne_eq]
    apply ne_of_gt
    apply Nat.lt_pow_self
    decide
  have t3 (y : ℕ+) (n : ℕ) : (2 : ℕ+) ^ (y : ℕ) ≠ 3^n := by
    apply_fun PNat.val
    simp only [PNat.pow_coe, PNat.val_ofNat, ne_eq]
    intro nh
    apply eq_of_prime_pow_eq at nh
    · contradiction
    · exact Nat.prime_two.prime
    · exact Nat.prime_three.prime
    · simp
  have t2 (y : ℕ+) : (2 : ℕ+) ^ (y : ℕ) ≠ 1 := t3 y 0
  have t4 (y : ℕ+) (n : ℕ) : (3 : ℕ+) ^ (y : ℕ) ≠ 2^n := by
    apply_fun PNat.val
    simp only [PNat.pow_coe, PNat.val_ofNat, ne_eq]
    intro nh
    apply eq_of_prime_pow_eq at nh
    · contradiction
    · exact Nat.prime_three.prime
    · exact Nat.prime_two.prime
    · simp
  have : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  have : Fact (Nat.Prime 3) := ⟨Nat.prime_three⟩
  simp only [t1, ↓reduceIte, t2, t3, PNat.val_ofNat, pow_one]
  by_cases hx : x = 1
  · simp only [hx, ↓reduceIte, PNat.val_ofNat, PNat.ofNat_inj, OfNat.ofNat_ne_one, ne_eq,
    Nat.succ_ne_self, not_false_eq_true, padicValNat_primes, pow_zero, ite_eq_else]
    intro nh
    split_ifs at nh
    · absurd nh
      apply ne_of_lt
      simp only [← PNat.coe_lt_coe, PNat.val_ofNat, PNat.pow_coe]
      apply lt_self_pow (by simp)
      apply one_lt_pow (by simp) (by simp)
    · contradiction
  simp only [Ne.symm hx, ↓reduceIte, PNat.pow_coe, PNat.val_ofNat, padicValNat.prime_pow,
    PNat.coe_toPNat']
  rw [if_neg, if_neg]
  · simp [pow_eq_one_iff]
  · split
    · apply t4
    · convert t4 _ 0

[Terence Tao]

Feel free to PR this (perhaps in a subfolder of the project)!

[Michael Stoll]

Daniel Weber said:

it collides with Mathlib's function composition

Maybe it would make sense to not use ∘, but use instead an otherwise unused (i.e., not used in a global notation in Mathlib) symbol?

[Oliver Nash]

Shouldn’t we just use docs#Mul i.e., *

[Terence Tao]

Oliver Nash said:

Shouldn’t we just use docs#Mul i.e., *

I did this initially but ran into problems https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Syntax/near/472959874

I guess we could change the operation symbol to something rarely used in mathlib if this sort of collision us going to be frequent, but i would imagine this to be rare

[Oliver Nash]

I see. I think I would have been inclined to stick with * but solve the problem you mention by using a type synonym for such counterexamples. In any case, it doesn't seem like this issue is especially pressing, so the best action here is probably no action.

[Terence Tao]

I have a slight preference against using * or + because of their connotations; I expect a * operation to be associative by default, and I expect a + operation to be both associative and commutative by default, whereas most of the magmas we would consider in this project are neither.

[Oliver Nash]

Yep, these psychological aspects definitely matter. OK forget about *!

[Daniel Weber]

Michael Stoll said:

Daniel Weber said:

it collides with Mathlib's function composition

Maybe it would make sense to not use ∘, but use instead an otherwise unused (i.e., not used in a global notation in Mathlib) symbol?

Perhaps •, then? Although it still has the existing instances problem

[Daniel Weber]

An interesting option is to use [CoeFun α (fun _ ↦ α → α)], and then we could use juxtapositioning

[Daniel Weber]

Although that'll probably need a custom delaborator, I see it doesn't look great in the infoview

@[app_unexpander CoeFun.coe]
def unexpCoeFunCoe : Unexpander
  | `($_ $arg) => `($arg)
  | _ => throw ()

works fairly well, though it adds spurious parentheses (although perhaps those are better without associativity)

[Terence Tao]

It seems the universal algebra literature often does use juxtaposition notation, as well as squaring notation x²=x ∘ x. I find the juxtaposition notation slightly harder to read (and also suggests associativity to me, though perhaps this can be unlearnt), but that is just my personal taste. (I'd be happy with squaring though.) Would be interesting to hear from any professional universal algebraists for their opinion on this.

[Terence Tao]

I added human-readable versions of these proofs to the blueprint (will appear at https://teorth.github.io/equational_theories/blueprint/sect0001.html shortly). Again, please feel free to PR a proof as a separate Lean file (and, if you are able, link it to the blueprint, though I can also do this manually).

[Daniel Weber]

I can't PR it currently because of the notation collision

[Daniel Weber]

$y^2 \circ z = 1$ isn't always true, it's possible that $z = y^2$

[Terence Tao]

I'm surprised there is a collision because α (or `ℕ+) shouldn't have a native ∘ operation

[Daniel Weber]

Ah, the problem is that I used the left-associativity, if I add more parentheses it works

[Terence Tao]

Daniel Weber said:

$y^2 \circ z = 1$ isn't always true, it's possible that $z = y^2$

Oops, good catch. I posted a fix

[Daniel Weber]

equational#58

[Terence Tao]

This PR brings up a future issue to discuss. This particular PR introduces a new equational law, currently called EquationKis, which is not on our list of 4694 equations (it involves six operations, not just four). But it has some external interest, being an example in the literature of an equation that is only satisfied by infinite magmas. It seems reasonable that we may selectively expand our list of equations under study from beyond the initial 4694, for instance to include other equations that have already been studied in the literature. How should we structure our file system etc. to be able to accommodate adding new equations without breaking any automated organizational tools? Perhaps we can allow Equations.lean to also include equations numbering from 4695 onwards (so, for instance, EquationKis would be placed here as Equation4695), and our automated tools would be smart enough to not hardcode the total number of equations as 4694, but infer that number from the two files Equations.lean and AllEquations.lean. Does anyone see any issues with this approach?

I can see, by the way, the Subgraph project gradually expanding to incorporate selected equations of interest, of which EquationKis seems like a prime candidate.

[Joachim Breitner]

Sounds reasonable.

It might be useful to have a non-lean file equations.txt in an easy to parse format, e.g.

1: x = x
2: x = y

and maintain that as the authoritative list and numbering of equations. I expect we will have non-lean scripts and tools that want that data and for which the lean file is not convenient to read.

With that we can even change AllEquations.lean to a little meta program that reads this file and creates definitions for all equations not already defined in Equations.lean, and check the statement for those defined there. I can do that part, should we want it.

[Terence Tao]

It occurs to me that a future research project (perhaps to be pursued after the primary aims of this project are completed) is to determine if the Kisielewicz example is minimal, that is to say whether one could find an equation involving only five or fewer operations that has only infinite non-trivial models.

[Terence Tao]

Sounds good to me. I'll create an issue for this.

[Terence Tao]

equational#64

[Ben Eltschig]

With the current naming scheme, EquationKis would be equation 374794 by the way - it might make sense to stick with that, as long as the numbers don't get too large? I don't know how large the equations of interest could really get, but at least for 6 operations the length of the list is still less than a million

[Ben Eltschig]

I'm not advocating for adding hundrets of thousands of equations to the list of course - I'm just saying, it might make sense to declare the equation as 374794: ..., even if that ends up being line 4695 in equations.txt :)

[Edward van de Meent]

by the way, what is the naming scheme? i haven't been able to make sense of it (yet). is it documented somewhere?

[Daniel Weber]

I think it's just the order produced by https://github.com/teorth/equational_theories/blob/main/scripts/generate_eqs_list.py ?

[Amir Livne Bar-on]

To be more explicit: The list is sorted by the total number of operations, then by the number of operations on the LHS. Within each such class we define an order on expressions by variable < operation, and lexical order on variables.

[Amir Livne Bar-on]

Further out from the way, the number of equations of each # of operations doesn't appear in OEIS

[Terence Tao]

I've put in a new task for a tool equational#79 that can take a magma equation and return its equation number (this may require first putting the equation in "normal form", i.e., shorter equation on the left, and variables relabeled in increasing order). A related request equational#72 is for a tool that can take an equation number and return its dual. Once we have such a tool I'd be happy to replace EquationKis with the number returned by that tool, though this means that any automated implication management software will have to allow for the possibility that the set of equations studied is not numbered consecutively.

[Terence Tao]

Adding another task equational#80 to compute the number of equations for each # of operations and then submit to OEIS :)

[Peter Jipsen]

This is an interesting project. Note that Kisielewicz showed in a 1997 follow-up paper that (((yy)y)x)(yz) = x is a shortest Austin identity (i.e. an identity that holds in some nontrivial magma, but any such magma must be infinite): Algebra Universalis 38 (1997) 324–328.

[Leo Shine]

Do we know infinite magmas are unnecessary for the current project? I can't see why knowing that you need 5 operations to ensure any non trivial magma is infinite means that there aren't 2 max 4 operation laws where one implies the other for finite magmas but not for infinite magmas

[Terence Tao]

I think this is open, and potentially a research question that could be answered by our project. That is: does there exist X, Y \leq 4694 such that the claim EquationX G \and \neg EquationY G is satisfied for some infinite G, but for no finite G? Currently this is only answered (in the negative) for Y=2.

to put it another way: is the finite magma brute force search sufficient in principle to determine the implication graph in (possibly galactic) finite time?

[Bhavik Mehta]

This doesn't answer the question but it may still be interesting - Equation168 G \and \neg (G has an idempotent) is true for some infinite G and false for every finite G

[Bhavik Mehta]

Ah actually I think I can improve that slightly with X=168 and Y=157 ((xy)(xy) = xy) to show that the claim is satisfied for some infinite G, but the only finite model is subsingleton:

• 157 is not equivalent to 2, it has a model in Bool with x*y = true
• There is an infinite G satisfying 168 with no idempotents, but 157 implies the existence of an idempotent in any nonempty magma, thus this G fails to satisfy 157
• Any finite G satisfying 168 must have n^2 elements and n idempotents. But if 157 is satisfied then xx=(xx)(xx)=x, so every element is idempotent, thus n^2=n

edit: this doesn't work in the way I thought it would, never mind

[Terence Tao]

Nevertheless focusing on central groupoids 168 as a hypothesis sounds promising. Perhaps one subproject is to completely determine which of the 4692 laws are implied by 168?