Free stuff

Stream: maths

[Adam Topaz]

I'm wondering about the recent PR #4077 and the related #4079 and #4078 that @Scott Morrison made.

I'm mainly wondering about the design choices here. Namely, the free $R$-algebra on a type $S$ is the $R$-tensor-algebra on the free module generated by $S$, whereas these PRs construct the tensor algebra as a quotient of the free algebra. Certainly I think the constructions of the free module and free algebra should interact, but the question is, in which way. With the PRs mentioned above, it would not be immediate that the free algebra is the tensor algebra of the free module, but what would be immediate is that the tensor algebra is a quotient of the free algebra.

A related question: We could take the approach from these PRs even further -- we can define the free $R$-algebra on a type $S$ as a quotient of the free (semi)ring on generated by the disjoint union of $R$ and $S$. Does it make sense to do this? I certainly think it is important to have some consistency in the way such free objects are constructed, and the "top-down/make the free-est thing possible first" approach might be a way to make everything more uniform.

[Adam Topaz]

All of these things should really be constructed by some metapprogram that looks at the equations and universal axioms of the objects involved a la universal algebra. And the approach taken by these PRs is presumably how such metaprograms would operate in practice.

[Kevin Buzzard]

@Kenny Lau @Chris Hughes what do you think?

[Adam Topaz]

One more thing to note: the previous construction of the tensor algebra was already as a quotient of some gigantic free thing with no relations, so the refactoring that Scott did in those PRs definitely makes sense.

[Chris Hughes]

I think that with most of these free objects, the universal property on its own is not that useful, and there is usually some other construction that tells you more about the object. E.g. It is hard to define the coefficient or degree of a polynomial directly from the universal property. I've been working with free groups lately, and some theory depends on induction on the length of a normalised word.

If you do use universal algebra to define these objects then you probably end up having to effectively prove isomorphism with some other construction to prove any non trivial theorem about the object.

[Chris Hughes]

I think it would be handy for a universal algebra to be able to deal with equational theories that aren't type classes, e.g. Rings with a root of a particular polynomial. I think maybe avoiding meta code for the bulk of the theory might be a good idea for this reason, and have a small amount of code to turn a structure like group into the appropriate term of a non-meta type equational_theory or something like that.

[Adam Topaz]

Of course, I agree that in the "usual" cases from algebra it's more useful to have a concrete construction of the free objects. But this is really an "accident" of the construction, and usually does not generalize.

[Adam Topaz]

Induction on the length of a normalized word in a free group is a good example.

[Adam Topaz]

Concerning metaprogramming, I think to make it actually useful you would need some code to go in both directions -- from classes like group to equational_theory, and some code to go from some equational theory thing back to a typeclass. This would let you carry out whatever general constructions you need in the universal world, and pass back to the concrete world if necessary

[Chris Hughes]

I agree that the concrete constructions can't be generalised, that's why I'm slightly skeptical that it would be useful to attempt to generalise free objects. I disagree that these are "accidents", it's almost the whole point of distributivity that the free commutative ring is also the free abelian group over the free monoid. Similarly the whole point of associativity is that free monoids are list. This is a slightly meaningless discussion I know.

[Adam Topaz]

I envision a world where I can write the following and have the class monoid generated for me, as well as code for free monoids, colimits of monoids, etc.

namespace monoid
def ops : list expr :=
  [ (one, 0),
    (mul, 2) ]

def axioms : list expr :=
  [ (mul_assoc, ∀ a b c, mul a (mul b c) = mul a (mul c b)),
    (one_mul, ∀ a, mul one a = a),
    (mul_one, ∀ a, mul a one = a) ]

run_cmd make_alg ops axioms
end monoid

[Reid Barton]

I think @Jacques Carette is working on a prover-independent version of this.

[Reid Barton]

I haven't had a chance to check it out yet though.

[Chris Hughes]

I would do it very similarly to this, but with a custom, non-meta expr

[Adam Topaz]

@Colter MacDonald and I did some non-meta stuff like this here: https://github.com/adamtopaz/UnivAlg
I still don't know how to make it actually useful.

[Adam Topaz]

I also dream of a world where I can write this:

namespace ring
def ops := monoid.ops ++ add_comm_group.ops
def axioms := monoid.axioms ++
  add_comm_group.axioms ++
  [ (left_distrib, ...), (right_distrib, ...) ]
run_cmd make_alg ops axioms
end ring

and have lean generate code for monoid rings, etc.

[Johan Commelin]

@Fabian Glöckle had written quite a bunch of meta code like that.

[Johan Commelin]

It could generate ring_hom and the category Ring from the lean code of ring

[Johan Commelin]

And similarly for the rest of the algebraic hierarchy.

[Adam Topaz]

Oh cool! Is there a repo somewhere?

[Chris Hughes]

The stuff I'd most like to see universal algebra do is develop my whole subobject library for me. I think that there's an awful lot of random little theorems about subobjects and quotients etc. that apply in a broad setting.

[Johan Commelin]

@Fabian Glöckle is your code available somewhere?

[Patrick Massot]

I've written several times that I think such things are a key component of the future of proof assistants, together with more proof automation. See also https://hal.inria.fr/hal-02478907v5

[Patrick Massot]

We should have human readable input files generating class and structures definitions, handling all the variations around binding, extending or parametrizing correctly etc.

[Jacques Carette]

We (my student Yasmine and I) are definitely working on this. I can see how open she'd be to targetting Lean. It's in scope, for sure, but she's also hoping to finish her Ph.D. this term, so...

[Jacques Carette]

Having the input files being human-readable, as @Patrick Massot mentions, is very important. I also think that the output should be human-readable too, as the aim is for human-based reuse. It turns out that that is not so hard [see my work on GOOL for a very concrete example.]

[Jacques Carette]

What I'm still looking for is a good list of what we should be generating. We have a long list of things we can generate, but I'm quite sure that 1) it's missing useful things, 2) it has useless things on it.

[Johan Commelin]

Can we see the list that you have? Or is that nontrivial?

[Jacques Carette]

Hmm, I can't upload a PDF to here, can I? There was a decent list on Yasmine's slides for her talk about our work at CICM 2020.

[Jacques Carette]

Let me try to cut-and-paste from it...

Signature, Product Algebra, Basic Term Language, Homomorphism, Closed Term
Language, Open Term Language, Evaluator, Simplication rules, Staged terms, Finally
tagless representations, induction principle, Relational Interpretation, Monomorphism,
Isomorphism, Endomorphism, Congruence relation, Quotient algebra, Trivial
subtheory, Flipped theory, Monoid action, Monoid Cosets, composition of morphisms,
kernel of homomorphisms, parse trees.

[Johan Commelin]

Aha... (you can upload PDF's btw)

[Johan Commelin]

See the :paperclip: below the input box where you write posts.

[Jacques Carette]

slides-1.pdf

[Jacques Carette]

Indeed I can! Slide 16. But it's perhaps better seen in context.

[Jacques Carette]

There is another list in her PhD proposal (https://github.com/ysharoda/PhD-Proposal). It has lots of overlap, but it is a different set.

[Reid Barton]

If you already target at least one similar language (Agda or Coq) then it might make sense for Lean/mathlib people to work on the Lean target--as you can see there's no shortage of people who would be interested.

[Jacques Carette]

We are actively targeting Agda.

[Jacques Carette]

Having some Lean/mathlib person who is Haskell-literate (our host implementation language for our infrastructure) would be fantastic.

[Scott Morrison]

Getting back to the current PRs --- one change I've made here is marking things as irreducible at the end of the file. So hopefully it will be a moot point whether we define tensor_algebra as a quotient or as a free construction.

Nevertheless, I agree we should add sometime the isomorphism between these two ways of building tensor_algebra (and the compatibility of that isomorphism with the \iota and lift).

[Adam Topaz]

Sorry, the discussion wandered a little bit :)

[Scott Morrison]

It wandered it very appealing directions! We want all this stuff, of course.

[Scott Morrison]

I've added free_algebra R X ≃ₐ[R] monoid_algebra R (free_monoid X) to #4077.

[Chris Hughes]

Why have both constructions in the first place if they're isomorphic?

[Scott Morrison]

Because it's a hassle to have to think of a free algebra in this way?

[Scott Morrison]

Maybe this is dumb, I'm really not sure.

[Scott Morrison]

I was actually tempted just now to go even further in the same direction --- define free_module R X, even though it is isomorphic to X \to\_0 R, just to protect me from having to look at the finsupp API. :-)

What I actually want at the moment is to know that I can construct a linear map out of a free algebra by specifying its values on elements of free_monoid X.

Options:

1. use free_algebra R X ≃ₐ[R] monoid_algebra R (free_monoid X), and then unfold the definition of monoid_algebra in terms of finsupp, and muck around with finsupps by hand
2. use free_algebra R X ≃ₗ[R] free_module R (free_monoid X) (doesn't exist), and use free_module.lift (also doesn't exist) to do the construction, without ever having to know that finsupp was involved.

[Chris Hughes]

Sounds like the finsupp API isn't very good. finsupp is so close to free_module already that we shouldn't need to redefine it. It can't be that hard to define the UMP of free modules on finsupp using the UMP of finsupp right? Isn't it supposed to make it easier to have that API available? I don't see why it's good to not have to know finsupp was involved; it has almost exactly the property you want.

[Reid Barton]

Jacques Carette said:

What I'm still looking for is a good list of what we should be generating. We have a long list of things we can generate, but I'm quite sure that 1) it's missing useful things, 2) it has useless things on it.

I tried to assemble a list without looking at yours too closely. I'll fix "group" as the theory in question for concreteness.

• Definition of a group.
• Definition of group homomorphisms, group isomorphisms.
• Products of groups (nullary (p)unit and binary prod, as well as indexed Pi)
• Definition of a subgroup. A subgroup also forms a group, with a group hom to the original group. Image and preimage of a subgroup under a group hom. Subgroup generated by a subset.
• Definition of a congruence. The quotient by a congruence forms a group, with a group hom from the original group. Image(?) and preimage of a congruence under a group hom. Congruence generated by a relation.
• Free group on a set, along with its associated structure: a function from a set to a group extends uniquely to a group hom from the free group; the free group on a group has an "evaluation" map back to the group; the free group is functorial in the group; etc.

Along with these come many lemmas, e.g. "the subgroup generated by a subgroup is the original subgroup" and "if two group homomorphisms agree on a subset, they agree on the subgroup generated by that subset".

[Adam Topaz]

I would add the "groupification" of a monoid as well (i.e. the left adjoint to the forgetful functor from groups to monoids).

[Kevin Buzzard]

If you allow "subgroup generated by" then you probably want that there's a Galois insertion between set and subgroup?

[Reid Barton]

Then there are statements in category theory, for example

• monomorphisms in Grp are the injective functions,
• Grp is a cocomplete, even locally presentable category,
• Grp is monadic over Set,
• the forgetful functor Grp -> Set preserves filtered colimits,

etc. This list is basically endless, so I suggest the following approach.
Inside the target theorem prover, we can also do universal algebra and prove all these statements for categories of models of algebraic theories of various sorts. So, we can generate a representation of the theory internal to the target language, e.g., as a handful of (inductive) types describing the function symbols, equations, etc. of the theory. Then, your system would emit the following:

• The category Grp, defined directly in terms of the notions of "group" and "group homomorphism" from above.
• The (faithful) forgetful functor Grp -> Set (in the case of a single sorted theory), making Grp into a concrete category.
• Some data G that describe the theory of groups together with an equivalence of concrete categories between Grp and Alg G, where Alg is something defined once and for all in the target language.

Then the target library (mathlib, say) can go off and prove things about monads, Lawvere theories, sketches, first order logic, whatever as it pleases, decoupled from your system.
Now, it could happen that we actually want a tighter integration, say to know that the objects of the Lawvere theory for groups really are literally free_group (fin n) or something, but this seems like a reasonable place to start.

[Reid Barton]

Kevin Buzzard said:

If you allow "subgroup generated by" then you probably want that there's a Galois insertion between set and subgroup?

Right, I guess this more or less qualifies as "lemmas" given what I listed, but it's good to mention it specifically.

[Reid Barton]

Adam Topaz said:

I would add the "groupification" of a monoid as well (i.e. the left adjoint to the forgetful functor from groups to monoids).

This arises from some kind of morphism between theories--what to generate for those is a separate and probably more interesting list.

[Adam Topaz]

I think even the question of how to write down a "morphism between theories" is an interesting one.

[Chris Hughes]

There's a rigorous notion of morphism between Lawvere theories right? It basically boils down to a way of defining the operations of structure X in terms of the operations of structure Y.

[Adam Topaz]

Yeah, it's just a functor that preserves finite products.

[Adam Topaz]

But once the system defines free objects, that already defines the corresponding monad, at least on objects.

[Adam Topaz]

The morphisms between theories are then "just" morphisms of monads.

[Reid Barton]

Or you can say a morphism of theories is an adjunction between locally presentable categories. But these are not syntactic descriptions.

[Chris Hughes]

There's such a thing as a multi-sorted Lawvere theory right? Are these worth doing? It might be handy to have stuff like morphism of groups that preserve an action on a particular set.

[Adam Topaz]

Yeah, certainly two-sorted things are important if you want modules :)

[Adam Topaz]

I think the main challenge in this abstract approach (using monads or Lawvere theories, for example), is to generate the moprhism of theories when you recognize that it should exist, for example going from groups to monoids.

[Chris Hughes]

Use type class inference? Inspect group.to_monoid.

[Adam Topaz]

In the universal algebra repo I mentioned above, I defined a language L as a function from N to Type*, and rules as a relation on some inductive gadget built out of a language. A "morphism" of theories was then a function L1 n \to L2 n for every n, such that the induced map on the inductive gadget gave an implication on rules. This is not the most general thing you can do, since you can have two pairs of languages/rules which give the same theory.

[Adam Topaz]

Chris Hughes said:

Use type class inference? Inspect group.to_monoid.

I think the point is that we want some metacode to generate the classes group and monoid, and to also be able to notice, for example, that group should extend monoid.

[Patrick Massot]

Don't forget that all this discussion is only about the trivial example (only one type involved). The first interesting case is module over a (semi)ring. This is where beginners (and not so beginners) get confused about parameters vs extension etc.

[Kevin Buzzard]

Will all this help with sheaves of modules over a sheaf of rings?

[Adam Topaz]

Sure, replace $Set$ with a sheaf topos and you're good.

[Adam Topaz]

On a more serious note, all this universal algebra stuff can, in principle, help in defining (and working with) internal algebraic objects in categories.

[Kevin Buzzard]

Adam Topaz said:

Sure, replace $Set$ with a sheaf topos and you're good.

I might get a bit confused about parameters vs extension

[Reid Barton]

Kevin Buzzard said:

Will all this help with sheaves of modules over a sheaf of rings?

What kind of help are you looking for?

[Johan Commelin]

I guess he doesn't want to manually duplicate the entire (constructive part of the) API

[Reid Barton]

What API though?

[Kevin Buzzard]

What I meant was "I cannot even formalise the statements of the theorems I want to work on, because we do not have the definition of a sheaf of modules over a sheaf of rings in mathlib as far as I know".

[Johan Commelin]

• Definition of a sheaf of modules.
• Definition of sheaf of module homomorphisms, sheaf of module isomorphisms.
• Products of sheaf of modules (nullary (p)unit and binary prod, as well as indexed Pi)
• Definition of a subsheaf of modules. A subsheaf of modules also forms a sheaf of modules, with a sheaf of module hom to the original sheaf of module hom. Image and preimage of a subsheaf of module hom under a sheaf of module hom.
• ... <snip>

[Reid Barton]

I mean, as all automation, I don't think it's going to help with something that there are currently 0 examples of

[Reid Barton]

at least it can't help you until after you've gone and written example 1

[Kevin Buzzard]

Sorry, where am I looking? I can't find sheaf of modules in the docs, in mathlib or in the PR's.

[Johan Commelin]

That's exactly Reid's point.

[Kevin Buzzard]

If M is an R-module, I bet I can make a sheaf of modules on Spec(R).

[Reid Barton]

Johan Commelin said:

• Definition of a sheaf of modules.

Already there are many possibilities for this definition

[Kevin Buzzard]

Right, and I can't prove that the category of sheaves of modules on Spec(R) is equivalent to R-mod because I can't currently state it.

[Reid Barton]

It seems that the approach used to define ringed spaces won't extend easily, because the value of a sheaf of modules on an open set U is an object in a category that depends on U.

[Kevin Buzzard]

Anyway, that was what I meant by "will all this abstract stuff help".

[Johan Commelin]

But it could be a sheaf of abelian groups + extra data expressed in a non-categorical manner.

[Reid Barton]

It could be but then it's hard to see how to generate that description from the theory of a module over a ring written in the first-order style that we use in mathlib and presumably would have in the abstract definitions of theories as well.

[Reid Barton]

Of course the real point of a ring is that it's a monoid object in $(\mathrm{Ab}, \otimes)$ (or maybe in the associated multicategory) but we don't have this information in mathlib AFAIK.

[Adam Topaz]

I mentioned the following code in the status of schemes thread we were in a little while ago.

import algebra
import topology.sheaves.local_predicate

open Top
open topological_space
universe v
variables {X : Top.{v}}
variables (T : X → Type v) (S : X → Type v)

structure local_ring_predicate [Π (x : X), ring (T x)] extends local_predicate T :=
(is_subring : ∀ {U : opens X}, is_subring (pred : set (Π (x : U), T x)))

structure local_module_predicate [Π (x : X), ring (T x)] (A : local_ring_predicate T)
  [Π (x : X), add_comm_group (S x)] [Π (x : X), module (T x) (S x)] extends local_predicate S :=
(is_submodule : sorry) -- is_submodule doesn't exist in mathlib, but you get the idea.

This approach should presumably work in the universal case as well.

[Adam Topaz]

Assuming the metacode produces is_subfoo classes...

[Adam Topaz]

local_ring_predicate should be read local_(ring_predicate) and not (local_ring)_predicate

[Reid Barton]

I think this is addressing a slightly later question--here the issue is how to represent even the data of a sheaf of modules

[Adam Topaz]

A sheaf of modules is a local_module_predicate satsifying some gluing axioms.

[Reid Barton]

Hang on, I don't know what a local_predicate is.

[Reid Barton]

I guess I'm confused by the language. Surely what a sheaf of modules is is the stuff that comes earlier: [Π (x : X), add_comm_group (S x)] [Π (x : X), module (T x) (S x)]

[Reid Barton]

maybe together with some more stuff

[Reid Barton]

This isn't how I'm used to thinking about things

[Adam Topaz]

This comes from the representation of a sheaf as a subpresheaf of the rule sending $U$ to $\Pi (u : U), T u$.

[Adam Topaz]

Where you are meant to think of $T u$ as some set which contains the stalk of the sheaf at $u$.

[Adam Topaz]

The local_predicate thing is essentially saying that this gives you a presheaf, and there is another structure which ensures the sheaf axiom.

[Adam Topaz]

Errr sorry, in mathlib local_predicate is satisfies the sheaf axiom, but there is also a prelocal_predicate which gives you presheaves.

https://github.com/leanprover-community/mathlib/blob/0c57b2da3c4e821fb2e1e351409e61e039fd7ea6/src/topology/sheaves/local_predicate.lean#L87

[Reid Barton]

So if I have an open set $U$ how do I get out the $\mathcal{O}_X(U)$-module?

[Adam Topaz]

it's the subset of $\Pi (x : U), T u$ given by the local predicate.

[Adam Topaz]

Hence the is_submodule

[Adam Topaz]

If $\mathcal{M}$ is a sheaf of modules over $\mathcal{O}$ then $\prod_{u : U} \mathcal{M}_u$ is a module over $\prod_{u : U} \mathcal{O}_u$.

[Reid Barton]

I guess to me this seems more like a way of avoiding answering the question of what is a sheaf of modules

[Adam Topaz]

Reid Barton said:

I guess to me this seems more like a way of avoiding answering the question of what is a sheaf of modules

I don't disagree, but what's the alternative aside from working internally in the sheaf topos?

[Johan Commelin]

Well, there is the hands-on definition. (A sheaf of modules over O is a sheaf M, + for each U an add-group structure on M U and a O U-module structure on M U.

[Adam Topaz]

Yes of course, but I think this would be harder to automate

[Adam Topaz]

You also need all the restriction maps to be morphisms in the correct category, etc

[Kevin Buzzard]

Ramon Mir used an extremely hands-on definition when making schemes for his MSc project last year, and then Kenny went on to prove things like Gamma-Spec adjointness using this definition. However, when Ramon went to port his stuff to mathlib he discovered that Scott had already put the definition of a presheaf in, and it used categories (which Ramon didn't), so we decided to wait.

[Reid Barton]

Another option is to define the tensor product of presheaves of abelian groups (ideally, also of sheaves by applying sheafification) and say a sheaf of modules is a module object over the monoid object that is a sheaf of rings

[Reid Barton]

Another option is to consider the (pseudo)functor Mod(O_X(-)) : opens X -> Cat and define a sheaf of modules to be some kind of enhancement of a sheaf to the category of lax sections of this functor

[Reid Barton]

Anyways the issue here seems to be that we don't know what we want the definition to be, not an automation problem.

[Reid Barton]

Probably the right thing to do is to go look up how Lurie defines sheaves of modules in SAG.

[Adam Topaz]

Looks like Lurie defines sheaves of abelian groups, he then defines sheaves of rings as monoid objects there, and modules as (internal) modules over those monoid objects.

[Adam Topaz]

Definition 2.1.0.1 here https://www.math.ias.edu/~lurie/papers/SAG-rootfile.pdf

[Adam Topaz]

I'm happy with that, but I was under the impression that people wanted to avoid the internal definitions.

[Adam Topaz]

But this definition does have an automation problem if you define sheaves of abelian groups as sheaves $\mathcal{A}$ such that for every open $U$, $\mathcal{A}(U)$ has an abelian group structure, such that blah blah blah, and then you go and define sheaves of rings as something internal to the category of sheaves of abelian groups. How would you tell the computer to decide to define sheaves of abelian groups "externally" like above, while defining sheaves of rings internally to the corresponding category of abelian sheaves?

I thought the whole point of this discussion was to tell the computer: "Here are the operations and axioms for an abelian group, here are the operations and axioms for a ring, and here is how to forget the ring structure to get an abelian group, now go and make me some categories of sheaves".

[Reid Barton]

I guess this gets back to my original question as well then. I don't understand what there is to automate. Don't we already have sheaves of abelian groups, which we could presumably make into a monoidal category, and monoid objects in a monoidal category, and modules over them (I'm not sure if they exist yet, but they are no harder than monoid objects)?

[Adam Topaz]

I was envisioning automating the creation of sheaves of foo where foois any (possibly multi-sorted) Lawvere theory (or variety in the sense of universal algebra, or ...).

[Adam Topaz]

But maybe this just amounts to making sheaves valued in categories with enough colimits, and automating the creation of such categories from universal algebra.

[Reid Barton]

This is somehow easier, right? This occurred to me as well--there's some category of "rings plus modules over them"; and a sheaf of modules over a sheaf of rings is a sheaf of one of those.

[Adam Topaz]

Yeah, you can look at the category of pairs $(R,M)$ where $R$ is a ring and $M$ is an $R$-module, with the obvious morphisms.

[Adam Topaz]

I don't know if @Patrick Massot would be happy with that approach.

[Kevin Buzzard]

That's an interesting approach!

[Kevin Buzzard]

A sheaf of modules is a dependent sheaf, so surely dependent type theory should just love them :-)

[Reid Barton]

It sounds pretty awkward to formulate statements like "O_{Spec R}-mod is equivalent to R-mod" in this language, though

[Reid Barton]

Well that's the thing. Dependent type theory loves them, which is why the hands on approach didn't run into any of these questions.

[Adam Topaz]

You need to work with the "forgetful functor" from this category to the category of rings.

[Reid Barton]

For the category theory version you would need consider some kind of "dependent functor", which is essentially the idea of
Reid Barton said:

Another option is to consider the (pseudo)functor Mod(O_X(-)) : opens X -> Cat and define a sheaf of modules to be some kind of enhancement of a sheaf to the category of lax sections of this functor

[Reid Barton]

Using sheaves of pairs $(R, M)$ is the analogue of getting rid of dependent types by using a Sigma type

[Kenny Lau]

then you start getting equality of types

[Reid Barton]

Yes, or you could insert an isomorphism--that is where things start to get awkward

[Adam Topaz]

I tried playing with this idea a bit. Even the "dependent functor" idea gives trouble. See the two sorry's below.

import category_theory.category.Cat
import algebra.category.CommRing
import algebra.category.Module.basic

open category_theory

def restrict_scalars {A B : Ring} (f : A ⟶ B) : functor (Module B) (Module A) :=
{ obj := λ M,
  { carrier := M,
    is_add_comm_group := by apply_instance,
    is_module :=
    { smul := λ a m, f a • m,
      one_smul := by simp,
      mul_smul := λ a b m, by {change (f _) • _ = _, rw ring_hom.map_mul, apply mul_smul },
      smul_add := λ a m n, by {change (f _) • _ = _, apply smul_add },
      smul_zero := by simp,
      add_smul := λ a b m, by {change (f _) • _ = _, rw ring_hom.map_add, apply add_smul },
      zero_smul := by simp }},
  map := λ M N g,
  { to_fun := g,
    map_add' := g.map_add,
    map_smul' := λ a m, by rw g.map_smul } }

def Mod : functor Ringᵒᵖ Cat :=
{ obj := λ A, Cat.of $ Module A.unop,
  map := λ A B f, restrict_scalars f.unop,
  map_id' := sorry, -- oh no!
  map_comp' := sorry }

[Reid Barton]

I think you'd want to use pseudofunctors anyways

[Adam Topaz]

Yeah for sure.

[Reid Barton]

although this is probably not that bad to prove

[Adam Topaz]

Yeah, but the fact that tidy didn't even get the map_id field was a bad sign.

[Adam Topaz]

By the way, does mathlib have the restriction of scalars functor above for possibly noncommutative rings?

[Adam Topaz]

I know there is restriction of scalars for algebras, but that assumes some commutativity.

[Adam Topaz]

Ha. tidy is happy with the second sorry.

[Reid Barton]

yep, with eta for structures, the first would be okay too

[Reid Barton]

at least, I think it would? I guess this is a level up from the usual situation

[Reid Barton]

namely, composition of bundled maps (of whatever kind, e.g., continuous maps) is definitionally associative, but not definitionally unital

[Reid Barton]

But I think when you go to write down the lax limit of categories you'll end up needing to turn these equalities of functors/objects into isomorphisms anyways

[Reid Barton]

so, it's probably easier to just work with isomorphisms (that is, a pseudofunctor) from the start

[Adam Topaz]

Yeah I agree.

[Adam Topaz]

I was just playing with what's currently in mathlib.

[Adam Topaz]

Which doesn't have pseudofunctors, right?

[Adam Topaz]

Or 2 categories.

[Reid Barton]

I don't think so.

[Reid Barton]

I wonder whether it would be possible to have a version of tidy that could be trusted to produce sufficiently trivial data

[Reid Barton]

I wouldn't bother with 2-categories for this purpose--Cat is the only one that matters

[Reid Barton]

In fact, I think we already basically prove a bunch of things are pseudofunctors but we lack the language to say that that's what we're doing

[Reid Barton]

I guess it's possible we could need pseudofunctors valued in some flavor of monoidal categories

[Reid Barton]

Also, bicategories wouldn't be that hard--I think it basically amounts to taking the existing monoidal category code and inserting a bunch more indices everywhere.

[Adam Topaz]

I think if/when we end up having some higher category theory, it would be nice if tidy can put in simple data like \lam X, Xfor us.

[Scott Morrison]

Reid Barton said:

Of course the real point of a ring is that it's a monoid object in $(\mathrm{Ab}, \otimes)$ (or maybe in the associated multicategory) but we don't have this information in mathlib AFAIK.

Still catching up on this thread, but we do have this: https://github.com/leanprover-community/mathlib/blob/7bade58/src/category_theory/monoidal/internal/Module.lean#L136 proves that monoid objects in R-modules are the same thing as R-algebras.

[Scott Morrison]

Reid Barton said:

I guess this gets back to my original question as well then. I don't understand what there is to automate. Don't we already have sheaves of abelian groups, which we could presumably make into a monoidal category, and monoid objects in a monoidal category, and modules over them (I'm not sure if they exist yet, but they are no harder than monoid objects)?

We have the monoidal structure on presheaves in C when C is monoidal, from https://github.com/leanprover-community/mathlib/blob/7bade58/src/category_theory/monoidal/functor_category.lean#L61. There is still some work to do to get this for sheaves.

We have modules over monoid objects, as https://github.com/leanprover-community/mathlib/blob/7bade58/src/category_theory/monoidal/internal.lean#L188, although almost nothing is proved about them (besides the comap construction).

[Scott Morrison]

Reid Barton said:

I wonder whether it would be possible to have a version of tidy that could be trusted to produce sufficiently trivial data

Somewhere there is a follow_your_nose tactic on a branch, which is essentially a cut-down version of tidy, further empowered to insert identity morphisms and a few other things. It's been a long time, but I'll try to find it.

[Fabian Glöckle]

Johan Commelin said:

Fabian Glöckle is your code available somewhere?

(Back from holidays, sorry for moving back in the discussion.)
I shared the code some while ago in this thread https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Generate.20homomorphism.20types.20for.20algebraic.20structures/
It generates homomorphism types for structures defined in regular lean code, no extra "structure description format" is required.
See it as a proof of concept that such things work in lean metaprogramming - the code itself might not be the cleanest.

[Johan Commelin]

Thanks... I had lost track of the other thread already...

[Johan Commelin]

@Adam Topaz :up:

[Jacques Carette]

Sorry to have 'disappeared' from this thread. I was expecting to get some kind of notification that it was active, but nope. Only when I tried to catch up on "everything" did I noticed it had been resurrected.

@Reid Barton thanks a lot for that list. Luckily, it overlaps a lot with our list, as most of these constructions are indeed polymorphic over (a presentation of) an algebraic theory. So indeed at least that much automation should be in scope.

When moving away from single-sorted theories, things do get tricky quite quickly. I'd eventually like to get to 'essentially algebraic theories', but that's a steep hill to climb.

[Eric Wieser]

Vaguelly related to this thread: Is it true that function.injective (free_algebra.ι R : X → free_algebra R X)?

[Eric Wieser]

I can't get beyond

lemma ι_inj : function.injective (ι R : X → free_algebra R X) := begin
  intros a b h,
  unfold ι at h,
  unfold_coes at h,
  apply @pre.of.inj R infer_instance X _,
  -- h: quot.mk (rel R X) (pre.of a) = quot.mk (rel R X) (pre.of b)
  -- ⊢ pre.of a = pre.of b
  sorry

[Johan Commelin]

I guess you need nontrivial R, right?

[Eric Wieser]

I think that's implied by the fact I have a submodule R X instance, but I may be mistaken

[Anne Baanen]

Isn't the zero ring a (semi)module of itself in Lean?

[Eric Wieser]

And my issue right now is more with finding a suitable induction principle.

[Eric Wieser]

Inducting on quot.eq.mp h loses the information that I started with pre.of

  replace h := quot.eq.mp h,
  induction h,

[Eric Wieser]

And using set to try and keep that information gives an app_builder error:

lemma ι_inj : function.injective (ι R : X → free_algebra R X) := begin
  intros a b h,
  unfold ι at h,
  unfold_coes at h,
  apply @pre.of.inj R infer_instance X _,
  replace h := quot.eq.mp h,
  set pa : pre R X := pre.of a,
  set pb: pre R X := pre.of b,
  induction h,
  {
    intro,
    -- [app_builder] failed to infer universe level for type
    -- (let pa : pre R X := pre.of a, pb : pre R X := pre.of b in
    -- λ (h : eqv_gen (rel R X) pa pb), pre.of a = pre.of b) h_x h_y (eqv_gen.rel h_x h_y h_a)
  },
end

[Eric Wieser]

Moved discussion to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60sorry.60.20tactic.20fails/near/212418947 - even sorryis failing, so this looks like a deeper problem

[Reid Barton]

It's not clear to me how you would continue anyways. Did you have a math proof of this in mind?

[Reid Barton]

As I recall, free_algebra R M is basically constructed so that by definition it has the universal property for $R$-algebras with an $R$-module map from $M$.

[Adam Topaz]

This function is injective assuming R is nontrivial. If you can construct some ring $A$ with a map $X \to A$ which is injective, then it has to factor through free_algebra R X via \iota by the universal property, so the map will be injective for free.

[Adam Topaz]

You can probably just map into the mv_polynomialring.

[Reid Barton]

If you only care about this injective statement then you could get away with much less. Namely, any $R$-module $M$ defines a square-zero extension $R \oplus M$ by defining the product of two elements of $M$ to be zero.

[Adam Topaz]

That's a ring into which M maps injectively :)

[Adam Topaz]

I was suggesting to use some explicit ring. The square-zero extension is a good choice.

[Adam Topaz]

The mv_polynomialring is another one.

[Adam Topaz]

Note that the free algebra is no longer the tensor algebra (this was refactored by Scott)

[Reid Barton]

If you want to understand what free_algebra R M looks like as an $R$-module then often a good way is to give a second construction (as $\bigoplus_{n \ge 0} M^{\otimes n}$ in this case) and check it also satisfies the universal property.

[Reid Barton]

Sorry, my internet cut out in the middle of writing this.

[Eric Wieser]

Perhaps I should un- #xy this - I'm trying to prove that algebra.adjoin R (set.range (ι R : X → free_algebra R X)) = ⊤

[Adam Topaz]

Oh this should be easier.

[Reid Barton]

This sounds a lot easier, and also pretty much unrelated to injectivity...?

[Adam Topaz]

Yeah, this amounts to proving that every element of the free algebra is some sum/product of elements in the image of \iota.

[Adam Topaz]

And this comes essentially from the inductive definition of free_algebra.pre

[Eric Wieser]

Injectivity came up because it looked like it was sufficient for the proof, and also seemed obviously true

[Adam Topaz]

And you give me some code with imports?

[Eric Wieser]

I think I can prove the adjoin statement above using #4335, but my goal was to replace #4335 with a proof via adjoin instead

[Adam Topaz]

I'll try to put something together.

[Eric Wieser]

import algebra.free_algebra
import ring_theory.adjoin

variables (R : Type*) [comm_semiring R]
variables (X : Type*)

open free_algebra

lemma ι_generator : algebra.adjoin R (set.range (ι R : X → free_algebra R X)) = ⊤ := sorry

[Adam Topaz]

This should get you started:

import algebra.free_algebra
import ring_theory.adjoin

variables (R : Type*) [comm_semiring R]
variables (X : Type*)

open free_algebra

local attribute [reducible] free_algebra

lemma ι_generator : algebra.adjoin R (set.range (ι R : X → free_algebra R X)) = ⊤ :=
begin
  ext,
  refine ⟨by simp,_⟩,
  intro hx,
  induction x,
  induction x,
  { sorry },
  { sorry },
  { sorry },
  { sorry },
  { sorry },
end

[Adam Topaz]

Of course, I'm cheating because I know the construction of free_algebra which I'm not supposed to use.

[Adam Topaz]

Hence the local attribute [reducible] free_algebra.

[Eric Wieser]

Yeah, I was hoping to either avoid cheating or make some extra statement about the universal property before we sealed the construction

[Eric Wieser]

Is the stronger statement (lift R f).range = algebra.adjoin R (set.range f) also true? (generalizing ι R to f)

[Adam Topaz]

Yeah that's also true.

[Reid Barton]

The induction principle in #4335 seems like a sensible thing to have (though we generally wouldn't bundle the conditions into a structure). I don't understand the proof in #4335, but it can just be proved directly.

[Adam Topaz]

Yeah if we don't want to temporarily make things reducible (which we probably don't), then it looks like we're missing some induction principles.

[Eric Wieser]

I don't understand the proof in #4335

What proof?

[Reid Barton]

everything after line 303

[Reid Barton]

The proof should just be: since free_algebra is a quotient it suffices to check C holds on things of the form quot.mk of something. Now define C' x to be C (quot.mk _ x) (or whatever the syntax is). Then the conditions on C turn into the conditions on C' needed to apply induction on pre.

[Eric Wieser]

Ah, the point was to generate the inductive principle from the universal property alone

[Reid Barton]

I see. That's also possible but it seems unnecessary.

[Eric Wieser]

I've realized that most of that proof is actually just a crutch for has_coe_to_sort (subalgebra R A) not existing

[Eric Wieser]

Or rather, something wacky going on with typeclass resolution

[Eric Wieser]

#4335 updated, the proof is now much shorter

[Eric Wieser]

I found myself needing a lemma something like this:

variables {R : Type*} [comm_semiring R]
variables {X : Type*}
variables {A : Type*} [semiring A] [algebra R A]
variables (f : X → A)  (g : A →ₐ[R] free_algebra R X)

-- better as  `ι R = (g.comp (lift R f)) ∘ ι R ↔ alg_hom.id R _ = g.comp (lift R f)`?
lemma forall_ι_iff_forall:
  (∀ x, ι R x = g (lift R f (ι R x))) ↔ ∀ z, z = g (lift R f z) :=
begin
  split,
  { intros h z,
    rw ←alg_hom.comp_apply,
    conv_lhs {rw ←@alg_hom.id_apply R _ _ _ _ z},
    revert z,
    rw ←alg_hom.ext_iff,
    refine free_algebra.hom_ext (funext $ λ x, _),  -- ext, but written to make clear what lemma I use
    simp only [alg_hom.id_apply, alg_hom.comp_apply, function.comp_app],
    exact h x, },
  { intros h x,
    exact h (ι R x), }
end

This feels really quite clumsy - can anyone think of a tidier proof or theorem statement? Are we missing some obvious lemmas about lift and ι that would make this easier?

[Reid Barton]

Two algebra maps out of the free algebra are equal (right hand side of iff) if and only if they agree on the generators X (left hand side of iff).

[Eric Wieser]

I think the non-trivial direction of that statement is exactly the statement of docs#free_algebra.hom_ext which my proof already uses

[Eric Wieser]

Although what you have there sounds like a nice docstring for hom_ext

[Reid Barton]

Well that's the general statement here. I don't see why we would have a lemma which is specialized to the case where one algebra map is the identity and the other one is lift f composed with some arbitrary other map. That's what passing arguments to lemmas is for.

[Reid Barton]

It might be more convenient to have a version of hom_ext that yields an iff, and takes the algebra maps as explicit arguments, and maybe uses elementwise equality rather than equality of functions/algebra morphisms.

[Eric Wieser]

That's what passing arguments to lemmas is for.

Agreed, that's why I felt uneasy with this proof. I'll have a go at your suggestion and see if it shortens my proof.

[Reid Barton]

I don't really understand what is happening in this proof without running it, but I think it would be more straightforward to use have or something with a statement that involves things like alg_hom.id and g.comp (lift R f), rather than trying to backwardsly massage the statement into making those expressions appear

[Reid Barton]

The key """insight""" in this proof from Lean's perspective is that z is really the value of the identity algebra map applied to z, and so on. If you can get that information in as early as possible it should make the rest of the proof trivial.

[Reid Barton]

The reason you have to do any work at all is that Lean doesn't know how to solve problems like "what's an algebra map F such that for every z, F z = z?"

[Eric Wieser]

Should that be an ext lemma for alg_hom?

[Eric Wieser]

(∀ z, ⇑F x = x) → F = alg_hom.id

[Eric Wieser]

I think you've nailed where the awkwardness is though - alg_hom is full of lemmas to simp to function applications, but I need to do the reverse and coalesce things into a single alg_hom.

[Reid Barton]

I mean this already exists as a specialization of ext

[Reid Barton]

But this is also the wrong direction, it says that the map has to be alg_hom, but what you need is something that makes you think to try alg_hom in the first place

[Eric Wieser]

Right, hence your suggestion to use have

[Reid Barton]

Right, or I suppose you could pass the alg_homs using @ notation but there would probably be a lot of _s involved

[Reid Barton]

Actually there is a mechanism to do this already--unification hints

[Reid Barton]

but I don't know if they would work here anyways

[Eric Wieser]

Anywhere I can read about those?

[Reid Barton]

Well they have about a 0% chance of getting used in mathlib anyways... not sure whether they are written up anywhere

[Reid Barton]

In brief, you can register "hints" that tell Lean that if it is trying to solve for a metavariable ?m_1 by unification and there's not enough information, but there is a constraint like ?m_1.foo = bar, then it should try to refine ?m_1 in some particular way. Johan and I experimented a bit with them and we have some notes at https://github.com/rwbarton/lean-omin/blob/master/old/unification_hints.lean

[Reid Barton]

I don't know if they would work with higher-order constraints--probably not because they're basically unsupported

[Eric Wieser]

Oh, that looks interesting

[Eric Wieser]

I wonder if that can be used to fix the problem I had in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Type.20inference.20on.20.60.E2.86.92.60.20vs.20.60.E2.89.83.60

[Eric Wieser]

Thanks for the advice anyway, I ended up with a much tidier proof in the PR

[Kevin Buzzard]

Note that they're being removed in lean 4 as far as I understand it

[Eric Wieser]

Related to free stuff, but only tangentially to the conversation above - I found that we'd missed some quite useful bundling that makes it a little easier to work with lift - namely framing it as an equivalence, where lift.symm F is F.comp ι (#4908) - that way all of the other equiv lemmas can be used too, after converting things back to the lift.symm form

[Eric Wieser]

Eric Wieser said:

Vaguelly related to this thread: Is it true that function.injective (free_algebra.ι R : X → free_algebra R X)?

I've circled back to wanting to prove this - it seems I need it to prove nontrivial R → nontrivial X → nontrivial (free_algebra R X)

[Eric Wieser]

False alarm, I can prove that without it too, #5033