Univalence axiom

Stream: general

[Thomas Scholz]

Is it possible to formulate and prove in Lean (together with the univalence axiom from homotopy type theory) the statement
"Isomorphic groups have the same (structural) properties."
Or is this just like a meta property that cannot be formulated in Lean?

Of course, one could formulate the statement not only for groups, but for any kind of structure.

[Simon Hudon]

The univalence axiom is inconsistent with proof irrelevence which is baked into Lean's logic. I think with parametricity theorems we may be able to prove this kind of result. @Mario Carneiro or @Johannes Hölzl might have to chime in to confirm.

[Thomas Scholz]

Okay. But in general (without proof irrelevance), would it be possible in type theory to formulate/formalize statements such as
"Isomorphic groups have the same (structural) properties."?
Or are such statements rather meta properties?
I guess that in ZFC, the above statement is not formalizable, because it is not possible to quantify over properties (let alone define what a structural property). So my hope is that the statement is formalizable in type theory, because in type theory, properties are mathematical objects. Also, in type theory, all properties are structural properties, I think.
Please let me know if this is the wrong place to ask this question.

[Johan Commelin]

Here is a property of groups: let G be a group. My property for groups H is: H = G.
This is true for the group G, but not in general for arbitary groups H that are merely isomorphic to G.

[Johan Commelin]

HoTT fixes this by changing =.

[Thomas Scholz]

Okay. In HoTT, is it possible to formulate/formalize statements such as
"Isomorphic groups have the same (structural) properties."?
Or are such statements rather meta properties in HoTT?

[Floris van Doorn]

Yes, in HoTT you can easily prove that isomorphic groups have the same properties. The formal statement could be something like

∀(G H : Group), G ≅ H → ∀(P : G → Prop), P G ↔ P H

Note that G and H share all properties that can be expressed in the type theory. This might look a bit weird from a set-theoretic perspective: G and H could have different elements. However, in type theory you cannot really express that.

Aside: with Prop above I mean all types that have at most 1 element. You can replace Prop by Type and the statement would still be true.

[Kevin Buzzard]

I don't really have time right now to start playing with this Voevodsky stuff where you work in Coq and have this extra axiom. Is there a way of doing this sort of stuff in Lean 3? Lean 4?

[Kevin Buzzard]

I went out for a meal this week with a strong algebraist and I asked him to prove that if R and S were isomorphic rings and R was Gorenstein then S was Gorenstein and he simply did not know where to start. He said it was obvious.

[Kevin Buzzard]

Mathematicians are really good at this. What are we doing?

[Kevin Buzzard]

Is there some sort of univalence conjecture that one can formalise in Lean? Stating that for all structures in a certain typeclass this basic property of "being the same" manages to permeate through -- the correct notion of equiv.

[Kevin Buzzard]

There are two notions as well, I think: one a prop and one a type.

[Kevin Buzzard]

How does one formalise what I'm saying in Lean?

[Kevin Buzzard]

There's some sort of statement whose proof is "by pure mathematician's secret power"

[Kevin Buzzard]

it's our heavy rfl

[Kevin Buzzard]

and everyone always tells me to go and do HOTT. I just want someone to do it for me ;-) or at least tell me what I should be formalising.

[Kevin Buzzard]

I can quite believe that this is all very well understood by some people.

[Kevin Buzzard]

Is it some mathematician monad or something?

[Kevin Buzzard]

"they are the same to a mathematician, who works in ZFC but has made a solomn promise never to do anything naughty such as looking at elements of elements of groups in set theory"

[Kevin Buzzard]

You're in the typeclass of you're the kind of structure which a mathematician would find acceptable.

[Greg Conneen]

I don't know enough about Lean to formalise something like this, but I think cheeky way to circumvent this is start with the proposition above by @Floris van Doorn as the definition of isomorphic mathematical structures, rather than an axiom. However, I don't know that such a definition would lend itself to being useful to Lean.

[Kevin Buzzard]

Ask a research mathematician who doesn't know anything about schemes the following question: "Say X and Y are schemes, and X and Y are isomorphic. Say X is affine. Do you think Y is also affine?". They would answer "yeah, probably. "

[Greg Conneen]

I know very little about schemes, despite my advisor being an algebraic geometer. However, I can say beyond a shadow of a doubt that two isomorphic schemes would both be affine if one is.

[Greg Conneen]

That's not because I've run into this before; it's because I know how mathematicians use the word isomorphic

[Kevin Buzzard]

Because schemes have a certain public interface which is mathematician-acceptable; there's a topological space, there's a functor from the open sets, but there's definitely no looking at elements of the topological space -- those are "unopenable sets" -- I think they're more like terms in type theory (terms that aren't types).

[Kevin Buzzard]

It's our super-power!

[Kevin Buzzard]

I want to find out what our super-power is, because not having it is really inconvenient!

[Johan Commelin]

I think Voevodsky found it and made HoTT

[Kevin Buzzard]

But I want it in Lean

[Greg Conneen]

how much HoTT is in Lean?

[Kevin Buzzard]

And it's not an axiom, it's just a predicate on structures -- are you a mathematician-friendly structure?

[Kevin Buzzard]

how much HoTT is in Lean?

Let's find out. There is a HoTT library for Lean 3 and I have never even looked at it. Where is it?

[Greg Conneen]

Sounds like the place to start

[Floris van Doorn]

@Greg Conneen : the problem with doing that is Lean is that you will never be able to prove that two structures are isomorphic (except in very trivial cases). You won't be able to show that the free group on 1 generator and (ℤ,+) are isomorphic. You would need some axiom like univalence for that.

[Floris van Doorn]

There is a big Lean 2 library for HoTT. Lean 2 used to support HoTT, but that support was dropped in Lean 3.

[Floris van Doorn]

The Lean 3 HoTT library is here: https://github.com/gebner/hott3

[Greg Conneen]

Yeah, I figured that would happen. I knew that such a cheeky construction wouldn't lend itself easily to actually proving theorems, but as a mathematician it's a nice definition

[Floris van Doorn]

It basically avoids the use of Prop, ever, because that (or at least: certain parts of it) is inconsistent with univalence.

[Greg Conneen]

What? What parts of Prop are inconsistent with univalence? Now I'm very curious

[Sebastien Gouezel]

To me, this looks like first order logic statements about a structure. Assume you have a structure together with some language (in rings, this would be constants 0 and 1 and addition and multiplication). Then any proposition expressed solely in this language (with forall and exists quantifiers, and negation, and free variables, and so on), if true in a ring, is true in any isomorphic ring. The proof is completely algorithmic (push everything by your isomorphism, by induction over the length of the formula). This is a weaker notion than isomorphism, in general (really deep theorem: in the language of groups, the free groups over 2 generators and 3 generators satisfy exactly the same formulas -- but ℤ^2 and ℤ^3 don't, it is a nice exercise to find a formula distinguishing the two).

If you allow yourself more words in your language (such as ∈, or subsets, or things like that), then you can express more statements. But again everything is clearly invariant under isomorphism (and algorithmic, there is nothing mathematically hard in there). I don't see why there couldn't be a completely general tactic to push first-order statements by isomorphisms of the language under consideration, but since writing a transfer tactic is apparently hard I am certainly underestimating the difficulty.

[Floris van Doorn]

Well, univalence allows you to prove that there are two proofs of a certain equality that are unequal (for example, you can prove this for bool = bool, but that is not important for now). In Lean, any two proofs of an equality are definitionally equal (because they are proofs of a Prop), so stating univalence naively for eq in Lean will be inconsistent...

[Greg Conneen]

oh

[Greg Conneen]

OH

[Greg Conneen]

Yeah, that's no good.

[Floris van Doorn]

One thing you might try is define a new inductive type:

inductive hott_eq {α : Type u} (a : α) : α → Type
| refl : hott_eq a

It is exactly the same as eq, except that it lives in Type instead of Prop. Since it lives in type, proof irrelevance doesn't apply to it, so this should be consistent with univalence, right?
Alas, assuming univalence for this hott_eq is also inconsistent in Lean. The fact that you have a proof-irrelevant eq living in Prop lying around, allows you to prove that eq and hott_eq are equivalent (i.e. a = a' is in bijection with hott_eq a a' for all a, a'). So you can prove that hott_eq a a' is also a subsingleton. So univalence is also inconsistent for that.

[Chris Hughes]

I think one difficulty with the algorithm to do this, is that using the axiom of choice makes it difficult to prove

[Chris Hughes]

That it is a theorem about the structures.

[Kevin Buzzard]

so stating univalence naively for eq in Lean will be inconsistent...

That's because you're not using the right eq. You need to use mathematician's $=$ not your silly equalities that we don't understand or care about. That's the one you state univalence for.

[Chris Hughes]

For example trying to prove two isomorphic vector spaces have the same dimension, requires some non trivial maths, since dimension is defined by choosing a basis.

[Kevin Buzzard]

But if it were not true, then the definition of dimension would never have been born

[Kevin Buzzard]

There is some sort of gap here

[Kevin Buzzard]

Of course isomorphic vector spaces have the same dimension -- the proof is that vector spaces and dimensions are mathematical objects so isomorphism cannot change them. That's the definition of isomorphism.

[Kevin Buzzard]

Isomorphisms are the equivs that preserves mathematical predicates.

[Kevin Buzzard]

Where are these notions in Lean? This is still the easy stuff for us.

[Kevin Buzzard]

All of our objects come with some notion of isomorphism, and all of our predicates, when defined formally, are isomorphism-invariant.

[Edward Ayers]

There are some predicates that are not preserved over vector space isomorphism right? Eg, isomorphism between V and its dual but x ∈ V → x ∈ V* is false.

[Kenny Lau]

but \in is not in the language of vector spaces

[Kevin Buzzard]

There are some predicates that are not preserved over vector space isomorphism right? Eg, isomorphism between V and its dual but x ∈ V → x ∈ V* is false.

Ed!

[Edward Ayers]

Maybe I am just confused

[Kevin Buzzard]

Did you say $x\in V \implies x\in V^*$??

[Edward Ayers]

That is false right?

[Kevin Buzzard]

Ed -- that absolutely makes no sense at all.

[Kevin Buzzard]

That sentence is not allowed in maths mode

[Kevin Buzzard]

It's a stupid question, go away and do your problem sheets and come back with better questions.

[Kevin Buzzard]

Your question is not mathematics

[Kevin Buzzard]

You can only say that question in stupid things like Lean that allow you to do any old crap and define objects that we're not interested in.

[Kevin Buzzard]

The moment you write $x\in V$ you have decreed that the type of $x$ is $V$, so what you say afterwards doesn't make sense in maths mode because it doesn't even typecheck.

[Sebastien Gouezel]

In first order logic, x \in V does not make sense as x is not part of the language you are allowing yourself currently, i.e., the language of vector spaces (with addition, 0, scalar multiplication and so on).

[Kevin Buzzard]

It typechecks in ZFC, but that is an unfortunate coincidence, and it's part of our vow never to use the fact that it typechecks in ZFC.

[Chris Hughes]

There are some other grey areas. I think there's a generator function for a principal ideal in mathlib. This function isn't preserved under isomorphism, but maybe the things I do with it are.

[Kevin Buzzard]

This use of $\in$ when I put Ed's statement into maths mode is not the type theory usage of $\in$. This is mathematian's $\in$. It's the mathematician's version of :. Mathematicans use some weird variant of ZFC where they add some extra "mathematician-allowable types", and we only allow certain uses of $\in$ rather than all the ones strictly allowed in ZFC. We abide by some other unwritten rules. I think it might be interesting to formalise them in Lean.

[Kevin Buzzard]

but \in is not in the language of vector spaces

@Kenny Lau @Sebastien Gouezel can you explain this to me in Lean? I will understand it better then. If [vector_space V] then I can still talk about x : V. So I've managed to get hold of it somehow, and I surely need those terms when I'm making some fundamental definitions like the definition of a linear map between vector spaces

[Kevin Buzzard]

Actually, I do wonder whether I need the terms at all. I could just define a linear map to be a function from V to W that commuted with all the structure. I don't even need the terms. The identity element is just a map from unit to V. And don't get me started with punit -- we like to use unit. And everything can be in Type because we have a clever way of doing category theory called "proper classes", and it honestly all works because sometimes Brian Conrad or Peter Scholze all check.

[Kevin Buzzard]

Here is another issue -- Patrick, Johan and I are constantly complaining that we are having to prove X=X and we are battling against your stupid constructivist nonsense. Of course two terms of a subsingleton are equal, this is just noncomputable rfl

[Kevin Buzzard]

It took me ages to learn all the equalities that you type theorists have been offering to our community, but the fact that no mathematician has ever heard of any equality other than $=$ and the fact that this equality symbol in maths mode is currently not in Lean is a core reason why mathematicians find the software hard to use. I don't care if they're defeq or not -- this typeclass instance, or monad or whatever it is, is telling me that these two things are EQUAL which is the way mathematicians spell $=$ when trying and failing to explain it to computer scientists. I don't have time to change systems now, I just want to work in a place where objects are treated only via their interfaces

[Sebastien Gouezel]

but \in is not in the language of vector spaces

Kenny Lau Sebastien Gouezel can you explain this to me in Lean? I will understand it better then. If [vector_space V] then I can still talk about x : V. So I've managed to get hold of it somehow, and I surely need those terms when I'm making some fundamental definitions like the definition of a linear map between vector spaces

Let me explain what is the first order logic of a structure. You have some symbols, and you are only allowed to write formulas using these symbols and quantifiers and free variables. For instance, in the language of groups (with multiplication, neutral element and inverses), you can write the formula ∃x, ∀y, ∃z, y=z*z ∨ y = z*z*x. It is true in some groups, and not true in some other groups (this one is true in ℤ but not in ℤ^2, for instance). I claim that if such a formula is true in a group, it is obviously true in an isomorphic group (induction over the length of the formula, this is completely algorithmic). And this is not specific at all to groups: whatever structure with some language, isomorphisms will respect true formulas. You can add to your language more symbols such as ∈, or ⊆ and then you can express more statements but that they are still all respected with any notion of isomorphism.

Most mathematical statements can be expressed as first order statements of the structure under consideration if you allow yourself the right language. And with this point of view isomorphism invariance is obvious for all these statements.

[Fabian Glöckle]

@Kevin Buzzard I think deciding which parts of the implementation of a certain structure are allowed to be "used / unfolded" within a theory and which aren't, can't only be decided syntactically. What you are describing, is to my mind the human intelligence to have a higher level model of a structure apart from its technical implementation (the reals as a continuum, not as Dedekind cuts / equivalence classes of Cauchy sequences; this is also the reason why people rarely prove that different implementations of an idea are in fact equivalent).
There have been several attempts at trying to make the term "within the scope of a theory / respecting a theory" precise.
First order model theory, as @Sebastien Gouezel describes, defines a language for a structure; isomorphism is then what is compatible with all parts of the language.
Category theory allows us to create an abstract notion of morphism and says that valid constructions are only those which respect isomorphisms (in the sense of morphisms with a two-sided inverse).
I think it is because we check definitions for their compatibility with a theory that we consider the question "is a scheme which is isomorphic to an affine scheme affine?" tautological. But this already assumes "affine-ness" to be well-defined with respect to the theory of schemes.

[Kevin Buzzard]

Most mathematical statements can be expressed as first order statements of the structure under consideration if you allow yourself the right language.

I do not understand this at all. Here is the Wikipedia page on global dimension of rings. I claim that isomorphic rings have equal global dimensions. I once read the definition of the global dimension of a ring, but that was a long time ago and I have forgotten it. However I am still absolutely 100% mathematician-sure that isomorphic rings have equal global dimensions. How do you do this in first order logic? Where and how is all this extra structure being represented in Lean, and what properties does this extra structure have?

[Kevin Buzzard]

Can isomorphism of schemes be expressed in first order logic? Can isomorphism of topological spaces?

[Kevin Buzzard]

I don't even know what these questions mean.

[Kevin Buzzard]

I just want to see it in Lean, that's the only thing I understand properly.

[Chris Hughes]

Aren't most of the properties we care about not part of the first order structure? Could I do state something like 'the product of all elements of a finite monoid is 1'. This seems to involve proving some equivalence of properties between finset A and finset B, and any proof that this property is preserved will require induction on a list.

[Kevin Buzzard]

Here's a basic thing I don't understand. If I see the definition of a ring in Lean, I can correctly guess the definition of a homomorphism of rings, and as a consequence guess the definition of isomorphism. If I see the definition of a topological space, I cannot guess the definition of morphism (i.e. a computer can't) because there are two choices. If I see the definition of a partial order again there seem to be two choices: either a < b -> f a < f b or a < b <-> f a < f b. Both might be used in mathematics. But I can guess what an isomorphism is, and miraculously this canonical notion of isomorphism is independent of the choice I made for my morphisms. Some stuff is happening automatically and some stuff isn't. Oh! Is it not a typeclass but some sort of weird new tag controlled by a machine? Is this the hold-up? It has to be tags so it's fiddly as hell and most of us can't do it? I can't have a "mathematician-approved for isomorphisms" Prop-valued tag?

[Fabian Glöckle]

I claim that isomorphic rings have equal global dimensions. I once read the definition of the global dimension of a ring, but that was a long time ago and I have forgotten it. However I am still absolutely 100% mathematician-sure that isomorphic rings have equal global dimensions.

The moment you call it a "property of rings", you are asserting that this property respects ring-isos.

[Fabian Glöckle]

I can correctly guess the definition of a homomorphism of rings, and as a consequence guess the definition of isomorphism

I am currently writing a command which is supposed to do exactly this. Given a has_xyz, generate the type of functions respecting xyz

[Kevin Buzzard]

I know, but what I am saying is that there is nothing mathematically interesting that can be said about predicates on the type of all rings which are not "properties of rings", because we don't talk about such ugly predicates -- they are no use to us. But they can be made in Lean, unfortunately.

[Sebastien Gouezel]

Most mathematical statements can be expressed as first order statements of the structure under consideration if you allow yourself the right language.

I do not understand this at all. Here is the Wikipedia page on global dimension of rings. I claim that isomorphic rings have equal global dimensions. I once read the definition of the global dimension of a ring, but that was a long time ago and I have forgotten it. However I am still absolutely 100% mathematician-sure that isomorphic rings have equal global dimensions. How do you do this in first order logic? Where and how is all this extra structure being represented in Lean, and what properties does this extra structure have?

This one is hard to express in first-order logic as it is quantifying over all A-modules. To me, it is not obvious even from a mathematical point of view. Think of a ring R in some universe u, and some other ring S in some universe v, which are isomorphic. Maybe it is possible to construct in universe v some S-module which has no analogue in universe u (maybe because its cardinality is larger than any set in universe u), and this S-module is precisely the one that plays a role in the definition.

On the other hand, for most properties which are obviously invariant from the definition (being principal or Euclidean, say), this can be expressed in first-order logic.

[Kevin Buzzard]

I think that definitional type equality should be banned and replaced with mathematical equality of mathematical structures.

[Kevin Buzzard]

Sebastien I am most definitely happy to restrict to objects in one universe. Mathematicians never need any more in practice, right?

[Kevin Buzzard]

I think a better example schemes. Let's do them. How do you express schemes in first order logic? A scheme is a topological space equipped with a functor from some (small) category made from the open sets to the (large) category of rings, plus some axioms that need not concern us but which I can assure you can be written in maths mode.

[Kevin Buzzard]

And I want to prove that if S and T are isomorphic schemes and S is Noetherian then T is Noetherian.

[Kevin Buzzard]

This is a baby example -- this is only MSc. Perfectoid spaces are much more complicated objects. But I can guarantee the purity of the make, because they were made by mathematicians. Can I do this in first order logic? Can I do this in Lean?

[Sebastien Gouezel]

If you try to write down the definition of noetherian unfolding everything, you will see it boils down to a complicated formula with a lot of quantifiers but just involving the objects you are working with. So this is definitely a first order formula in the appropriate language, yes.

[Sebastien Gouezel]

Of course, I am not expecting you to unfold everything by hand, a computer can do this much better than you!

[Kevin Buzzard]

I can correctly guess the definition of a homomorphism of rings, and as a consequence guess the definition of isomorphism

I am currently writing a command which is supposed to do exactly this. Given a has_xyz, generate the type of functions respecting xyz

What will you do for topological spaces and for binary relations? How many choices do you have for the homomorphisms? What about the isomorphisms though? Do you agree that there are two different questions here -- generating morphisms and generating isomorphisms i.e. generating the groupoid associated to the structure.

Do you see any difference between bundled and unbundled objects? In a parallel universe Lean could have had bundled groups. Just one type! It would have looked something like this:

structure Group :=
(G : Type) -- or Type*, I don't care, but putting in the star makes it harder work
(mul : G -> G -> G)
(one : G)
(one_mul : forall g : G, mul one g = g)
...

[Kevin Buzzard]

If you try to write down the definition of noetherian unfolding everything, you will see it boils down to a complicated formula with a lot of quantifiers but just involving the objects you are working with. So this is definitely a first order formula in the appropriate language, yes.

So there is a "first order language of schemes"? Even though schemes involve something which can't be done in Isabelle within its typeclass framework?

[Fabian Glöckle]

I think the category theory approach about defining morphisms as stronger than the first order approach
(because at some point, the tools for moving parts of structures back and forth become higher-order, think of sheaf pullbacks in morphism definitions)

[Fabian Glöckle]

And I think the correct order is "define morphisms" -> "isomophisms as morphisms with a two-sided inverse" -> "everything that respects isomorphisms is a sensible definition"

[Fabian Glöckle]

What will you do for topological spaces and for binary relations? How many choices do you have for the homomorphisms? What about the isomorphisms though? Do you agree that there are two different questions here -- generating morphisms and generating isomorphisms i.e. generating the groupoid associated to the structure.

Okay I understand what you are saying. But then if I think about two different foundational systems for mathematics, the associated groupoids of a structure can be "different" (whatever that means). From a metamathematical point of view, asking about how the groupoid looks is not well-defined. Hence the decision for the univalence axiom to compress it as much as possible (to the hott_eq groupoid).

[Chris Hughes]

What is a first order statement about groups? I thought anything involving Pi (x : Pi _) was no longer first order. Is this correct?

[Sebastien Gouezel]

It depends on the language you are allowing. Second order statements are first order for an extended language. A first order statement in the classical sense is: ∃x, ∀y, ∃z, y=z*z ∨ y = z*z*x. A second order statement in the classical sense, which becomes first order if you allow quantification over sets, is the following: there is a finite subset that generates the group (written suitably with quantifiers).

[Sebastien Gouezel]

Do you see any difference between bundled and unbundled objects?

I guess a good transfer tactic would unbundle everything, write everything in first order form, transfer everything, and then rebundle it.

[Kevin Buzzard]

If you showed a mathematician a definition of a pushforward of sheaves (that's called $f_*\mathcal{F}$ in maths and sheaf.map f in Lean) they would agree that it was pretty canonical. On the other hand you could also imagine some far more stupid definitions (e.g. just send everything to the zero sheaf). Here's a question. Let $\mathcal{C}$ denote the category of sheaves of abelian groups on a topological space $X$ and let $\mathcal{D}$ denote the category of sheaves of abelian groups on $Y$. If I give you a continuous map $f:X\to Y$ then I claim that there is a $canonical$ functor from $\mathcal{C}$ to $\mathcal{D}$, namely the pushforward. One has to be careful here -- this construction seems to be giving some sort of "functor" from a category to some sort of two-category; I say "functor" because F(fg) and F(f) o F(g) are perhaps only canonically isomorphic rather than equal.

[Mario Carneiro]

I agree with Fabian that the meaning of "predicate on rings" is that it is a predicate that respects ring isomorphism. There is a generic mechanism for producing isomorphisms (not homomorphisms) on first order structures, and I believe it extends to higher order as well (so that topologies are also applicable and so on). I think it's best to define these manually though, since we care how it's expressed.

I want to reiterate an example Chris gave, which demonstrates the important fact that some structure preserving predicates contain subterms that are not structure preserving. dim V is the cardinality of a basis of V. This is a structure preserving predicate, but the reason this is a deep proof is because it is formed out of a non-structure preserving function "a basis of V" (i.e. choice (exists basis of V)). An arbitrary vector space isomorphism will not take choice (exists basis of V) to choice (exists basis of W), because there is no connection between these bases (unless V = W in lean). There is a particular isomorphism that preserves this, but that's not what a "vector space property" means.

[Kevin Buzzard]

But rfl++ should still prove that if V and W are isomorphic then their dimensions are equal.

[Kevin Buzzard]

I don't care if there's content -- it's math-trivial.

[Kevin Buzzard]

dimension has some "I am isomorphism-invariant" tag

[Kevin Buzzard]

it just took some work to get it there

[Mario Carneiro]

yes, that's transfer

[Sebastien Gouezel]

If you define "dimension" as the maximal cardinality of an independent subset, yes, rfl++ should prove it. If you defined it as "take the cardinality of some random basis", then the statement that is is invariant under isomorphism is non-trivial.

[Mario Carneiro]

it relies on "I am isomorphism invariant" tags to build such proofs for first order statements (like other properties you want this tag on)

[Mario Carneiro]

The problem is not that transfer doesn't work, it's that nothing has these tags right now so transfer doesn't know what to do

[Kevin Buzzard]

If you define "dimension" as the maximal cardinality of an independent subset, yes, rfl++ should prove it. If you defined it as "take the cardinality of some random basis", then the statement that is is invariant under isomorphism is non-trivial.

The mathematician in me wants to say that it is a theorem that the max cardinality of an independent subset is equal to the cardinality of a random basis, and I appreciate that this needs to be proved in a good API. However my point is simply that however the definition of dimension is made in Lean, a good API should have the result that it is isomorphism-invariant. Does this make people more inclined towards one definition than the other?

[Sebastien Gouezel]

I definitely prefer the definition as the maximal cardinality of a linearly independent subset, as it is obviously isomorphism-invariant, contrary to the definition "take the cardinality of a basis found using choice".

[Chris Hughes]

Do you have the same problem deep down though, since "cardinals have supremums" is presumably proven with choice?

[Sebastien Gouezel]

Even if some choice is involved, it will be the same choice over both sides of the isomorphism, i.e., choice over the same set of cardinals. Hence, it should give the same result (choice is an unpredictable but deterministic function: give it the same argument, it will give the same conclusion). At least if you don't change universes.

[Kevin Buzzard]

I'm happy not to change universes. Mathematicians don't really need universes for most of what we do.

[Mario Carneiro]

Actually dim V in mathlib is defined in that way - it is the minimum cardinality of any basis for V, so it is "manifestly invariant" provided you can show that the set of basis cardinalities is preserved under isomorphism

[Mario Carneiro]

I recall thinking about whether to extend the definition to modules, but I think it isn't clear whether the min or sup is preferred in that case

[Kevin Buzzard]

Free modules over a nonzero ring have a well-defined dimension, it's interesting that Mario says it's not clear what the best definition is, the theorem that if R^a injects into R'b then a<=b is tricky even for a, b finite. But if R^b surjects onto R^a then just tensoring up to a residue field shows b>=a

[Kevin Buzzard]

Tensoring with a fixed thing preserves surjections but not injections -- it's right exact but not left exact

[Kevin Buzzard]

I always thought that inequality situation was a strange asymmetry

[Mario Carneiro]

I should preface this by saying it's been a while and I've forgotten the results of my research. I see that dim is only defined for vector spaces so apparently I gave up

[Kevin Buzzard]

Of course we just prove that they're the same and then who cares what the definition is, it's both.