unbundled v.s. (semi-)bundled

Stream: general

[Utensil Song]

The discussion originated here and moved here since the topic has drastically changed since the beginning.

We were struggling to determine the more suitable form of our definition in Lean and ran into issues like parameters v.s. variables (the latter should be preferred but we only got the parameters version working), unbundled v.s. (semi-)bundled and class v.s. structure.

The less relevant properties are stripped away for a simpler #mwe . Here's the simplified definition we call "mwc" (a dummy name):

Let R be a field and V a vector space over R, we define an algebra G over R equipped with the following homomorphisms:

1. fᵣ , a semiring homomorphism from R to G;
2. fᵥ, an additive monoid homomorphism from V to G.

Then we want to state some theorems using these two homs as simple as possible, at least the following one:

∀ v ∈ V, ∃ r : R,  (fᵥ v)^2 = fᵣ r

or better, just ∀ v ∈ V, ∃ r : R, (v)^2 = r if the homs can be inferred by lean through possibly coercion.

That's when we noticed the technical difficulty of referring to the homs in Lean. It's hard for us to refer to the homs by specifying the G equipping the algebra. parameters can help fixing the target G, but it only hides the problem and such a solution is not scalable, not preferred by mathlib and not portable to Lean 4.

[Utensil Song]

The following is the #mwe to express them in Lean in the unbundling form, bundling only V and bundling both R&V, all using variables.

import ring_theory.algebra

universes u₀ u₁ u₂

namespace unbundled

class mwc
(R : Type u₀) [field R]
(V : Type u₁) [add_comm_group V] [vector_space R V]
(G : Type u₂) [ring G]
extends algebra R G
:=
(fᵣ : R →+* G := algebra_map R G)
(fᵥ : V →+ G)

section lemmas

variables (R : Type u₀) [field R]
variables (V : Type u₁) [add_comm_group V] [vector_space R V]
variables (G : Type u₂) [ring G]

variables (r₀ : R)
variables (v₀ : V)

example [mwc R V G] : ∀ v : V, ∃ r : R,
  ((mwc.fᵥ R v) * (mwc.fᵥ R v)) = (mwc.fᵣ V r : G)
:= sorry

end lemmas

end unbundled

namespace V_bundled

class mwc
(R : Type u₀) [field R]
(G : Type u₂) [ring G]
extends algebra R G
:=
(V : Type u₁)
[V_acg : add_comm_group V]
[V_vs : vector_space R V]
(fᵣ : R →+* G := algebra_map R G)
(fᵥ : V →+ G)

section lemmas

variables (R : Type u₀) [field R]
variables (G : Type u₂) [ring G] [mwc R G]

variables (r₀ : R)
variables (v₀ : mwc.V R G)

example : ∀ v : mwc.V R G, ∃ r : R,
  (mwc.fᵥ v) * (mwc.fᵥ v) = mwc.fᵣ r
:= sorry

end lemmas

end V_bundled

namespace VR_bundled

class mwc
(G : Type u₂) [ring G]
:=
(R : Type u₀)
[R_f : field R]
(V : Type u₁)
[V_acg : add_comm_group V]
[V_vs : vector_space R V]
(to_algebra : algebra R G)
(fᵣ : R →+* G := algebra_map R G)
(fᵥ : V →+ G)

section lemmas

variables (G : Type u₂) [ring G] [mwc G]

variables (r₀ : mwc.R G)
variables (v₀ : mwc.V G)

example : ∀ v : mwc.V G, ∃ r : mwc.R G,
  (mwc.fᵥ v) * (mwc.fᵥ v) = mwc.fᵣ r
:= sorry

end lemmas

end VR_bundled

[Utensil Song]

In the unbundled verson, fᵣ has to know R, V and G, the parameter r : R will help it infer R, but Lean demands an extra V which is intuitively unrelated to fᵣ. And even with fᵣ V r, Lean still can't figure out what G is, so a further type ascription is needed, fᵥ has the similar problem, eventually ended up ugly as ((mwc.fᵥ R v) * (mwc.fᵥ R v)) = (mwc.fᵣ V r : G).

We want to get rid of mwc., type ascription :G and the extra type parameters R and V.

B.T.W. During the process, Lean's prompts for demanding the parameters are confusing, it's easy to see lots of ?Ms, ⁇ →+ ⁇, Type (max u₀ ? ?), has type ?m_1 →+ ?m_2 : Type (max ? ?) but is expected to have type Prop : Type, too many arguments if someone directly trying to express it under lemma, ∀ and ∃, fortunately, there's variables and #check to figure things out and port back to lemma and ∀ later.

[Utensil Song]

V_bundled seems to solve almost all the problems, it can be simplified to

example : ∀ v : mwc.V R G, ∃ r : R,
  (mwc.fᵥ v) * (mwc.fᵥ v) = mwc.fᵣ r
:= sorry

But there's still no way to refer to fᵥ as naturally as G.fᵥ, or V as G.V, we have to repeatedly face the problem that Lean doesn't the G equipped with the algebra we are talking about, and we have to tell which R, which V again and again, even in the different parts of the same lemma.

[Utensil Song]

VR_bundled seems to be going too far, where we mimic the inheritance by manually adding a data field called to_algebra for referring to R. The expression of the lemma is similarly simple.

[Utensil Song]

It's also worth noting that we used (fᵣ : R →+* G := algebra_map R G) in all these cases and this is only supported in a new structure. We don't know how to express the same if we need to change it back to the old structure.

[Utensil Song]

@Eric Wieser This is the discussion on bundling, have you looked at the commit yet? Have you managed to go further ?

[Utensil Song]

If we write

example {GA : mwc R G} : ∀ v : GA.V, ∃ r : R,
  (GA.fᵥ v) * (GA.fᵥ v) = GA.fᵣ r
:= sorry

in the namespace V_bundled, Lean is happy with GA.V, but complains about GA.fᵥ:

invalid field notation, function 'V_bundled.mwc.fᵥ' does not have explicit argument with type (V_bundled.mwc ...)

[Utensil Song]

This feels inconsistent

[Utensil Song]

R: Type u₀
_inst_1: field R
G: Type u₂
_inst_2: ring G
_inst_3: mwc R G
GA: mwc R G
v: mwc.V R G
r: R
⊢ mwc R G

The state is also wierd. Why demand mwc R G even when there's already GA: mwc R G?

[Utensil Song]

Literally, the reason is that(just look at the ()s ):

/-
mwc.V : Π (R : Type u_2) [_inst_1 : field R] (G : Type u_4) [_inst_2 : ring G] [c : mwc R G], Type u_3
-/
#check mwc.V

V expects explicit R and G, GA indirectly provided that, so Lean's happy.

/-
V_bundled.mwc.fᵥ : Π {R : Type u₀} [_inst_1 : field R] {G : Type u₂} [_inst_2 : ring G] [c : mwc R G], mwc.V R G →+ G

-/
#check mwc.fᵥ

mwc.fᵥ expects no explicit type arguments, because everything can be inferred from the only mwc.V argument which indirectly gives R and G.

Unlike mwc.fᵥ which eats a bundled V, GA.fᵣ eats an unbundled R, so a type ascription G for the output is needed:

/-
V_bundled.mwc.fᵣ : Π {R : Type u₀} [_inst_1 : field R] {G : Type u₂} [_inst_2 : ring G] [c : mwc R G], R →+* G
-/
#check mwc.fᵣ

example : ∀ v : mwc.V R G, ∃ r : R,
  mwc.fᵣ r = (mwc.fᵣ r : G)
:= sorry

[Kevin Buzzard]

If this is a question, it might get more attention if you made a mwe

[Scott Morrison]

I think @Utensil Song did post a #mwe above --- for me it was still a bit long, and I don't know the maths, so I haven't attempted to think about it.

[Utensil Song]

Yes, that was actually 3 #mwe in 3 namespaces. This is mostly a technical post because before thinking about this unbundled v.s. (semi-)bundled issue like in the mathlib/perfectoid papers, there're already many small but recurring technical issues to prevent a natural expression of the definitions I'm dealing with. Today's posts are self answering part of the questions asked in the main post.

[Utensil Song]

As for the confusing states here and here, I can't trigger them if I further minimalize the example.