Zulip Chat Archive
Stream: new members
Topic: synthesized not defeq inferred
Utensil Song (Jun 05 2020 at 15:23):
Hi, I have encountered the following error and I can't figure out why, any help would be greatly appreciated:
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
ring.to_semiring
inferred
comm_semiring.to_semiring ↥K
#mwe is
import tactic.ring_exp ring_theory.algebra algebra.opposites algebra.commute data.equiv.ring
import linear_algebra.quadratic_form
import data.real.basic
import data.complex.basic
class geometric_algebra (G : Type*) (K : set G) (V : set G)
[field K]
[add_comm_group V] [vector_space K V]  [Q : quadratic_form K V]
[ring G]
[is_subring K]
[is_subring V]
extends algebra K G
:=
(inner_product : quadratic_form K V)
The background is that I need K ⊆ G and V ⊆ G and they need to share the same +, * and follow the same basic arithmetic rules.
Reference: https://en.wikipedia.org/wiki/Geometric_algebra
Jeremy Avigad (Jun 05 2020 at 16:36):
I get a different error message, but the problem seems to be the [is_subring K]
. Lean can infer that K
is a ring from [field K]
. Below, when I ask Lean to print everything and I give it the instance explicitly, it complains that it is trying to match the two different ring instance for K
and failing. Why do you need [is_subring K]
? If I comment it out, the definition works for me.
import tactic.ring_exp ring_theory.algebra algebra.opposites algebra.commute data.equiv.ring
import linear_algebra.quadratic_form
import data.real.basic
import data.complex.basic
set_option pp.all true
class geometric_algebra (G : Type*) (K : set G) (V : set G)
[field K]
[add_comm_group V] [h : vector_space K V]  [Q : quadratic_form K V]
[ring G]
[is_subring K]
[is_subring V]
extends algebra K G
:=
(inner_product : quadratic_form K V _ _ h)
Utensil Song (Jun 05 2020 at 16:43):
I need it because there's another property I need that is \forall v : V, v*v \in K
Utensil Song (Jun 05 2020 at 16:45):
I can tell the direct cause from the error massage but don't know if it's a limitation of Lean or I'm puting the assumption at the wrong location
Utensil Song (Jun 05 2020 at 16:46):
Three places to choose from: [] before extends, after extends, after :=
Utensil Song (Jun 05 2020 at 16:51):
By limitation I mean whether one type can be subsomething and something++ and Lean knows the duplication of specifying something is acceptable
Jeremy Avigad (Jun 05 2020 at 16:52):
If I understand correctly, what is happening is that you are giving K
two different (and possibly entirely unrelated) ring structures. I don't think the type classes are set up to do exactly what you want. Hmm.....
Utensil Song (Jun 05 2020 at 16:54):
Yes, I guess that's the root cause and I need to try doing it in another way.
Jeremy Avigad (Jun 05 2020 at 16:55):
I think you need to define a special structure for is_subfield K
, write down the axioms that describe that, and then show is_subring K
and field K
both follow.
Utensil Song (Jun 05 2020 at 16:56):
but G is not a field...
Jeremy Avigad (Jun 05 2020 at 16:56):
(Where is_subfield K
says, roughly, that K
is equipped with a division that makes it both a field and a subring of the bigger ring. Maybe there is a better name for that, like is_field_as_subring K
.)
Utensil Song (Jun 05 2020 at 16:57):
I see, that seems ok
Utensil Song (Jun 05 2020 at 16:58):
I'll try that, thanks!
Johan Commelin (Jun 05 2020 at 16:59):
@Utensil Song In practice it seems to be better in the long run to work with injective structure preserving functions rather than set G
Johan Commelin (Jun 05 2020 at 16:59):
(In the perfectoid project we had the definition of a Huber pair, which is a ring A
and a subring A^+
...
Johan Commelin (Jun 05 2020 at 17:00):
And after a while we realised that we couldn't prove that Z_p, Q_p
was an example.
Johan Commelin (Jun 05 2020 at 17:00):
Because in lean, Z_p
is not a subring of Q_p
, even though there is a injective ring homomorphism.
Johan Commelin (Jun 05 2020 at 17:01):
So then we changed the definition, to use an injective ring hom (or algebra), and most proofs stayed the same, some became shorter.
Johan Commelin (Jun 05 2020 at 17:01):
In general it was just a lot more pleasant to work with.
Utensil Song (Jun 05 2020 at 17:01):
That's because I just found out how to write is_subring A B
(not Lean) from Zulip chat history
Utensil Song (Jun 05 2020 at 17:03):
broken into A : set B
and is_subring A
...
Utensil Song (Jun 05 2020 at 17:06):
strictly speaking, in my case, K is indeed not a subring of G
Utensil Song (Jun 05 2020 at 17:06):
the hom approach is more accurate
Utensil Song (Jun 07 2020 at 14:40):
Johan Commelin said:
So then we changed the definition, to use an injective ring hom (or algebra), and most proofs stayed the same, some became shorter.
The PR seems to be https://github.com/leanprovercommunity/leanperfectoidspaces/pull/56 and particular this commit.
The related code are:
class algebra (R : Type u) (A : Type v) [comm_semiring R] [semiring A]
extends has_scalar R A, R →+* A :=
(commutes' : ∀ r x, to_fun r * x = x * to_fun r)
(smul_def' : ∀ r x, r • x = to_fun r * x)
/ Embedding `R →+* A` given by `algebra` structure. /
def algebra_map (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] : R →+* A :=
algebra.to_ring_hom
structure Huber_pair :=
(plus : Type)
(carrier : Type)
[ring : comm_ring plus]
[top : topological_space plus]
[Huber : Huber_ring carrier]
[alg : algebra plus carrier]
(intel : is_ring_of_integral_elements plus carrier)
local postfix `⁺` : 66 := λ A : Huber_pair, A.plus
instance : comm_ring (A⁺) := A.ring
instance : topological_space (A⁺) := A.top
instance : Huber_ring A := A.Huber
instance : algebra (A⁺) A := A.alg
Utensil Song (Jun 07 2020 at 14:44):
From this example now I can see clearly why @Kevin Buzzard said that B : subring C
and algebra B C
are kind of the same in https://leanprover.zulipchat.com/#narrow/stream/116395maths/topic/algebra.20is.20not.20scaling.20for.20me/near/191348229 (found during searching for a proper solution for my issue here) .
Utensil Song (Jun 07 2020 at 14:49):
BTW, I don't know we can do []
after :=
too(I always wondered how we can reference the algebraic structure), only that it can be used before extends
, and we can do it between extends
and :=
without the []
.
Utensil Song (Jun 07 2020 at 14:56):
And how do we decide where to put []
(the type class arguments)? I'm very confused now. All three places seem to be legal, this seems to be just a mathematical design principle issue.
Kevin Buzzard (Jun 07 2020 at 14:59):
If you're talking about defining structures and classes, then []
after :=
means that you tell it the instance at the same time as you're making the structure. Before the :=
Lean will try to make the instance before you have even started making the structure
Utensil Song (Jun 07 2020 at 15:17):
Thanks, but what it means for the definition, mathematically?
Utensil Song (Jun 07 2020 at 15:17):
import tactic.ring_exp ring_theory.algebra algebra.opposites algebra.commute data.equiv.ring
import linear_algebra.quadratic_form
import data.real.basic
import data.complex.basic
class test :=
(K : Type*)
(V : Type*)
[field : field K]
[group : add_comm_group V]
[space : vector_space K V]
#check test.mk ℝ ℝ  test.mk ℝ ℝ : test
noncomputable instance test_rr : test := {
K := ℝ,
V := ℝ
}
class test'
(K : Type*)
(V : Type*)
[field : field K]
[group : add_comm_group V]
[space : vector_space K V]
#check test' ℝ ℝ  test' ℝ ℝ : Type
instance test'_rr : test' ℝ ℝ := by sorry  by apply_instance  tactic.mk_instance failed to generate instance for
class test''
(K : Type*)
(V : Type*)
[field : field K]
[group : add_comm_group V]
extends vector_space K V  invalid 'structure' extends, 'vector_space' is not a structure
Utensil Song (Jun 07 2020 at 16:59):
Finally I got to my x of the #xy , here's a #mwe that's actually working :
import tactic.ring_exp ring_theory.algebra algebra.opposites algebra.commute data.equiv.ring
import linear_algebra.quadratic_form
import data.real.basic
import data.complex.basic
class geometric_algebra (G : Type*) (K : Type*) (V : Type*)
[field K] [has_lift K G]
[add_comm_group V] [vector_space K V] [has_lift V G]
[ring G]
:=
[assoc : ∀ (a b c : G), (a * b) * c = a * (b * c)]
[left_distrib : ∀ a b c : G, a * (b + c) = (a * b) + (a * c)]
[right_distrib : ∀ a b c : G, (a + b) * c = (a * c) + (b * c)]
(v_sq_in_k : ∀ v : V, ∃ k : K, (↑v : G) * (↑v : G) = (↑k : G))
namespace geometric_algebra
variables (G : Type*) (K : Type*) (V : Type*)
[field K] [has_lift K G]
[add_comm_group V] [vector_space K V] [has_lift V G]
[ring G]
variables (a b c : G) [GA : geometric_algebra G K V]
 the trivial case: prove ℝ is a GA
instance : has_lift ℝ ℝ := { lift := λ x, x }
noncomputable instance : geometric_algebra ℝ ℝ ℝ := {
assoc := (λ a b c, semigroup.mul_assoc a b c),
left_distrib := (λ a b c, distrib.left_distrib a b c),
right_distrib := (λ a b c, distrib.right_distrib a b c),
v_sq_in_k := begin
intro v,
use (↑v) * (↑v),
refl
end
}
end geometric_algebra
But I have 3 new questions:
Q1: How can I express that there should exist only one k? (by changing \in to \exist, I avoided the has_mem
issues but it seems not completely safe)
Q2: Why do I have to write an instance for has_lift ℝ ℝ
? Shouldn't it be automatically inferred?
Q3: Why can't assoc
, left_distrib
, right_distrib
be automatically inferred?
Johan Commelin (Jun 07 2020 at 17:25):
@Utensil Song You are requiring [ring G]
and afterwards you have axioms assoc
, left_distrib
, and right_distrib
. But those are already part of ring G
...
Did you mean something else?
Johan Commelin (Jun 07 2020 at 17:26):
Also, you are not asking for any compatibility of the field structure on K
and the ring structure on G
. Should the has_lift
respect multiplication and addition?
Utensil Song (Jun 07 2020 at 17:30):
Johan Commelin said:
Utensil Song You are requiring
[ring G]
and afterwards you have axiomsassoc
,left_distrib
, andright_distrib
. But those are already part ofring G
...
Did you mean something else?
I think that I might have done something redundant here, but what I was thinking is that G is a ring but geometric_algebra G K V isn't so I added these trivial properties and name them under geometric_algebra. This seems to be exactly why it can't be inferred.
Ignore Q3 then.
Utensil Song (Jun 07 2020 at 17:35):
Johan Commelin said:
Also, you are not asking for any compatibility of the field structure on
K
and the ring structure onG
. Should thehas_lift
respect multiplication and addition?
Yes, you're right, it should, I can add [algebra K G]
back, and everything still works.
I removed it for K since I can't do the same for V. [algebra V G]
requires V
to be [comm_semiring V]
but *
(geometric product) does not commute for vectors and it's not even a group since the multiplication is not closed, a vector times a vector becomes a bivector, it's in G, but not in V. But actually for K, [algebra V G]
is fine and so is the *
for K.
Patrick Massot (Jun 07 2020 at 17:44):
Kevin Buzzard said:
If you're talking about defining structures and classes, then
[]
after:=
means that you tell it the instance at the same time as you're making the structure. Before the:=
Lean will try to make the instance before you have even started making the structure
Either I don't understand this or Kevin is wrong here.
Kevin Buzzard (Jun 07 2020 at 17:49):
I can quite believe I'm wrong. I think Utensil Song knows exactly what they are talking about at this point though.
Utensil Song (Jun 07 2020 at 17:57):
~To answer Q1, it seems that I should take a closer look at~
/An Ralgebra A is integrally closed if every element of A that is integral over R is contained in
the image of the canonical map R → A. This algebra_map is required to be injective./
structure is_integrally_closed : Prop :=
(inj : injective (algebra_map A : R → A))
(closed : ∀ a : A, (is_integral R a) → a ∈ set.range (algebra_map A : R → A))
~from the Huber_pair PR.~
EDIT: doesn't help. The injection of the lift seems to be covered in [algebra K G]
, the uniqueness of k is another question.
Utensil Song (Jun 07 2020 at 18:00):
Kevin Buzzard said:
I can quite believe I'm wrong. I think Utensil Song knows exactly what they are talking about at this point though.
From the tests in https://leanprover.zulipchat.com/#narrow/stream/113489newmembers/topic/synthesized.20not.20defeq.20inferred/near/200028361 , I do know that they're very different, but still, the applicability of each choice is still an unsolved puzzle.
Kevin Buzzard (Jun 07 2020 at 18:01):
Lean is just letting you write what you mean.
Utensil Song (Jun 07 2020 at 18:09):
Indeed.
Kevin Buzzard (Jun 07 2020 at 18:34):
However sometimes there is more than one way to write what you mean...
Utensil Song (Jun 12 2020 at 05:42):
After updating Lean to 3.16.0 and mathlib to mathlib = {git = "https://github.com/leanprovercommunity/mathlib", rev = "593f731dd200fe74c218ff9886eb663d4a860dcd"}
using leanproject up
, Lean dies frequently for the following #mwe :
import algebra.group.hom
import ring_theory.algebra
import data.real.basic
import data.complex.basic
universes u u₀ u₁
class geometric_algebra (G : Type*)
 Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀] [has_zero G₀] [has_one G₀]
 Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
 Axiom 1: G is a ring with unit.
 The additive identity is called 0 and the multiplicative identity is called 1.
[ring G] [has_zero G] [has_one G]
 TODO: find better ways to map G₀ and G₁ to G
[has_coe G₀ G] [has_coe G₁ G]
[G₀ →+* G]
[G₁ →+ G]
[algebra G₀ G]
:=
 Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar : ∀ v : G₁, ∃ k : G₀, (v * v : G) = (k : G))
namespace geometric_algebra
section
variables (G : Type*)
 Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀] [has_zero G₀] [has_one G₀]
 Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
 Axiom 1: G is a ring with unit.
 The additive identity is called 0 and the multiplicative identity is called 1.
[ring G] [has_zero G] [has_one G]
 TODO: find better ways to map G₀ and G₁ to G
[has_coe G₀ G] [has_coe G₁ G]
[G₀ →+* G]
[G₁ →+ G]
[algebra G₀ G]
[GA : geometric_algebra G G₀ G₁]
end
end geometric_algebra
Utensil Song (Jun 12 2020 at 05:44):
After every restart of Lean, and opening only this #mwe in the editor, the orange bar shows up and does not disappear and then
image.png
Utensil Song (Jun 12 2020 at 05:45):
How can I get more trace log to debug this?
Mario Carneiro (Jun 12 2020 at 05:46):
I don't have any issues running this, although I get an error on the last line because [G₀ →+* G] [G₁ →+ G]
are not classes
Mario Carneiro (Jun 12 2020 at 05:47):
Usually, if you get something that kills lean straight away, it requires some C++ debugging
Mario Carneiro (Jun 12 2020 at 05:47):
because you don't have the opportunity to ask more info
Utensil Song (Jun 12 2020 at 05:52):
[G₀ →+* G] [G₁ →+ G] are not classes
Oh I see, type class algebra
extends them but it doesn't mean I can use them as type classes. But I can't extend them either since there would be duplicated to_fun
etc.
Mario Carneiro (Jun 12 2020 at 05:54):
you don't need to extend them
Utensil Song (Jun 12 2020 at 05:54):
I don't have any issues running this
I don't always have issues running this, but when I comment out some type classes and add some back, somehow it triggers Lean to be killed and it stays that way even after restart
Mario Carneiro (Jun 12 2020 at 05:54):
just have a field
Utensil Song (Jun 12 2020 at 05:54):
G1 is not a field by itself
Mario Carneiro (Jun 12 2020 at 05:55):
no, the function
Mario Carneiro (Jun 12 2020 at 05:55):
the two functions should be fields of the structure
Mario Carneiro (Jun 12 2020 at 05:55):
well probably not [G₀ →+* G]
since that one duplicates the function embedded in the algebra
Mario Carneiro (Jun 12 2020 at 05:56):
you should not ask for has_coe
instances either
Utensil Song (Jun 12 2020 at 05:57):
the intention was to comment out the has_coe
, algebra
lines
Utensil Song (Jun 12 2020 at 05:57):
Mario Carneiro: the two functions should be fields of the structure
I'll try that
Mario Carneiro (Jun 12 2020 at 06:00):
I think you want something like this:
class geometric_algebra (G : Type*)
 Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀]
 Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
 Axiom 1: G is a ring with unit.
[ring G]
[algebra G₀ G]
:=
(f₁ : G₁ →+ G)
 Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar : ∀ v : G₁, ∃ k : G₀, f₁ v * f₁ v = algebra_map _ _ k)
Utensil Song (Jun 12 2020 at 06:01):
import algebra.group.hom
import ring_theory.algebra
import data.real.basic
import data.complex.basic
universes u u₀ u₁
class geometric_algebra (G : Type*)
 Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀] [has_zero G₀] [has_one G₀]
 Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
 Axiom 1: G is a ring with unit.
 The additive identity is called 0 and the multiplicative identity is called 1.
[ring G] [has_zero G] [has_one G]
 TODO: find better ways to map G₀ and G₁ to G
 [has_coe G₀ G] [has_coe G₁ G]
 [G₀ →+* G]
 [algebra G₀ G]
:=
(scalar_hom : G₀ →+* G)
(vec_hom : G₁ →+ G)
 Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar : ∀ v : G₁, ∃ k : G₀, vec_hom(v) * vec_hom(v) = scalar_hom(k) )
Here's what I came up with
Mario Carneiro (Jun 12 2020 at 06:01):
you have a lot of duplicate data in the parameters
Utensil Song (Jun 12 2020 at 06:02):
Oh, algebra_map _ _ k
is the scalar_hom
equivalent
Mario Carneiro (Jun 12 2020 at 06:03):
those has_zero
and has_one
instances are also duplicate
Utensil Song (Jun 12 2020 at 06:03):
Mario Carneiro: you have a lot of duplicate data in the parameters
Yes, I'm trying to see the effect of doing so. Was expecting to get warnings about them.
Mario Carneiro (Jun 12 2020 at 06:03):
no, you will just get stuck in proofs
Mario Carneiro (Jun 12 2020 at 06:03):
I don't think lean knows what a warning is
Mario Carneiro (Jun 12 2020 at 06:05):
If you have any duplicate data, you are constructing something like "a field with two independent multiplications" or similar. Any theorem using one operation will not be able to play well with definitions based on the other
Utensil Song (Jun 12 2020 at 06:06):
Mario Carneiro: no, you will just get stuck in proofs
Oh, I got stuck somewhere else. Using has_coe
made me to prove ↑kab  ↑ka  ↑kb = ↑(kab  ka  kb)
which can't be proved unless I have a >+
.
Mario Carneiro (Jun 12 2020 at 06:06):
for example, with [field G₀] [has_one G₀]
you will not be able to prove 1 * x = x
Mario Carneiro (Jun 12 2020 at 06:06):
because nothing says that 1
is a unit
Utensil Song (Jun 12 2020 at 06:07):
Oh, I thought it's eliminated in the solution to the diamond problem.
Mario Carneiro (Jun 12 2020 at 06:07):
if they were fields it would be a different matter, but you are passing everything as parameters
Mario Carneiro (Jun 12 2020 at 06:08):
there is no way for lean to assert a relation on the inputs unless you provide such relation
Mario Carneiro (Jun 12 2020 at 06:10):
I notice that Axiom 2
and Axiom 3
make additional claims about closure. These need to be axioms inside the structure
Mario Carneiro (Jun 12 2020 at 06:10):
maybe they come for free given the homs
Utensil Song (Jun 12 2020 at 06:13):
Mario Carneiro: maybe they come for free given the homs
I believe so
Utensil Song (Jun 12 2020 at 14:47):
@Mario Carneiro I can't refer to f1 later though:
import ring_theory.algebra
class geometric_algebra (G : Type*)
 Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀]
 Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
 Axiom 1: G is a ring with unit.
[ring G]
[algebra G₀ G]
:=
(f₁ : G₁ →+ G)
 Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar : ∀ v : G₁, ∃ k : G₀, f₁ v * f₁ v = algebra_map _ _ k)
namespace geometric_algebra
section
variables (G : Type*)
 Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀]
 Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
 Axiom 1: G is a ring with unit.
[ring G]
[algebra G₀ G]
[GA : geometric_algebra G G₀ G₁]
def square (a : G) := a * a
def sym_prod (a b : G) := a * b + b * a
local infix `*₊`:75 := sym_prod
local postfix `²`:80 := square
#check f₁
/
Symmetrised product of two vectors must be a scalar
/
lemma vec_sym_prod_scalar_failed :
∀ (a b : G₁), ∃ k : G₀,
f₁ a *₊ f₁ b = algebra_map _ _ k := by sorry
 type mismatch at application
 f₁ a
 term
 a
 has type
 G₁ : Type u_3
 but is expected to have type
 Type ? : Type (?+1)
 Additional information:
 minimal.lean:43:2: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
 type mismatch, term
 f₁ ?m_2
 has type
 ?m_1 →+ ?m_2 : Type (max ? ?)
 but is expected to have type
 Type ? : Type (?+1)
lemma vec_sym_prod_scalar_still_failed :
∀ (a b : G₁), ∃ k : G₀,
(f₁ G₀ a) *₊ (f₁ G₀ b) = algebra_map _ _ k := by sorry
 failed to synthesize type class instance for
 G₀ : Type u_2,
 _inst_1 : field G₀,
 _inst_2 : char_zero G₀,
 G₁ : Type u_3,
 _inst_3 : add_comm_group G₁,
 _inst_4 : vector_space G₀ G₁,
 a b : G₁,
 k : G₀
 ⊢ ring (Type ?)
end
end geometric_algebra
And Lean dies randomly again...
Kevin Buzzard (Jun 12 2020 at 17:58):
I'm not able to reproduce this random dying thing. If you hover over the first error, namely f₁
, you see that it has this type:
geometric_algebra.f₁ : Π {G : Type u_1} (G₀ : Type u_2) [_inst_1 : field G₀] [_inst_2 : char_zero G₀] {G₁ : Type u_3} [_inst_3 : add_comm_group G₁] [_inst_4 : vector_space G₀ G₁] [_inst_5 : ring G] [_inst_6 : algebra G₀ G] [c : geometric_algebra G G₀ G₁], G₁ →+ G
In particular f₁ a
will not work because a
is supposed to be G₀
, the first ()
input to f₁
Kevin Buzzard (Jun 12 2020 at 18:00):
If you would like G₀
to be inferred by unification, then change (G₀ : Type*)
to {G₀ : Type*}
when you're setting up your variables.
Kevin Buzzard (Jun 12 2020 at 18:03):
Your second error is because when Lean sees f₁ G₀ a
it has to now guess all of the {}
variables for f₁
by unification, and it doesn't know how to guess G
, so it just uses a metavariable, and then it has to prove that this metavariable is a ring because of [ring G]
, so it gets stuck.
Kevin Buzzard (Jun 12 2020 at 18:07):
Next problem: sym_prod
expects an explicit G
(look at the type) so the *₊
notation won't work.
include GA  you named it, so it doesn't get included automatically
 and Lean cannot solve the problem you have left it regarding implicit variables so I
 told it the solution explicitly
lemma vec_sym_prod_scalar_typechecks :
∀ (a b : G₁), ∃ k : G₀,
sym_prod G (@f₁ G G₀ _ _ G₁ _ _ _ _ _ a) (@f₁ G G₀ _ _ G₁ _ _ _ _ _ b) = algebra_map _ _ k := by sorry
Kevin Buzzard (Jun 12 2020 at 18:09):
The problem is that if you're just telling f\_1
that it's going to eat a
, then it can figure out G\_1
, but it can't figure out G
or G\_0
because even though we have geometric_algebra G G₀ G₁
Lean thinks that maybe there could be some other instances geometric_algebra H H₀ G₁
so it will refuse to guess G and G_0 from what you told it.
Kevin Buzzard (Jun 12 2020 at 18:10):
One easy fix is to let f_1 also eat G and G_0. This sort of thing happens with algebras in Lean  if A is an Ralgebra then Lean never quite knows if A is an algebra for any other ring too, so many definitions and lemmas about Ralgebras ask for R explicitly.
Kevin Buzzard (Jun 12 2020 at 18:20):
You probably want to make G implicit in sym_prod
and to make G and G_0 explicit in f_1. Maybe this?
import ring_theory.algebra
class geometric_algebra (G : Type*)
 Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀]
 Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
 Axiom 1: G is a ring with unit.
[ring G]
[algebra G₀ G]
:=
(f₁' : G₁ →+ G)  I added a prime because the binders are wrong
 Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar : ∀ v : G₁, ∃ k : G₀, f₁' v * f₁' v = algebra_map _ _ k)
namespace geometric_algebra
#check @f₁'  G is implicit
 let's fix those binders
def f₁ (G : Type*)  explicit G
(G₀ : Type*) [field G₀] [char_zero G₀] {G₁ : Type*}
[add_comm_group G₁] [vector_space G₀ G₁] [ring G] [algebra G₀ G]
[geometric_algebra G G₀ G₁] : G₁ →+ G := @f₁' G G₀ _ _ G₁ _ _ _ _ _
section
variables {G : Type*}  make it implicit
 Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀]
 Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
 Axiom 1: G is a ring with unit.
[ring G]
[algebra G₀ G]
[geometric_algebra G G₀ G₁]  removing the name
def square (a : G) := a * a
 implicit G for sym_prod
def sym_prod (a b : G) := a * b + b * a
local infix `*₊`:75 := sym_prod
local postfix `²`:80 := square
 now back to explicit G
variable (G)
/
Symmetrised product of two vectors must be a scalar
/
lemma vec_sym_prod_scalar_typechecks :
∀ (a b : G₁), ∃ k : G₀,
(f₁ G G₀ a) *₊ (f₁ G G₀ b) = algebra_map _ _ k := by sorry
end
end geometric_algebra
Utensil Song (Jun 13 2020 at 03:54):
Thanks for your detailed explanations on how Lean works , here's the further #mwe to demonstrate what I need partially following your hints with many comments describing my motivation and goal here:
import algebra.group.hom
import ring_theory.algebra
import data.real.basic
import data.complex.basic
universes u u₀ u₁
class geometric_algebra
 Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀]
 Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
 Axiom 1: G is a ring with unit.
 The additive identity is called 0 and the multiplicative identity is called 1.
(G : Type*) [ring G] [algebra G₀ G]
:=
(f₁ : G₁ →+ G)
 Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar : ∀ v : G₁, ∃ k : G₀, f₁ v * f₁ v = algebra_map _ _ k )
namespace geometric_algebra
section
variables
{G₀ : Type*} [field G₀]
{G₁ : Type*} [add_comm_group G₁] [vector_space G₀ G₁]
{G : Type*} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G]
def square (a : G) := a * a
def sym_prod (a b : G) := a * b + b * a
local infix `*₊`:75 := sym_prod
local postfix `²`:80 := square
#check @f₁
 implicit G₀
def f₁' : G₁ →+ G := f₁ G₀
#check @f₁'
/
f₁' :
Π {G₀ : Type u_4} [_inst_1 : field G₀]
{G₁ : Type u_5} [_inst_2 : add_comm_group G₁] [_inst_3 : vector_space G₀ G₁]
{G : Type u_6} [_inst_4 : ring G] [_inst_5 : algebra G₀ G]
[_inst_6 : geometric_algebra G₀ G₁ G],
G₁ →+ G
/
/
Symmetrised product of two vectors must be a scalar
/
lemma vec_sym_prod_scalar_works_but_not_ideal :
∀ (a b : G₁), ∃ k : G₀,
f₁ G₀ a *₊ f₁ G₀ b = algebra_map G₀ G k := by sorry
/
OK, it seems Lean knows G₁ from a and b,
but requires explicit G₀ to know to which G f₁ belongs
/
lemma vec_sym_prod_scalar_works_inferred_as_much_as_possible :
∀ (a b : G₁), ∃ k : G₀,
f₁ G₀ a *₊ f₁ G₀ b = algebra_map _ G k := by sorry
/
The only thing can be inferred is the type of k from k
/
lemma vec_sym_prod_scalar_better_but_failed:
∀ (a b : G₁), ∃ k : G₀,
f₁' a *₊ f₁' b = algebra_map G₀ G k := by sorry
/
Here's why I "think" this should work:
 rhs fixed G₀ and G, a and b fixed G₁, Lean should know everything about f₁'
 plus *₊ fixed G too
Note that now I've made all parameters in f₁' implicit
/
lemma vec_sym_prod_scalar_ideal_but_seems_impossble_in_lean:
∀ (a b : G₁), ∃ k : G₀,
a *₊ b = k := by sorry
/
Here's why I further "think" this should work:
 a and b fixed G₁
 *₊ fixed G
 G₀ can be inferred from [geometric_algebra G₀ G₁ G]
Here's why I want it:
It's closer to how it's stated in literature, without the hassle of homs
and I have to state more complicated theoerem that involves more +*/exp
as in https://github.com/pygae/GAlgebra.jl/blob/master/test/runtests.jl#L321
Here's how I'm so close to it:
If I relax →+ and demand [has_coe G₀ G], then I get to state it like:
lemma vec_sym_prod_scalar [geometric_algebra G K V] :
∀ (a b : V), ∃ k : K, a *₊ b = (k : G) := by sorry
as in https://github.com/pygae/leanga/blob/master/src/geometric_algebra/nursery/basic.lean#L98
/
end
end geometric_algebra
Utensil Song (Jun 13 2020 at 04:14):
The crucial thing here is "even though we have geometric_algebra G G₀ G₁ Lean thinks that maybe there could be some other instances geometric_algebra H H₀ G₁ so it will refuse to guess G and G_0 from what you told it."
Utensil Song (Jun 13 2020 at 04:15):
Is there a way to force so, just locally?
Utensil Song (Jun 13 2020 at 04:16):
(sorry I change the order of G₀ G₁ G to make it in an ascendant order like in algebra)
Alex J. Best (Jun 13 2020 at 04:46):
The @ character can be used to tell lean you want to explicitly fill some implicit types in
lemma vec_sym_prod_scalar_better_but_failed:
∀ (a b : G₁), ∃ k : G₀,
(@f₁' G₀ _ _ _ _ _ _ _ _) a *₊ (@f₁' G₀ _ _ _ _ _ _ _ _) b = algebra_map G₀ G k := by sorry
I think your logic that the right hand side of this fixes G₀
doesn't really follow, the type of the RHS is G
and just because you used a particular G₀
doesn't mean the LHS has to use the same one.
P.s. the extra brackets I added aren't needed really.
Utensil Song (Jun 13 2020 at 04:47):
It seems that to achieve what I want, I have to redesign the whole thing from ground up.
Starting by giving G₁ a (not has_mul) multiplication that always return G but it's actually just G₀ or G₂, which in turn needs a grade projection operator first, and make G₁ not special and not in the parameters but generated from a projection. But in this case I'll have to use G > set G
as the type of the grade projection, which I have been trying to avoid, because I want G₀ and G₁ to be a real type and not a type to Prop. And then from there I'll need to redefine eq
as well, because eventually I'll need all 0 in G₀, G₁, G₂, ..., G etc. to equal and a G with only G₁ or G₂ components to equal to G₁ or G₂. I'll also need to state that G can be written as the infinite sum of G₀, G₁, G₂, ..., which might involve some cardinality stuff......
(This formalism is used in GA to GC by Hestenes and Sobczyk, I thought I could try something simpler first, but the simpler formalism seems to be making it more difficult in Lean)
(To make the discussion above easier to interpret, think G as another formalism to spell out Clifford Algebra (it seems to be not ready to be defined generally in mathlib yet as I've read on the Zulip, as well as Grassmann Algebra i.e. exterior algebra ).)
Utensil Song (Jun 13 2020 at 04:49):
Alex J. Best said:
I think your logic that the right hand side of this fixes
G₀
doesn't really follow, the type of the RHS isG
and just because you used a particularG₀
doesn't mean the LHS has to use the same one.
Yes, I can see that now, but I'm wondering whether it's possible to specify so somehow.
Alex J. Best (Jun 13 2020 at 04:53):
I haven't used it myself, but perhaps using parameters
instead of variables
in this file does what you want
Utensil Song (Jun 13 2020 at 05:05):
Oh silly me, I've confused them before and doing this again...Changing variables
to parameters
makes vec_sym_prod_scalar_better_but_failed
work as expected! Thanks!
Utensil Song (Jun 13 2020 at 16:43):
Is there anyway to simply use cc
after rw h1
, by making it somehow see through homs? It's painful to move terms around step by step...
begin
intros hb ha hab,
/
G₀ : Type u_1,
_inst_1 : field G₀,
G₁ : Type u_2,
_inst_2 : add_comm_group G₁,
_inst_3 : vector_space G₀ G₁,
G : Type u_3,
_inst_4 : ring G,
_inst_5 : algebra G₀ G,
_inst_6 : geometric_algebra G₀ G₁ G,
a b : G₁,
h1 : (a + b)²ᵥ = a²ᵥ + b²ᵥ + a*₊ᵥ b,
vec_sq_scalar : ∀ (v : G₁), ∃ (k : G₀), v²ᵥ = ⇑fₛ k,
kab ka kb : G₀,
hb : b²ᵥ = ⇑fₛ kb,
ha : a²ᵥ = ⇑fₛ ka,
hab : (a + b)²ᵥ = ⇑fₛ kab
⊢ ∃ (k : G₀), a*₊ᵥ b = ⇑fₛ k
/
rw [hb, ha, hab] at h1,
use (ka) + (kb) + kab,
 a*₊ᵥ b = ⇑fₛ (ka  kb + kab)
rw ring_hom.map_add,
rw h1,
 a*₊ᵥ b = ⇑fₛ (ka + kb) + (⇑fₛ ka + ⇑fₛ kb + a*₊ᵥ b)
rw ←add_assoc,
 a*₊ᵥ b = ⇑fₛ (ka + kb) + (⇑fₛ ka + ⇑fₛ kb) + a*₊ᵥ b
rw ←add_assoc,
 a*₊ᵥ b = ⇑fₛ (ka + kb) + ⇑fₛ ka + ⇑fₛ kb + a*₊ᵥ b
rw ←ring_hom.map_add,
 a*₊ᵥ b = ⇑fₛ (ka + kb + ka) + ⇑fₛ kb + a*₊ᵥ b
rw ←ring_hom.map_add,
 a*₊ᵥ b = ⇑fₛ (ka + kb + ka + kb) + a*₊ᵥ b
rw add_comm (ka) (kb),
 a*₊ᵥ b = ⇑fₛ (kb + ka + ka + kb) + a*₊ᵥ b
rw add_assoc (kb) (ka) ka,
 a*₊ᵥ b = ⇑fₛ (kb + (ka + ka) + kb) + a*₊ᵥ b
simp only [add_zero, ring_hom.map_zero, add_left_neg, zero_add],
end
(Full working code is too long to paste in here, it's at https://github.com/pygae/leanga/blob/1d589406ffbed0e00bafff18bf1466689ea8b4b8/src/geometric_algebra/nursery/chisolm.lean#L97 )
Kevin Buzzard (Jun 13 2020 at 17:51):
After use (ka) + (kb) + kab,
you can do simp [fₛ.map_add, h1]
, which immediately reduces your goal to
⊢ a*₊ᵥ b = ⇑fₛ ka + ⇑fₛ kb + (⇑fₛ ka + ⇑fₛ kb + a*₊ᵥ b)
and then the abel
tactic finishes the job.
rw [hb, ha, hab] at h1,
use (ka) + (kb) + kab,
 a*₊ᵥ b = ⇑fₛ (ka  kb + kab)
simp [fₛ.map_add, h1],
abel,
Eric Wieser (Jun 29 2020 at 16:23):
Alex J. Best said:
I haven't used it myself, but perhaps using
parameters
instead ofvariables
in this file does what you want
But parameters
is being removed in lean 4, right? So what should we do here instead?
Alex J. Best (Jun 29 2020 at 16:31):
Well if the problem you're trying to solve is, "I have a bunch of variables, and every def/lemma/theorem in the theory I'm writing takes all of them as input and I don't want to write them all the time (i.e. some ambient space / ring you are working in with some properties)" then I think the solution is to bundle everything you need into a structure that holds all these assumptions and use a single variable of type that structure and use that as input to every lemma etc.
Reid Barton (Jun 29 2020 at 16:31):
Or just don't worry about what Lean 4 may or may not do.
Eric Wieser (Jun 29 2020 at 16:35):
Well in this case I run into the same problem using variables
as I do trying to move my parameters to separate files
Alex J. Best (Jun 29 2020 at 16:36):
Can you give an example of what you mean?
Eric Wieser (Jun 29 2020 at 16:36):
I'm trying to
Eric Wieser (Jun 29 2020 at 16:40):
Here's a fairly minimal example:
import algebra.group.hom
import ring_theory.algebra
class geometric_algebra
(G₀ : Type*) [field G₀]
(G₁ : Type*) [add_comm_group G₁]
(G : Type*) [ring G]
:=
(f₁ : G₁ →+ G)
namespace geometric_algebra
section
/ doesn't work if `variables` instead /
parameters
{G₀ : Type*} [field G₀]
{G₁ : Type*} [add_comm_group G₁]
{G : Type*} [ring G] [geometric_algebra G₀ G₁ G]
def fᵥ : G₁ →+ G := f₁ G₀
def prod_vec (a b : G₁) : G := fᵥ a * fᵥ b
end
end geometric_algebra
As is, this has no errors.
If I change parameters
to variables
, then prod_vec
doesn't "know how to synthesize placeholder" at fᵥ
.
Eric Wieser (Jun 29 2020 at 16:41):
But I if leave it with parameters
, then I have the same problem attempting to use fᵥ
from another file.
Utensil Song (Jun 29 2020 at 16:43):
The problem from the beginning is that I put too many things in parameters, which should probably be bundled into the class.
Utensil Song (Jun 29 2020 at 16:46):
But still, I'm very confused about the subtle differences between parameters and variables and the idiomatic ways to use them.
Utensil Song (Jun 29 2020 at 16:47):
As demonstrated in the #mwe above
Johan Commelin (Jun 29 2020 at 16:47):
idiomatic in the sense of mathlib is "don't use parameters"
Johan Commelin (Jun 29 2020 at 16:47):
But I'm not a mathlib dictator!
Johan Commelin (Jun 29 2020 at 16:47):
So feel free to use them. I've just never used them myself.
Utensil Song (Jun 29 2020 at 16:48):
then how to use variables to achieve similar purpose?
Eric Wieser (Jun 29 2020 at 16:48):
I'm seeing the argument against using parameters
since I've been trying to split a section in two, but I can't work out an alternative spelling of the above without parameters
that doesn't need a gazillion _
placeholders
Utensil Song (Jun 29 2020 at 16:48):
I wish to avoid relying on something not recommended by mathlib
Bryan Ginge Chen (Jun 29 2020 at 16:50):
I think making G
implicit in fᵥ
is a bit strange. The issue is that when you write fᵥ a
, Lean can't tell what G
should be.
Eric Wieser (Jun 29 2020 at 16:51):
Changing to def fᵥ (G : Type*) : G₁ →+ G := f₁ G₀
in the example above results in an error at →+
Utensil Song (Jun 29 2020 at 16:51):
The end goal is even to remove the need of fv...
Utensil Song (Jun 29 2020 at 16:52):
since they're not in the original math
Utensil Song (Jun 29 2020 at 16:53):
the arithmetic just works across "types"
Eric Wieser (Jun 29 2020 at 16:54):
I'd still like to understand how to write the #mwe above, even if we don't end up needing it
Utensil Song (Jun 29 2020 at 16:54):
yeah
Bryan Ginge Chen (Jun 29 2020 at 17:08):
Oh, I was wrong. The issue wasn't with G
being implicit, but with G₀
:
import algebra.group.hom
import ring_theory.algebra
class geometric_algebra
(G₀ : Type*) [field G₀]
(G₁ : Type*) [add_comm_group G₁]
(G : Type*) [ring G]
:=
(f₁ : G₁ →+ G)
namespace geometric_algebra
section
variables
(G₀ : Type*) [field G₀]  I made G₀ explicit here
{G₁ : Type*} [add_comm_group G₁]
{G : Type*} [ring G] [geometric_algebra G₀ G₁ G]
def fᵥ : G₁ →+ G := f₁ G₀
def prod_vec (a b : G₁) : G := (fᵥ G₀ a) * (fᵥ G₀ b)
end
end geometric_algebra
Bryan Ginge Chen (Jun 29 2020 at 17:09):
As Alex says, I get the feeling this would be easier with more bundling though.
Eric Wieser (Jun 29 2020 at 17:10):
What do you mean by bundling in this case?
Bryan Ginge Chen (Jun 29 2020 at 17:11):
Instead of:
class geometric_algebra
(G₀ : Type*) [field G₀]
(G₁ : Type*) [add_comm_group G₁]
(G : Type*) [ring G]
:=
(f₁ : G₁ →+ G)
Something more like:
class geometric_algebra
(G : Type*)
:=
(G₀ : Type*) (f : field G₀)
(G₁ : Type*) (acg : add_comm_group G₁)
(r : ring G)
(f₁ : G₁ →+ G)
(I haven't tested the latter.)
Eric Wieser (Jun 29 2020 at 17:11):
That was what I was about to ask
Eric Wieser (Jun 29 2020 at 17:12):
That means the field
and add_comm_group
fields have to be provided explicitly though, right?
Bryan Ginge Chen (Jun 29 2020 at 17:12):
They should only need to be provided once though when you create an instance of geometric_algebra G
.
Bryan Ginge Chen (Jun 29 2020 at 17:13):
There's a little more about bundled vs unbundled stuff in 4.1.1 of the mathlib paper.
Kevin Buzzard (Jun 29 2020 at 17:13):
by apply_instance
will supply the e.g. field instance if you're making an instance of the bundled structure
Eric Wieser (Jun 29 2020 at 17:13):
I suppose we can make a helper def
to obtain them automatically anyway?
Eric Wieser (Jun 29 2020 at 17:14):
geometric_algebra.mk_from_instances
or something?
Johan Commelin (Jun 29 2020 at 17:14):
Eric Wieser said:
That means the
field
andadd_comm_group
fields have to be provided explicitly though, right?
You can also use []
for fields in a class.
Bryan Ginge Chen (Jun 29 2020 at 17:15):
Right, so:
class geometric_algebra (G : Type*)
:=
(G₀ : Type*) [f : field G₀]
(G₁ : Type*) [ag : add_comm_group G₁]
[r : ring G]
(f₁ : G₁ →+ G)
Johan Commelin (Jun 29 2020 at 17:16):
Something in between would be to make the three types into arguments, but put all the other stuff in fields.
Johan Commelin (Jun 29 2020 at 17:17):
Also, don't you need more functions, and injectivity assumptions?
Eric Wieser (Jun 29 2020 at 17:17):
This becomes slightly painful because we have as a field that I removed, (vec_sq_scalar : ∀ v : G₁, ∃ k : G₀, f₁ v * f₁ v = algebra_map _ _ k )
, where algebra_map
needs the []
arguments
Eric Wieser (Jun 29 2020 at 17:17):
Johan Commelin said:
Also, don't you need more functions, and injectivity assumptions?
Yes, I stripped them to get a #mwe of parameter woes
Kevin Buzzard (Jun 29 2020 at 17:18):
import tactic data.complex.basic
noncomputable theory
structure geometric_algebra
(G : Type*)
:=
(G₀ : Type*) [f : field G₀]
(G₁ : Type*) [acg : add_comm_group G₁]
[r : ring G]
(f₁ : G₁ →+ G)
example : geometric_algebra ℂ :=
{ G₀ := ℂ,
G₁ := ℂ,
f₁ := add_monoid_hom.id ℂ }
It should surely be a structure not a class if it's bundled this much. How many terms of type geometric_algebra ℂ
might there be? Surely "more than one" is a reasonable answer. So structure not class.
Eric Wieser (Jun 29 2020 at 17:19):
I think "exactly one" is a perfectly reasonable answer
Eric Wieser (Jun 29 2020 at 17:22):
ℂ
is canonically Cl(0, 1)
, I think  a GA with a onedimensional vector space, with the sole basis vector squaring to 1
Eric Wieser (Jun 29 2020 at 17:23):
Now maybe I misunderstand the question "how many terms of the form ..."
Johan Commelin (Jun 29 2020 at 17:24):
I don't know what a geometric algebra is... so I can't really help there. (I know Clifford algebras, and I think they are examples.)
Kevin Buzzard (Jun 29 2020 at 17:25):
The reason [group G]
is a class is that if G
is a set/type/whatever you want to call it, then it is generally unlikely that you will want to put more than one group structure on G
(i.e. two different multiplications).
Eric Wieser (Jun 29 2020 at 17:25):
I was under the impression they were synonymous, but I may be mistaken
Kevin Buzzard (Jun 29 2020 at 17:25):
So under normal circumstances, if G
is a type then there will be at most one term of type group G
Johan Commelin (Jun 29 2020 at 17:25):
Eric Wieser said:
I was under the impression they were synonymous, but I may be mistaken
Maybe! Like I said, I don't know what a geom alg is
Kevin Buzzard (Jun 29 2020 at 17:25):
The type class inference system algorithm assumes that there will be at most one instance per class.
Eric Wieser (Jun 29 2020 at 17:26):
Wikipedia says "Real Clifford algebras are also sometimes referred to as geometric algebras."
Kevin Buzzard (Jun 29 2020 at 17:27):
If you decided to make a vector space structure and wrote
class vector_space (k : Type) [field k] :=
(V : Type)
(all the structure of a vector space on V)
then this would be bad, because a term of type vector_space k
would be a vector space over K, and because it's a class, each field is allowed to have at most one vector space over it.
Eric Wieser (Jun 29 2020 at 17:28):
I think I now see Kevin's point. ℂ can be thought of as either a 0d clifford algebra over itself, or a 1d clifford algebra over the reals
Eric Wieser (Jun 29 2020 at 17:28):
So at least G₀
needs to be an argument too
Kevin Buzzard (Jun 29 2020 at 17:29):
The question with
class geometric_algebra (G : Type*)
:=
(G₀ : Type*) [f : field G₀]
(G₁ : Type*) [ag : add_comm_group G₁]
[r : ring G]
(f₁ : G₁ →+ G)
is nothing to do with what happens when G changes. It's precisely to do with what happens if the other stuff changes.
Kevin Buzzard (Jun 29 2020 at 17:29):
If you want more than one G_0 for a given G then you must make it a structure not a class.
Eric Wieser (Jun 29 2020 at 17:29):
Or a class taking two arguments?
Kevin Buzzard (Jun 29 2020 at 17:29):
Eric Wieser said:
So at least
G₀
needs to be an argument too
No. Not if you make it a structure
Kevin Buzzard (Jun 29 2020 at 17:30):
This is a design decision. You can make whatever you like an input or a structure field.
Kevin Buzzard (Jun 29 2020 at 17:30):
My only point was simply that class
means that you expect at most one instance, and structure
means you are allowed as many as you like.
Kevin Buzzard (Jun 29 2020 at 17:31):
but which mathematical object corresponds to "instance" depends on what you make as structure fields and what you make as inputs. The answer changes.
Eric Wieser (Jun 29 2020 at 17:32):
All makes sense, thanks.
Eric Wieser (Jun 29 2020 at 17:33):
I suppose the question now is whether I expect G₀
to uniquely parameterize a geometric algebra G
, or if there's a situation I haven't thought of where multiple choices of G₁
are available
Johan Commelin (Jun 29 2020 at 17:33):
If you want help with that decision, please write down 3 examples for me.
Kevin Buzzard (Jun 29 2020 at 17:34):
Yes, the definition is completely confusing
Kevin Buzzard (Jun 29 2020 at 17:34):
(in its current state, where G_0 plays no role at all)
Utensil Song (Jun 29 2020 at 17:34):
for a given G, there's only one G0
Eric Wieser (Jun 29 2020 at 17:35):
Not if we generalize to the clifford algebras I think...
Utensil Song (Jun 29 2020 at 17:35):
it's still the same
Eric Wieser (Jun 29 2020 at 17:36):
Kevin Buzzard said:
Yes, the definition is completely confusing
That's because the one I post above was the minimum definition that showed a language difficulty, not a mathematically meaningful statement!
Johan Commelin (Jun 29 2020 at 17:36):
Can you write down the definition in maths?
Johan Commelin (Jun 29 2020 at 17:36):
Or link to one?
Kevin Buzzard (Jun 29 2020 at 17:36):
That's because the one I post above was the minimum definition that showed a language difficulty, not a mathematically meaningful statement!
Yes, I know :) That's why Johan just wants to see some examples. Then we'll get the hang of it.
Eric Wieser (Jun 29 2020 at 17:37):
I can give the paper that @Utensil Song started our formalization from: https://arxiv.org/abs/1205.5935
Kevin Buzzard (Jun 29 2020 at 17:37):
I would rather see three examples of G, G_0 and G_1
Eric Wieser (Jun 29 2020 at 17:38):
Ah, ok, got it
Johan Commelin (Jun 29 2020 at 17:39):
The definition on wiki is vague and incomplete as far as I can tell
Kevin Buzzard (Jun 29 2020 at 17:39):
Just some dumb examples
Eric Wieser (Jun 29 2020 at 17:40):
Discussing offline with utensil to try and find some we agree on :)
Johan Commelin (Jun 29 2020 at 17:41):
Hmm, from page 10 onwards in that link there is a pretty precise definition.
Johan Commelin (Jun 29 2020 at 17:41):
However, there is a tonne of structure there.
Johan Commelin (Jun 29 2020 at 17:41):
There will be some nontrivial design decisions here
Johan Commelin (Jun 29 2020 at 17:42):
My intuition is: add all the structure into the definition, and ask for lots of compatibilities.
Eric Wieser (Jun 29 2020 at 17:42):
What do you mean by "compatibilities"?
Johan Commelin (Jun 29 2020 at 17:42):
Then build custom constructors that take less data, and generate the remaining structure (because there will be apparent redundancy in the definition)
Kevin Buzzard (Jun 29 2020 at 17:43):
oh this is highlevel structure making tips!
Johan Commelin (Jun 29 2020 at 17:43):
Example: the inner product follows from other pieces of data, but you might want to explicitly include it in the definition, and then say that the inner product that you include is the same as the one built from the other pieces.
Johan Commelin (Jun 29 2020 at 17:44):
The reason you want this redundancy is that it will give you flexibility in definitional equalities later on.
Utensil Song (Jun 29 2020 at 17:44):
https://stackedit.io/viewer#!url=https://raw.githubusercontent.com/pygae/leanga/master/docs/misc/many_faces.md is an incomplete workinprogress math description of the definition problem here.
Kevin Buzzard (Jun 29 2020 at 17:45):
Like <
can be deduced from <=
in a partial order, but there's an axiom saying a < b ↔ a ≤ b ∧ ¬b ≤ a
Eric Wieser (Jun 29 2020 at 17:46):
@Johan Commelin, is there an example of that approach I can look at in mathlib?
Johan Commelin (Jun 29 2020 at 17:46):
Yes, metric_space
is a classical example
Johan Commelin (Jun 29 2020 at 17:46):
It takes a topology, even though that's completely redundant. But...
Eric Wieser (Jun 29 2020 at 17:46):
Kevin Buzzard (Jun 29 2020 at 17:46):
It takes a uniform structure now, I think
Johan Commelin (Jun 29 2020 at 17:47):
The product topology on the product of two metric spaces is not definitionally the same as the metric topology on the product.
Johan Commelin (Jun 29 2020 at 17:47):
It is a theorem that they are the same. And this theorem is now part of the definition
Johan Commelin (Jun 29 2020 at 17:47):
But there is a constructor that will ignore the topology and just generate it from the metric.
Eric Wieser (Jun 29 2020 at 17:48):
What is that constructor?
Kevin Buzzard (Jun 29 2020 at 17:48):
This is rather advanced structuremaking.
Johan Commelin (Jun 29 2020 at 17:48):
But for the product metric/topology, you don't want to use that constructor!
Johan Commelin (Jun 29 2020 at 17:48):
Kevin Buzzard said:
This is rather advanced structuremaking.
Yup, but the example at hand (geometric algebra) seems quite a complex thing.
Kevin Buzzard (Jun 29 2020 at 17:49):
But I suspect that nondefeq diamonds are right now the least of their worries. We still don't even know if it's a structure or a class.
Eric Wieser (Jun 29 2020 at 17:49):
Looks like https://leanprovercommunity.github.io/mathlib_docs/notes.html#forgetful%20inheritance is related to this conversation?
Kevin Buzzard (Jun 29 2020 at 17:50):
But we can't even think about forgetful inheritence issues until we have decided what is an input and what is a structure field.
Utensil Song (Jun 29 2020 at 17:51):
Johan Commelin (Jun 29 2020 at 17:52):
@Eric Wieser https://github.com/leanprovercommunity/mathlib/blob/eb05a94/src/topology/metric_space/basic.lean#L71
I was wrong, it's not a seperate constructor, but a default argument.
Utensil Song (Jun 29 2020 at 17:52):
the current design is that it's a class
Kevin Buzzard (Jun 29 2020 at 17:52):
So for R R^1 C which is G, G_0, G_1?
Eric Wieser (Jun 29 2020 at 17:53):
Order is specified as G_0 G_1 G
Kevin Buzzard (Jun 29 2020 at 17:53):
so if R R^1 C and C C C are both Ok, you can't have a class and just make G an input
Eric Wieser (Jun 29 2020 at 17:54):
Correct, but we can have a class and make both G_0 and G an input
Utensil Song (Jun 29 2020 at 17:54):
The instended design is geometric_algebra R R^1 G(0, 1)
Utensil Song (Jun 29 2020 at 17:54):
not R R C
Kevin Buzzard (Jun 29 2020 at 17:55):
What is G(0,1)?
Eric Wieser (Jun 29 2020 at 17:55):
The geometric algebra with 0 basis vectors with length 1 and 1 basis vector with length 1
Kevin Buzzard (Jun 29 2020 at 17:55):
Unfortunately that definition is circular
Kevin Buzzard (Jun 29 2020 at 17:55):
Is G determined by G_0 and G_1?
Eric Wieser (Jun 29 2020 at 17:56):
I think the answer is probably yes.
Kevin Buzzard (Jun 29 2020 at 17:56):
Is there a reason you're asking for it at all?
Johan Commelin (Jun 29 2020 at 17:56):
I suggest also reading the story in §6.1 of https://arxiv.org/pdf/1910.12320.pdf
Eric Wieser (Jun 29 2020 at 17:57):
Wait, G can be any implementation of that though right?
Johan Commelin (Jun 29 2020 at 17:57):
About how we approached valuations and especially the target type.
Kevin Buzzard (Jun 29 2020 at 17:57):
We made a lot of design decisions which turned out to be bad
Johan Commelin (Jun 29 2020 at 17:57):
@Utensil Song This G(0,1)
looks fishy.
Kevin Buzzard (Jun 29 2020 at 17:57):
but it was OK, because we learnt a lot
Johan Commelin (Jun 29 2020 at 17:58):
It's may work very well for the abstract theory, but it looks bad for application to examples.
Utensil Song (Jun 29 2020 at 17:58):
The answer is no actually
Johan Commelin (Jun 29 2020 at 17:59):
Kevin Buzzard said:
We made a lot of design decisions which turned out to be bad
Another example was that we gave a mathematically correct definition of "Huber pair" (whatever that may be), but the canonical example that every mathematician will give first (padic integers, padic numbers) could not be made into an instance
with our definition.
Johan Commelin (Jun 29 2020 at 17:59):
We could prove lots of stuff though! But all abstract.
Utensil Song (Jun 29 2020 at 17:59):
it's also determined by the signature p q r and the specific way to implement a geometric algebra
Johan Commelin (Jun 29 2020 at 18:00):
I will repeat, give me an example.
Eric Wieser (Jun 29 2020 at 18:00):
The signature pqr is embedded in the G_1
argument
Johan Commelin (Jun 29 2020 at 18:00):
Is $\mathbb{R}, \mathbb{R}, \mathbb{C}$ an example?
Utensil Song (Jun 29 2020 at 18:00):
sorry I'm typing on my phone in bed...
Reid Barton (Jun 29 2020 at 18:01):
I think all(?) examples are given by G = the Clifford algebra of a vector space V over a field k equipped with a quadratic form, G_0 = k, G_1 = V.
Reid Barton (Jun 29 2020 at 18:01):
If that helps.
Reid Barton (Jun 29 2020 at 18:01):
And obviously up to isomorphism.
Utensil Song (Jun 29 2020 at 18:01):
will type examples out tmr
Johan Commelin (Jun 29 2020 at 18:01):
Reid Barton said:
And obviously up to isomorphism.
That's exactly my point.
Johan Commelin (Jun 29 2020 at 18:01):
You want a definition that also applies to objects isomorphic to that.
Utensil Song (Jun 29 2020 at 18:03):
Eric Wieser (Jun 29 2020 at 18:03):
some examples (G₀ G₁ G
) that utensil may or may not agree with:
Euclidean space: ℝ ℝ³ some_implementation_of_g3_i_wish_to_register
spacetime: ℝ ℝ³,¹ some_implementation_of_sta_i_wish_to_register
an embedding of the builtin complex numbers: ℝ ℝ⁰,¹ ℂ
a different embedding of the builtin complex numbers: ℂ ℂ⁰ ℂ
Johan Commelin (Jun 29 2020 at 18:05):
So your third type should not be some construction, but allow for arbitrary types.
Eric Wieser (Jun 29 2020 at 18:06):
G
you mean  yes, just like the M
argument to vector_space
currently behaves
Johan Commelin (Jun 29 2020 at 18:07):
And maybe G
already has some inner product (from a different part of mathlib), so you don't want to construct the inner product, but take it as an argument. (Even though you might want to give a default argument that constructs it from other data.)
Eric Wieser (Jun 29 2020 at 18:08):
The (vector) inner product comes from G₁
Johan Commelin (Jun 29 2020 at 18:08):
And maybe your G
is already naturally graded into pieces G_0
, G_1
, ... G_r
by another piece of mathlib, so you might want to take all the G_r
as parameters as well
Utensil Song (Jun 29 2020 at 18:08):
@Eric Wieser your examples made it clear to me that we don't need G1 in the parameters
Johan Commelin (Jun 29 2020 at 18:08):
Etc... (this is why I said there is so much data flying around in this definition.)
Eric Wieser (Jun 29 2020 at 18:09):
That's funny @Utensil Song, because it made clear to me that we do if we want the algebra to know about it's own metric
Utensil Song (Jun 29 2020 at 18:10):
it's actually in G already
Utensil Song (Jun 29 2020 at 18:10):
the quadratic form and other stuff...
Utensil Song (Jun 29 2020 at 18:12):
we are talking about two different designs
Johan Commelin (Jun 29 2020 at 18:13):
@Utensil Song Again, I'll claim that's only true in maths, not in lean.
Johan Commelin (Jun 29 2020 at 18:13):
Up to isomorphism, everything is fine.
Utensil Song (Jun 29 2020 at 18:17):
We won't have C R^n Gsth, right? @Eric Wieser
Johan Commelin (Jun 29 2020 at 18:17):
@Utensil Song Is ℂ ℂ⁰ ℂ
an example of a geometric algebra? How about ℝ ℝ⁰,¹ ℂ
?
Utensil Song (Jun 29 2020 at 18:18):
not in the design I'm referring to
Johan Commelin (Jun 29 2020 at 18:19):
Then I can't use your theorems in some interesting concrete examples :sad: :cry:
Utensil Song (Jun 29 2020 at 18:19):
C will be proven to be isomorphic to the G something later
Eric Wieser (Jun 29 2020 at 18:19):
Utensil Song said:
We won't have C R^n Gsth, right? Eric Wieser
No, because there is no instance of vector_space C R^n
Johan Commelin (Jun 29 2020 at 18:19):
Utensil Song said:
C will be proven to be isomorphic to the G something later
Lean doesn't like such isomorphisms. They are a royal pita.
Johan Commelin (Jun 29 2020 at 18:20):
If you create a more flexible definition, your proofs will probably also benefit.
Utensil Song (Jun 29 2020 at 18:20):
That's why G1 should not be special and it's redundant in the parameter and it's just a bundled field
Johan Commelin (Jun 29 2020 at 18:23):
Please read §6.1 of the perfectoid paper (linked above). It's not that long.
Johan Commelin (Jun 29 2020 at 18:24):
Note that this was not a problem that we hit during our project. We were done, and we tried to get some juicy examples. That's when we hit the problem.
Johan Commelin (Jun 29 2020 at 18:24):
We could easily write 1000s of lines of interesting theorems... but they were useless, because we couldn't apply them to concrete examples.
Eric Wieser (Jun 29 2020 at 18:25):
So, the case I'm thinking of is one where I want extra constraints on the vector space for a proof, perhaps that the square of a vector is always positive. I suppose that can be written whether G1 is an argument or not though, as [ga G0 G1 G] (h : ∀ g : G1, p g)
or [h : ga G0 G] (h : ∀ g : h.G1, p g)
Utensil Song (Jun 29 2020 at 18:25):
consider the complex numbers as either:
 G(0, 1) over R
 G(0, 0) over C
Johan Commelin (Jun 29 2020 at 18:25):
@Utensil Song Lean disagrees. It only knows complex
. That's it.
Eric Wieser (Jun 29 2020 at 18:25):
I'm working on reading it @Johan Commelin, my math background is pretty weak :)
Johan Commelin (Jun 29 2020 at 18:25):
Lean is pretty stubborn. It will not change it's mind.
Utensil Song (Jun 29 2020 at 18:25):
we need both
Johan Commelin (Jun 29 2020 at 18:25):
I agree that you need both.
Utensil Song (Jun 29 2020 at 18:26):
so it seems isomorphism is the way to go
Johan Commelin (Jun 29 2020 at 18:26):
And since both are examples of foobar : Type*
, you should include a foobar : Type*
that abstracts over this.
Johan Commelin (Jun 29 2020 at 18:26):
No, abstracting into types with axioms about that type. That's the way to go.
Utensil Song (Jun 29 2020 at 18:26):
(deleted)
Johan Commelin (Jun 29 2020 at 18:27):
A Huber pair is a pair (R, A)
where R
is a subring of A
. Except that in mathlib Z_p
is not a subring of Q_p
. There is an injective ring homomorphism.
Johan Commelin (Jun 29 2020 at 18:28):
So we changed the definition of Huber pair to: a pair (R, A)
with an injective ring homomorphism R →+* A
.
Johan Commelin (Jun 29 2020 at 18:28):
Mathematically an isomorphic definition, but it makes a big difference in lean.
Johan Commelin (Jun 29 2020 at 18:28):
And guess what! Some proofs became easier!
Utensil Song (Jun 29 2020 at 18:28):
abstracting into types with axioms about that type. That's the way to go.
I see, this is it.
Eric Wieser (Jun 29 2020 at 18:29):
So to be clear, you replace the requirement "is a subring of" with a field providing that homomorphism?
Johan Commelin (Jun 29 2020 at 18:30):
And my impression from what I've read so far about geometric algebras, is that there are lot's of things that can be abstracted into types and functions, and there will be many compatibility axioms.
Utensil Song (Jun 29 2020 at 18:30):
yes
Johan Commelin (Jun 29 2020 at 18:30):
@Eric Wieser Yes, replace (A : Type*) (R : subring A)
with (A : Type*) (R : Type*) (f : R →+* A) (hf : injective f)
.
Eric Wieser (Jun 29 2020 at 18:31):
And then presumably provide a constructor that populates f
and hf
for you if you can show R : subring A
?
Johan Commelin (Jun 29 2020 at 18:31):
We didn't provide such a constructor, but you could do that.
Eric Wieser (Jun 29 2020 at 18:32):
Did you find it would never have been useful?
Eric Wieser (Jun 29 2020 at 18:33):
It seems like you're obliged to provide that constructor to prove the statements are mathematically isomorphic ;)
Utensil Song (Jun 29 2020 at 18:33):
so now we all agree C cant directly stand at the position of G, but a structure abstracted over it, right?
Johan Commelin (Jun 29 2020 at 18:34):
I'm confused...
Eric Wieser (Jun 29 2020 at 18:34):
At me or utensil, @Johan Commelin?
Johan Commelin (Jun 29 2020 at 18:34):
Utensil
Johan Commelin (Jun 29 2020 at 18:35):
I would think that when you create examples, you do want to be able to plug C
into some field at some point.
Kevin Buzzard (Jun 29 2020 at 18:35):
Eric Wieser said:
So to be clear, you replace the requirement "is a subring of" with a field providing that homomorphism?
In type theory there is no such thing as a subring, really. There is some construction called a subring. But if A > B is an injective ring homomorphism then that does not make A a subring of B, and indeed it would be impossible in general to make A a subring of B. A and B are just different types. The whole "sub" thing is dangerous.
Johan Commelin (Jun 29 2020 at 18:35):
Eric Wieser said:
Did you find it would never have been useful?
We just directly plugged in R
, subtype.val
and subtype.val_injective
. It's so short that it didn't merit a new constructor.
Eric Wieser (Jun 29 2020 at 18:40):
This has been lots of useful discussion for me, thanks everyone
Utensil Song (Jun 29 2020 at 18:42):
sorry since its 2:39am in my timezone, I'll get some sleep first. I'm pretty sure I can come up with a #mwe to demonstrate what's in my mind after the discussion above, with defs and juicy concrete examples.
Johan Commelin (Jun 29 2020 at 18:42):
So clearly, if you start with Q : V → K
, and you construct the Clifford algebra, then you want Q
, V
and K
to be fields in the structure. Not isomorphic things.
Johan Commelin (Jun 29 2020 at 18:43):
Utensil Song said:
sorry since its 2:39am in my timezone, I'll get some sleep first. I'm pretty sure I can come up with a #mwe to demonstrate what's in my mind after the discussion above, with defs and juicy concrete examples.
Sleep well! :sleeping:
Bryan Ginge Chen (Jun 29 2020 at 18:43):
Kevin Buzzard said:
In type theory there is no such thing as a subring, really. There is some construction called a subring. But if A > B is an injective ring homomorphism then that does not make A a subring of B, and indeed it would be impossible in general to make A a subring of B. A and B are just different types. The whole "sub" thing is dangerous.
Speaking for myself, this has been one of the harder things to wrap my head around in formalization. (I spent a bunch of time trying to figure out how to define and work with submatroids and I'm still stuck...) I hope that MiL has a lot of discussion about this.
Johan Commelin (Jun 29 2020 at 18:43):
Johan Commelin said:
So clearly, if you start with
Q : V → K
, and you construct the Clifford algebra, then you wantQ
,V
andK
to be fields in the structure. Not isomorphic things.
Because in the end, you want to deduce facts about Q
, V
and K
.
Utensil Song (Jun 29 2020 at 18:43):
thanks!
Utensil Song (Jun 30 2020 at 10:37):
I realized that I should first #xy the problem before writing a new #mwe . The following will refer to the definitions in The Many Faces of Geometric Algebra by section titles with <> around them. I'll try to avoid mentioning any specific language structure in Lean such as structure/type class/instance, inheritance, parameters, bundled v.s. unbundled etc. because they're part of the y.
The grand design is somewhat topdown.
 Define general Geometric Algebra (GA) with axioms about its properties/behaviors instead of representations, avoid mentioning grades/coordinates/metric, etc., keep it as readable and intuitive as possible;
 Define G(p, q, r) over a field which could be ℝ, ℂ or dual numbers 𝔻, hyperbolic numbers ℍ ( note that this is not quaternions ) but without specific metric, where (p, q, r) means
p
positive,q
negative andr
zero dimensions, e.g. Minkowski space is ℝ(1, 3, 0), dual number is G(0, 0, 1); Projective GA(PGA) and Conformal GA(CGA) are of specific interest at this abstraction layer with their own theorems and identities unrelated to specific metrics  Define G(p, q, r) over a field a specific metric(or quadratic form)

All of
a. Formalize data structures and the corresponding algorithms in sense of software libraries, such as using binary trees or prefix trees or whatever to implement GA
b. formalize GA in other ways so that it's equivalent to the definition in 1 (with certain limited scope), the formalization might be <Lawson 1989>, <Clifford algebra as a quotient of the tensor algebra> or <Clifford 1882>
c. ℝ, ℂ, dual numbers 𝔻, hyperbolic numbers ℍ, quaternions ℚ are all GAs 
Prove general theorems and identities for 1, prove 2 "is" 1, prove dedicated theorems and identities for PGA and CGA, prove 3 "is" 2, prove 4b is 2 or 1, prove 4a and 4c are 3.
Last night, Eric was talking about at most the relationship between 3 and 4, and I was thinking about how to handle all the relationships between all of the above(and they might not be the same!). Maybe I've overcomplicated the problem at an initial stage. That's why I kept saying "not exactly" to Eric's examples.
Now let's come back to the current attempt in https://github.com/pygae/leanga/blob/master/src/geometric_algebra/nursery/chisolm.lean . It's trying to directly address 1 and it has at least the following mistakes:
 it should not directly try to address 1, instead, it should try something more concrete at the level of 2 or 3 and attack 1 based on what's learned during the process;
 it should not choose the axiom sets in <Chisolm 2012>, the axioms treated G₀ and G₁ specially and I believe this is its weakness; on the opposite, something like <Buchholz 2005>, <Definition by generators and relations>, <Lynn> might be better alternatives;
 it should not choose using [] parameters to specify most of the axioms, the axioms should be bundled fields
 it could reduce the numbers of types in parameters, the possibilities are 2(only G₀ and G), 1(only G) or 0;
 it should not stick to type class to implement the "is"s in 5, and might need to use the technique documented in https://leanprovercommunity.github.io/mathlib_docs/notes.html#forgetful%20inheritance for better definitionally equality; there might be other alternatives;
 it should handle the equality across types (i.e. Gr) better, such as the way to deal with the fact that the square of G₁ is G₀, homs are used here, but there're alternatives like coe, set, subtype etc.
 it should pick a way to prove that ℂ could "be" G(0, 1, 0) over ℝ or G(0, 0, 0) over ℂ, and find a way to allow plugging ℂ into proven theorems about abstract GA.
Utensil Song (Jun 30 2020 at 11:09):
Some concrete examples of GA (but not of the geometric_algebra G₀ G₁ G
here) are(note: it's not Lean):
# Basic
ℝ = G(0) # Real numbers.
ℂ = G(0,1) # Complex numbers.
ℚ = G(0,2) # Quaternions.
ℍ = G(1) # Hyperbolic numbers.
𝔻 = G(0,0,1) # Dual numbers.
# Clifford
Cl2 = G(2) # Clifford algebra for 2D vector space.
Cl3 = G(3) # Clifford algebra for 3D vector space.
Spacetime = G(1,3) # Clifford algebra for timespace vectors.
# Geometric
PGA2D = G(2,0,1) # Projective Euclidean 2D plane. (dual)
PGA3D = G(3,0,1) # Projective Euclidean 3D space. (dual)
CGA2D = G(3,1) # Conformal 2D space.
CGA3D = G(4,1) # Conformal 3D space.
Reid Barton (Jun 30 2020 at 12:55):
One curious thing about this notion of geometric algebra (at least in the Chisolm version) which is clarified by some of the other presentations is that it is not really an algebraic structure at all, in the sense of describing a kind of algebra. Rather, it's attempting to axiomatize the free algebra of some sort: namely (noncommutative) $k$algebras equipped with a $k$linear map from $V$ compatible with the quadratic form on $V$ in a certain way.
Reid Barton (Jun 30 2020 at 12:57):
So maybe it would be worthwhile to start by formalizing that kind of algebra.
Reid Barton (Jun 30 2020 at 12:57):
I think equations which hold in all geometric algebras would also hold in all of these guys.
Utensil Song (Jun 30 2020 at 14:23):
Mathematically, it's correct. GA is simply a free algebra with one particular constraint on the quadratic form. But such a statement is of no interest to the community applied GA in mathematical physics, quantum physics, electromagnetism, astrophysics, computer graphics, machine vision, engineering, robotics etc. All rich structures and interesting behaviors arise from that one constraint, and in turn, embeds many concepts in different math areas with different appearances.
Utensil Song (Jun 30 2020 at 14:48):
it is not really an algebraic structure at all, in the sense of describing a kind of algebra.
I don't follow what qualifies as an algebra here.
Repeatedly and independently a long list of Clifford's geometric algebras, their subalgebras have been studied and applied historically, often under different names. Some of these algebras are complex numbers (and the complex number plane), hyperbolic numbers (split complex numbers, real tessarines), dual numbers, quaternions, biquaternions (complex quaternions), dual quaternions, Plucker coordinates, bicomplex numbers (commutative quaternions, tessarines, Segre quaternions), Pauli algebra (space algebra), Dirac algebra (spacetime algebra, Minkowski algebra), algebra of physical space, paravector algebra, spinor algebra, Lie algebras, Cartan algebra, versor algebra, rotor algebra, motor algebra, Clifford bracket algebra, conformal algebra, algebra of differential forms, etc.
Utensil Song (Jul 01 2020 at 04:03):
Johan Commelin said:
I suggest also reading the story in §6.1 of https://arxiv.org/pdf/1910.12320.pdf
I'm trying to sort out what's going on in that section. The storyline seems to be:
The definition
$\Gamma_0 := \Gamma \cup {0}$ where the multiplication and order relation are extended by specifying that 0γ = 0 × 0 = 0 and 0 ≤ γ for every γ in Γ.
focuses on the construction of $\Gamma_0$, starting from an ordered group and adding an element, rather than the properties of the resulting object.
The latter (directly addressing the properties of the resulting object instead of piecing some construction together and suddenly new behaviors emerge out of no(intuitively)where) is exactly what I'm after. If I have to extend some structure or bundle some field, I'll rather be adding some behaviors rather than gluing some constructions.
We used Lean’s coercion mechanism to automatically insert the “inclusion” map from Γ to $\Gamma_0$. In set
theory, this is indeed a true inclusion, but there are no inclusions between types in type theory as a term
can only have one type. Thenorm_cast
tactic, by PaulNicolas Madeleine [Mad19], greatly alleviates
the pain of invoking lemmas about such coercions
Settheoretically, it is almost true that $\mathbb{R}_{\ge 0} = (\mathbb{R}_{\gt 0})_0$. This tiny lie only requires that we forget that the 0 in $(\mathbb{R}_{\gt 0})_0$ is meant to be an extra element coming from nowhere in particular, hence has nothing to do with the neutral element of the additive group R. It gets harder to ignore with typetheoretic foundations. It means that merging the elementary theory with our abstract theory would require nontrivial glue.
Generally I love typetheoretic foundations because it seems more strict and you can't blur things out unintentionally. But it's really problematic when you intentionally need to do something across types, it forces you to be verbosely formal and I'm yet to find the best practice to handle such situations. This story give hints about how to handle it, accompanied by old code presumably here.
We defined the concept of totally ordered commutative monoid with zero as a type equipped with a composition law, a total order, and special elements 0 and 1 with enough properties to guarantee that all instances are isomorphic (as ordered commutative monoids) to some $\Gamma_0$. This corresponds to a type class which admits both with_zero Γ and {x : R // 0 ≤ x} as instances. Once again, focusing on properties instead of constructions gives us the needed extra flexibility at no cost.
So here's the solution. Basically I understood the last sentence and worked my way backwards with the help of the corresponding code here, particularly src/valuation/basic.lean
(see also linear_ordered_comm_group_with_zero at master branch). The core idea here seems to be we should model the properties in the definitions and prove some construction is an instance of it later and the benefit would be (I guess) better integration with elementary theory which involves more informal treatment?
Johan Commelin (Jul 01 2020 at 05:58):
The core idea here seems to be we should model the properties in the definitions and prove some construction is an instance of it later
Yes, exactly.
and the benefit would be (I guess) better integration with elementary theory which involves more informal treatment?
The benefit would be that examples that are not by definition equal to you construction can still be turned into instances, whereas with the approach we took first this is simply impossible.
nnreal
is not of the formwith_zero G
. It's only isomorphic to it.Z_p
is not aset Q_p
and henceis_subring Z_p
will never work. But it does have an injective ring homomorphism toQ_p
.
Kevin Buzzard (Jul 01 2020 at 06:35):
As a mathematician you might say "but what is the problem here? If X and Y are isomorphic then everything which is true for X is true for Y". This is problematic for two reasons. Firstly, the principle is not true in general. For example if P(T) is T=X
(which makes sense in type theory) then P(X) is true and P(Y) might not be (in Lean at least  in a univalent theory this would be true but their = is not proofirrelevant and this seems to bring other problems).
And secondly, because all the mathematical facts about X, which of course do translate over to Y, actually have to be translated over. There is no "rewrite along an isomorphism" like there is a rewrite along an equality, and until such a tactic exists (and it will be hard to write because it's not always true, it's not true for P above for example) everything has to be transferred manually. Completely dumb proofs like if V and W are isomorphic algebras and V is 10 dimensional over some subalgebra isomorphic to the reals then so is W  this is mathematically obvious but will not be a oneliner in Lean by any means
Utensil Song (Jul 01 2020 at 13:40):
I was trying to have a few examples under the current definition, and have difficulty proving instance rrc_ga : geometric_algebra ℝ ℝ ℂ
at the sorry / here /
in the following #mwe:
import algebra.group.hom
import ring_theory.algebra
import data.real.basic
import data.complex.basic
import data.complex.module
import tactic
universes u u₀ u₁
class geometric_algebra
 Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀]
 Axiom 3: G contains a subset G1 closed under addition,
 and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
 Axiom 1: G is a ring with unit.
 The additive identity is called 0 and the multiplicative identity is called 1.
(G : Type*) [ring G]
[algebra G₀ G]
:=
(f₁ : G₁ →+ G)
 Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar : ∀ v : G₁, ∃ k : G₀, f₁ v * f₁ v = algebra_map _ _ k )
namespace geometric_algebra
section
parameters
{G₀ : Type*} [field G₀]
{G₁ : Type*} [add_comm_group G₁] [vector_space G₀ G₁]
{G : Type*} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G]
def fᵥ : G₁ →+ G := f₁ G₀
def fₛ : G₀ →+* G := algebra_map G₀ G
noncomputable instance rrc_ga : geometric_algebra ℝ ℝ ℂ := {
f₁ := {
to_fun := λx, x,
map_zero' := rfl,
map_add' := begin
intros x y,
norm_cast,
end
},
vec_sq_scalar := begin
intro v,
use v * v,
simp only [add_monoid_hom.coe_mk, ring_hom.map_mul],
sorry / here /
end
}
/ For later discussion, the below doesn't matter for this question /
instance field_ga (K : Type*) [field K] : geometric_algebra K K K := {
f₁ := {
to_fun := id,
map_zero' := rfl,
map_add' := begin
simp only [forall_const, id.def, eq_self_iff_true]
end
},
vec_sq_scalar := begin
intro v,
use v * v,
simp only [algebra.id.map_eq_self, add_monoid_hom.coe_mk, id.def],
end
}
 noncomputable instance rcc_ga : geometric_algebra ℝ ℂ ℂ := {
 f₁ := {
 to_fun := id,
 map_zero' := rfl,
 map_add' := by simp,
 },
 vec_sq_scalar := / mathematically false due to the wrong mul equiped with ℂ /
 }
end
end geometric_algebra
Utensil Song (Jul 01 2020 at 13:40):
The goal state is
v : ℝ
⊢ ↑v * ↑v = ⇑(algebra_map ℝ ℂ) v * ⇑(algebra_map ℝ ℂ) v
Eric Wieser (Jul 01 2020 at 13:46):
The solution to your sorry is refl
Utensil Song (Jul 01 2020 at 13:46):
unfold algebra_map
only gives
v : ℝ
⊢ ↑v * ↑v = ⇑algebra.to_ring_hom v * ⇑algebra.to_ring_hom v
and I can't do any rw
or apply
with algebra.to_ring_hom.xxx
Utensil Song (Jul 01 2020 at 13:47):
I tried everything except refl
!
Reid Barton (Jul 01 2020 at 13:48):
Utensil Song said:
it is not really an algebraic structure at all, in the sense of describing a kind of algebra.
I don't follow what qualifies as an algebra here.
I mean in the sense of universal algebra. For example groups are the models of an algebraic theory in the sense that they are sets equipped with certain functions/constants which satisfy universally quantified equations (like "for all $x$, $y$, $z$, we have $(x * y) * z = x * (y * z)$"). Free groups however are not the models of an algebraic theory.
Utensil Song (Jul 01 2020 at 13:48):
It's really weird that simp
can't cover this and refl
can.
Utensil Song (Jul 01 2020 at 14:02):
@Reid Barton After reading the group example in https://en.wikipedia.org/wiki/Universal_algebra , I'm pretty sure GA can be rephrased so that it's also a universal algebra.
Utensil Song (Jul 01 2020 at 14:05):
There are many existing substitutions of "Axiom 4: The square of every vector is a scalar" in literature, I always wondered which's the best one.
Utensil Song (Jul 01 2020 at 14:10):
For example, would the following qualify for universal algebra?
Let $(\mathrm{X}, \mathrm{Q})$ be an arbitrary finite dimensional real quadratic space and let $\mathcal{A}$ be a real associative algebra with identity. Furthermore, let
$\alpha: \mathbb{R} \rightarrow \mathcal{A}$ and $v: \mathrm{X} \rightarrow \mathcal{A}$ be linear injections such that
(i) $\mathcal{A}$ is generated as an algebra by its distinct subspaces $\{v(v) \mid v \in X\}$ and $\{\alpha(a) \mid a \in \mathbb{R}\}$
(ii) $\forall v \in X:(v(v))^{2}=\alpha(Q(v))$
Then $\mathcal{A}$ is said to be a Clifford algebra for $(\mathrm{X}, \mathrm{Q})$. The elements of a Clifford algebra are
called multivectors. The product of a Clifford algebra is named geometric product. The signature of the quadratic space is also the signature of the algebra.
Utensil Song (Jul 01 2020 at 14:16):
I guess not yet. It's still not only about nary operations and identities.
Reid Barton (Jul 01 2020 at 14:24):
If you remove part (i), then I think so
Utensil Song (Jul 01 2020 at 14:55):
I think (i) is not necessary but a natural result of the rest of the definition. Will have to verify that.
Jalex Stark (Jul 01 2020 at 16:57):
Utensil Song said:
It's really weird that
simp
can't cover this andrefl
can.
A proof of equality by simp
is "once we simplify both sides, using simp lemmas we created on purpose, they become syntactically equal".
A proof of equality by refl
is "these are definitionally equal, you can check by unfolding the definitions"
Jalex Stark (Jul 01 2020 at 17:00):
If simp
can't solve something that you expect it to solve, there's implicitly a lemma that you think should be tagged with @[simp]
but isn't.
Eric Wieser (Jul 01 2020 at 17:13):
@Jalex Stark: So to be clear, if simp
fails but refl
succeeds, refl
is unfolding definitions that simp
is not?
Kevin Buzzard (Jul 01 2020 at 17:19):
refl
will unfold everything. simp
won't.
Kevin Buzzard (Jul 01 2020 at 17:19):
def foo := ℕ
example : foo = ℕ :=
begin
simp,  fails
end
Kevin Buzzard (Jul 01 2020 at 17:20):
def foo := ℕ
example : foo = ℕ :=
begin
simp [foo],  works
end
Of course refl
works.
Kevin Buzzard (Jul 01 2020 at 17:21):
simp [foo]
looks a bit weird because simp
likes to use lemmas of the form A=B
or A <> B
 it is a confluent rewriting system.
Jalex Stark (Jul 01 2020 at 17:21):
Yes
Kevin Buzzard (Jul 01 2020 at 17:21):
But
def foo := ℕ
#print prefix foo
/
foo : Type
foo.equations._eqn_1 : foo = ℕ
/
and what's happening is that simp
temporarily is adding foo.equations._eqn_1
to the simp set
Kevin Buzzard (Jul 01 2020 at 17:22):
This is how unfold
works. unfold X
is basically "simp only [X.equations*]" I think.
Scott Morrison (Jul 01 2020 at 23:05):
This difference between simp
and refl
is quite instructive. At first everyone thinks of refl
as a "really simply" tactic, that "just checks if things are equal". However it's actually potentially doing a huge amount of work, because it is willing to unfold definitions arbitrarily deeply. This is what people are referring to when they say "a heavy refl
".
Scott Morrison (Jul 01 2020 at 23:06):
On the other hand simp
looks complicated because it potentially makes use of a whole zoo of lemmas, but on the other hand it works at a syntactic level (it will unfold reducible
, and this can be tweaked) so is in some sense much more controllable.
Scott Morrison (Jul 01 2020 at 23:07):
I would say that is refl
is succeeding and simp
is failing, it's probably an indication you should try to add some simp
lemmas.
Utensil Song (Jul 02 2020 at 02:36):
Thanks for the very informative answers!
By "weird", actually there's a whole bunch of questions:
Q1. As @Jalex Stark @Scott Morrison pointed out the potential possibility, is there some simp
lemma missing for algebra
, ring_hom
? Should we and how can we do something about it?
Q2. Are all the understandings below correct or some of them are misleading? Particularly c, d, f, i, j, l. And the questions n through r.
a. Initially I enjoy the atomic apply
and rw
for >
and =
, respectively.
b. simp
was merely a tool helping me find out the stuff in simp only [stuff]
.
c. Using simp only [stuff]
instead of rw [stuff]
was merely saving me the trouble from handling the order and the repetition of the rewrites.
d. Then I noticed that sometimes seemingly complex goal can be simplified significantly by simp only []
which indicates there must be something other than just rewrites using simp
lemmas in simp
which I have no idea what's going on.
e. I try to avoid using simp
in the middle of a proof and consider it a finishing tactic.
f. but I find myself repeatedly having to using simp only []
or simp only [stuff]
to clean up some noise in the goal and proceed. I don't know if it's something wrong with my use of coe/homs/alias etc.
g. then I noticed the differences of syneq, defeq, propeq (and in this order the eq is from close to more far away)
h. and start using unfold
for defeq instead of rw
since the latter can only apply the defeq rewrite for one pattern repeatedly but unfold
can do this for all patterns repeatedly. by pattern I mean, if I have a def of f
, than rw
works on both f(a)
in f(a) + f(b) + f(a)
but not f(b)
but unfold
works on f(*)
.
i. then I noticed dsimp
, which seems to be more powerful than unfold
which should help me figure out the stuff in unfold [stuff]
j. and it's more conservative than simp
since it only uses defeq
k. but I haven't been able to use dsimp
to solve any goal yet
l. and I'm reluctant to use dsimp
because I don't know how to squeeze it or trace it
m. with the discussions above, it seems refl
is much heavier than just check defeq
at a shallow level and applying refl lemmas, and it's "willing" to check defeq at arbitrary depth
n. then why there's the need of manual unfold and dsimp? is the difference only that refl is a finishing tactic and it fails if it can't close the goal?
o. why I can't close the goal with dsimp
?
p. do I have some nonfinishing tactic to do what's similar to refl
did but in the middle of a proof?
q. the most important question is, what defeq did refl
check in this example?
r. can I mimic it with other tactics which explicitly mention the defeq it used?
Scott Morrison (Jul 02 2020 at 02:43):
Oof, too many questions to be able to answer...
Scott Morrison (Jul 02 2020 at 02:44):
o. why I can't close the goal with dsimp?
because it doesn't have anything in it that could close a goal; it always replaces one goal with another. Anytime you think you might "close a goal with dsimp
", you want to use refl
.
Scott Morrison (Jul 02 2020 at 02:45):
re: m. and n. Yes! I never use unfold
, only dsimp
.
Scott Morrison (Jul 02 2020 at 02:46):
d. simp only []
will do beta reduction, and I think also unfold projections(?)
Scott Morrison (Jul 02 2020 at 02:47):
dsimp
is allowed midproof (although often can be removed once the proof is working, unless the following tactic is relying on the syntactic form that dsimp
produced)
Scott Morrison (Jul 02 2020 at 02:48):
(i.e. in anything of the form dsimp, exact ...
, the dsimp
is unnecessary. Often however a dsimp
may be needed before simp
or rw
)
Scott Morrison (Jul 02 2020 at 02:49):
re "n" again: the need for dsimp
is that it unfolds definitions, and many other tactics won't, so you need to do it by hand before calling them
Scott Morrison (Jul 02 2020 at 02:50):
Regarding Q1: anytime you think simp
should help, but it doesn't, you should try to write the simp
lemma that you think should have fired!
Scott Morrison (Jul 02 2020 at 02:50):
This is a very important part of developing a new theory  setting up the (hopefully confluent) rewriting rules that are always "safe" to use.
Scott Morrison (Jul 02 2020 at 02:50):
You want as much as possible to be handled by simp
, because it makes everything easier for anyone who comes afterwards to your theory.
Utensil Song (Jul 02 2020 at 04:15):
Scott Morrison said:
o. why I can't close the goal with dsimp?
because it doesn't have anything in it that could close a goal; it always replaces one goal with another. Anytime you think you might "close a goal with
dsimp
", you want to userefl
.
Ah, I phrased it wrong. The actual question is, now that refl can close the goal, and it's about defeq, why can't dsimp which focuses on defeq achieve the same thing? What can I do to help it to achieve this, like supply defs in dsimp [defs]
?
Utensil Song (Jul 02 2020 at 04:18):
Scott Morrison said:
Regarding Q1: anytime you think
simp
should help, but it doesn't, you should try to write thesimp
lemma that you think should have fired!
Yes, but the defs involved here are in algebra
part of mathlib, I was wondering if anyone is aware of the situation that some simp
lemma is missing.
Scott Morrison (Jul 02 2020 at 04:25):
dsimp
will only use lemmas marked with @[simp]
. So yes, you need to explicitly make these lemmas.
Scott Morrison (Jul 02 2020 at 04:26):
And yes, @[simp] lemmas are missing all across mathlib! As you identify them, please make PRs adding @[simp]
to them. :)
Scott Morrison (Jul 02 2020 at 04:27):
It's nontrivial to decide exactly which lemmas should be simp lemmas, and so it doesn't always get done thoroughly.
Utensil Song (Jul 02 2020 at 04:27):
Scott Morrison said:
You want as much as possible to be handled by
simp
, because it makes everything easier for anyone who comes afterwards to your theory.
I totally agree to do so for the endusers and intend to do so in a later stage. And yet inside the library, I'm a little bit afraid of the lemmas proven by simp
, which means I don't have any clue about the dependencies here, it feels circular to me somehow although I know this is unlikely the actual case.
So, what's the best practice here? I might be a little pedantic or overcautious here and was thinking about:
 only use
simp only [xxx]
with the help ofsqueeze_simp
; simp
involving only the simp lemmas in mathlib is allowed; use no
simp
inside the theory if it involves simp lemmas in the theory;  to avoid the circular feeling  to relax 2 a little bit, if I can break the theory into a few layers, then the top layers can invoke the layers under it;  but I don't know how to prevent
simp
usingsimp
lemmas from the same layer, except check manually or by a linter examining the[xxx]
insimp only [xxx]
.
Jalex Stark (Jul 02 2020 at 04:34):
i don't understand what circularity you are trying to avoid
Scott Morrison (Jul 02 2020 at 04:37):
I'm not sure either.
Scott Morrison (Jul 02 2020 at 04:39):
How could there be any circularity? simp
will only use lemmas proved higher up the page
Utensil Song (Jul 02 2020 at 05:25):
The circularity does not exist in Lean. It exists in one's mind because one has read the simp lemmas higher up the page and everywhere else...
Johan Commelin (Jul 02 2020 at 06:05):
@Utensil Song
p. do I have some nonfinishing tactic to do what's similar to refl did but in the middle of a proof?
How about tactic#change ? Is that what you're looking for?
Utensil Song (Jul 02 2020 at 06:08):
I tried change
but I fail to provide the new goal to change
, copying from the goal and modifying it won't always work, what's printed in goal view is not always legal lean.
Utensil Song (Jul 02 2020 at 06:09):
e.g. copying the goal state in https://leanprover.zulipchat.com/#narrow/stream/113489newmembers/topic/synthesized.20not.20defeq.20inferred/near/202569857
Johan Commelin (Jul 02 2020 at 06:10):
Utensil Song said:
I tried
change
but I fail to provide the new goal tochange
, copying from the goal and modifying it won't always work, what's printed in goal view is not always legal lean.
Yup, this is a known issue, and it's hard to solve. Lean 4 will have a delaborator, and then life should be much better.
Johan Commelin (Jul 02 2020 at 06:10):
However, usually you can fix this by adding some type annotations and removing some uparrows.
Utensil Song (Jul 02 2020 at 06:10):
or {re := v, im := 0} * {re := v, im := 0} = ⇑(algebra_map ℝ ℂ) (v * v)
Johan Commelin (Jul 02 2020 at 06:10):
What's printed in the goal is not always legal lean, but it is almost always almost legal lean.
Bryan Ginge Chen (Jul 02 2020 at 06:12):
You can try using set_option pp.implicit true
or other pp
options, sometimes that helps to get something you can use.
Scott Morrison (Jul 02 2020 at 06:20):
I find deleting the up arrows fixes 95% of prettyprinted output problems.
Utensil Song (Jul 02 2020 at 06:38):
That's basically set_option pp.coercions false
?
Utensil Song (Jul 02 2020 at 06:38):
What's the quickest way to convert the structure stuff in goal view into legal Lean? like in https://leanprover.zulipchat.com/#narrow/stream/113489newmembers/topic/synthesized.20not.20defeq.20inferred/near/202653388
Utensil Song (Jul 16 2020 at 04:46):
We got stuck on how to implement the bundled version for a while and here's how far we have got ( #mwe for unbundled, bundling V, and bundling both R&V, demonstrated in 3 different namespaces). The most natural one seems to be bundling only V.
It there any way to make the references to the maps less verbose?
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
Scott Morrison (Jul 16 2020 at 05:25):
Just a random comment  using abbreviations like mwc
is unhelpful. Presumably this is intended to be some standard mathematical object, and perhaps if you'd written out mwc
I'd have heard of it, and not have to reverse engineer by _actually reading the code_. :)
Scott Morrison (Jul 16 2020 at 05:26):
Also  given there's been a two week pause on this thread, and this doesn't seem to be about the original title anymore, perhaps moving this to a new thread would be easier.
Scott Morrison (Jul 16 2020 at 05:26):
(and get more attention)
Utensil Song (Jul 16 2020 at 06:06):
Thanks, I'll start a new topic. As for the naming, because other mathematical properties are stripped away and only the technical issue (figuring out how bundling v.s. unbundling type classes works in Lean and how to refer to fields in them) is left, I don't have any meaningful name for it anymore...I'll add a description though.
Utensil Song (Jul 16 2020 at 07:04):
Last updated: May 08 2021 at 10:12 UTC