# Zulip Chat Archive

## Stream: maths

### Topic: Free stuff

#### Adam Topaz (Sep 09 2020 at 12:15):

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 (Sep 09 2020 at 12:23):

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 (Sep 09 2020 at 12:29):

@Kenny Lau @Chris Hughes what do you think?

#### Adam Topaz (Sep 09 2020 at 12:51):

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 (Sep 09 2020 at 13:38):

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 (Sep 09 2020 at 13:46):

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 (Sep 09 2020 at 13:48):

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 (Sep 09 2020 at 13:48):

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

#### Adam Topaz (Sep 09 2020 at 13:51):

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 (Sep 09 2020 at 14:01):

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 (Sep 09 2020 at 14:05):

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 (Sep 09 2020 at 14:07):

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

#### Reid Barton (Sep 09 2020 at 14:08):

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

#### Chris Hughes (Sep 09 2020 at 14:10):

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

#### Adam Topaz (Sep 09 2020 at 14:11):

@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 (Sep 09 2020 at 14:12):

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 (Sep 09 2020 at 14:13):

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

#### Johan Commelin (Sep 09 2020 at 14:14):

It could generate `ring_hom`

and the category `Ring`

from the lean code of `ring`

#### Johan Commelin (Sep 09 2020 at 14:14):

And similarly for the rest of the algebraic hierarchy.

#### Adam Topaz (Sep 09 2020 at 14:14):

Oh cool! Is there a repo somewhere?

#### Chris Hughes (Sep 09 2020 at 14:14):

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 (Sep 09 2020 at 14:14):

@Fabian Glöckle is your code available somewhere?

#### Patrick Massot (Sep 09 2020 at 14:15):

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 (Sep 09 2020 at 14:16):

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 (Sep 09 2020 at 14:26):

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 (Sep 09 2020 at 14:28):

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 (Sep 09 2020 at 14:29):

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 (Sep 09 2020 at 14:33):

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

#### Jacques Carette (Sep 09 2020 at 14:35):

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 (Sep 09 2020 at 14:36):

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

Signature, Product Algebra, Basic Term Language, Homomorphism, Closed Term

Language, Open Term Language, Evaluator, Simplication 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 (Sep 09 2020 at 14:37):

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

#### Johan Commelin (Sep 09 2020 at 14:37):

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

#### Jacques Carette (Sep 09 2020 at 14:37):

#### Jacques Carette (Sep 09 2020 at 14:38):

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

#### Jacques Carette (Sep 09 2020 at 14:39):

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 (Sep 09 2020 at 14:45):

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 (Sep 09 2020 at 14:46):

We are actively targeting Agda.

#### Jacques Carette (Sep 09 2020 at 14:47):

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

#### Scott Morrison (Sep 09 2020 at 22:54):

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 (Sep 09 2020 at 22:54):

Sorry, the discussion wandered a little bit :)

#### Scott Morrison (Sep 09 2020 at 22:57):

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

#### Scott Morrison (Sep 10 2020 at 02:44):

I've added `free_algebra R X ≃ₐ[R] monoid_algebra R (free_monoid X)`

to #4077.

#### Chris Hughes (Sep 10 2020 at 02:59):

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

#### Scott Morrison (Sep 10 2020 at 03:04):

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

#### Scott Morrison (Sep 10 2020 at 03:05):

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

#### Scott Morrison (Sep 10 2020 at 03:10):

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:

- 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 - 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 (Sep 10 2020 at 03:24):

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 (Sep 10 2020 at 13:53):

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 (Sep 10 2020 at 13:59):

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 (Sep 10 2020 at 14:01):

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

and `subgroup`

?

#### Reid Barton (Sep 10 2020 at 14:06):

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 (Sep 10 2020 at 14:07):

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 (Sep 10 2020 at 14:08):

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 (Sep 10 2020 at 14:19):

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

#### Chris Hughes (Sep 10 2020 at 14:33):

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 (Sep 10 2020 at 14:33):

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

#### Adam Topaz (Sep 10 2020 at 14:34):

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

#### Adam Topaz (Sep 10 2020 at 14:34):

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

#### Reid Barton (Sep 10 2020 at 14:35):

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

#### Chris Hughes (Sep 10 2020 at 14:35):

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 (Sep 10 2020 at 14:36):

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

#### Adam Topaz (Sep 10 2020 at 14:37):

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 (Sep 10 2020 at 14:39):

Use type class inference? Inspect `group.to_monoid`

.

#### Adam Topaz (Sep 10 2020 at 14:40):

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 (Sep 10 2020 at 15:04):

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 (Sep 10 2020 at 15:41):

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 (Sep 10 2020 at 16:00):

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

#### Adam Topaz (Sep 10 2020 at 16:01):

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

#### Adam Topaz (Sep 10 2020 at 16:03):

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 (Sep 10 2020 at 16:03):

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 (Sep 11 2020 at 12:53):

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 (Sep 11 2020 at 12:54):

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

#### Reid Barton (Sep 11 2020 at 12:55):

What API though?

#### Kevin Buzzard (Sep 11 2020 at 12:57):

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 (Sep 11 2020 at 12:58):

- 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 (Sep 11 2020 at 12:58):

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 (Sep 11 2020 at 12:59):

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

#### Kevin Buzzard (Sep 11 2020 at 13:00):

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

#### Johan Commelin (Sep 11 2020 at 13:01):

That's exactly Reid's point.

#### Kevin Buzzard (Sep 11 2020 at 13:02):

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

#### Reid Barton (Sep 11 2020 at 13:02):

Johan Commelin said:

- Definition of a sheaf of modules.

Already there are many possibilities for this definition

#### Kevin Buzzard (Sep 11 2020 at 13:03):

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 (Sep 11 2020 at 13:12):

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 (Sep 11 2020 at 13:13):

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

#### Johan Commelin (Sep 11 2020 at 13:13):

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

#### Reid Barton (Sep 11 2020 at 13:15):

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 (Sep 11 2020 at 13:16):

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 (Sep 11 2020 at 14:01):

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 (Sep 11 2020 at 14:02):

Assuming the metacode produces `is_subfoo`

classes...

#### Adam Topaz (Sep 11 2020 at 14:19):

`local_ring_predicate`

should be read `local_(ring_predicate)`

and not `(local_ring)_predicate`

#### Reid Barton (Sep 11 2020 at 14:25):

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 (Sep 11 2020 at 14:27):

A sheaf of modules is a `local_module_predicate`

satsifying some gluing axioms.

#### Reid Barton (Sep 11 2020 at 14:28):

Hang on, I don't know what a `local_predicate`

is.

#### Reid Barton (Sep 11 2020 at 14:30):

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 (Sep 11 2020 at 14:31):

maybe together with some more stuff

#### Reid Barton (Sep 11 2020 at 14:31):

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

#### Adam Topaz (Sep 11 2020 at 14:32):

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

#### Adam Topaz (Sep 11 2020 at 14:33):

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

#### Adam Topaz (Sep 11 2020 at 14:33):

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 (Sep 11 2020 at 14:35):

Errr sorry, in mathlib `local_predicate`

is satisfies the sheaf axiom, but there is also a `prelocal_predicate`

which gives you presheaves.

#### Reid Barton (Sep 11 2020 at 14:35):

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

#### Adam Topaz (Sep 11 2020 at 14:35):

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

#### Adam Topaz (Sep 11 2020 at 14:36):

Hence the `is_submodule`

#### Adam Topaz (Sep 11 2020 at 14:37):

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 (Sep 11 2020 at 14:37):

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

#### Adam Topaz (Sep 11 2020 at 14:39):

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 (Sep 11 2020 at 14:41):

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 (Sep 11 2020 at 14:42):

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

#### Adam Topaz (Sep 11 2020 at 14:42):

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

#### Kevin Buzzard (Sep 11 2020 at 14:46):

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 (Sep 11 2020 at 14:56):

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 (Sep 11 2020 at 14:58):

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 (Sep 11 2020 at 14:59):

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 (Sep 11 2020 at 15:00):

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

#### Adam Topaz (Sep 11 2020 at 15:09):

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 (Sep 11 2020 at 15:09):

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

#### Adam Topaz (Sep 11 2020 at 15:12):

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

#### Adam Topaz (Sep 11 2020 at 15:41):

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 (Sep 11 2020 at 16:35):

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 (Sep 11 2020 at 16:38):

I was envisioning automating the creation of sheaves of `foo`

where `foo`

is any (possibly multi-sorted) Lawvere theory (or variety in the sense of universal algebra, or ...).

#### Adam Topaz (Sep 11 2020 at 16:40):

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 (Sep 11 2020 at 16:41):

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 (Sep 11 2020 at 16:41):

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 (Sep 11 2020 at 16:42):

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

#### Kevin Buzzard (Sep 11 2020 at 16:43):

That's an interesting approach!

#### Kevin Buzzard (Sep 11 2020 at 16:43):

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

#### Reid Barton (Sep 11 2020 at 16:43):

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

#### Reid Barton (Sep 11 2020 at 16:44):

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 (Sep 11 2020 at 16:44):

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

#### Reid Barton (Sep 11 2020 at 16:45):

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 (Sep 11 2020 at 16:48):

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

#### Kenny Lau (Sep 11 2020 at 16:49):

then you start getting equality of types

#### Reid Barton (Sep 11 2020 at 16:50):

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

#### Adam Topaz (Sep 11 2020 at 21:07):

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 (Sep 11 2020 at 21:08):

I think you'd want to use pseudofunctors anyways

#### Adam Topaz (Sep 11 2020 at 21:09):

Yeah for sure.

#### Reid Barton (Sep 11 2020 at 21:10):

although this is probably not that bad to prove

#### Adam Topaz (Sep 11 2020 at 21:10):

Yeah, but the fact that `tidy`

didn't even get the `map_id`

field was a bad sign.

#### Adam Topaz (Sep 11 2020 at 21:10):

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

#### Adam Topaz (Sep 11 2020 at 21:10):

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

#### Adam Topaz (Sep 11 2020 at 21:17):

Ha. `tidy`

is happy with the second sorry.

#### Reid Barton (Sep 11 2020 at 21:18):

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

#### Reid Barton (Sep 11 2020 at 21:20):

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

#### Reid Barton (Sep 11 2020 at 21:20):

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

#### Reid Barton (Sep 11 2020 at 21:24):

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 (Sep 11 2020 at 21:25):

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

#### Adam Topaz (Sep 11 2020 at 21:25):

Yeah I agree.

#### Adam Topaz (Sep 11 2020 at 21:25):

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

#### Adam Topaz (Sep 11 2020 at 21:25):

Which doesn't have pseudofunctors, right?

#### Adam Topaz (Sep 11 2020 at 21:25):

Or 2 categories.

#### Reid Barton (Sep 11 2020 at 21:26):

I don't think so.

#### Reid Barton (Sep 11 2020 at 21:27):

I wonder whether it would be possible to have a version of `tidy`

that could be trusted to produce sufficiently trivial data

#### Reid Barton (Sep 11 2020 at 21:29):

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

#### Reid Barton (Sep 11 2020 at 21:29):

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 (Sep 11 2020 at 21:34):

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

#### Reid Barton (Sep 11 2020 at 21:34):

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 (Sep 11 2020 at 21:45):

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, X`

for us.

#### Scott Morrison (Sep 11 2020 at 23:32):

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 (Sep 11 2020 at 23:38):

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 (Sep 11 2020 at 23:41):

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 (Sep 12 2020 at 09:36):

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 (Sep 12 2020 at 09:39):

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

#### Johan Commelin (Sep 12 2020 at 09:39):

@Adam Topaz :up:

#### Jacques Carette (Sep 17 2020 at 22:57):

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 (Oct 06 2020 at 11:29):

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

?

#### Eric Wieser (Oct 06 2020 at 11:42):

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 (Oct 06 2020 at 11:47):

I guess you need `nontrivial R`

, right?

#### Eric Wieser (Oct 06 2020 at 11:54):

I think that's implied by the fact I have a `submodule R X`

instance, but I may be mistaken

#### Anne Baanen (Oct 06 2020 at 11:55):

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

#### Eric Wieser (Oct 06 2020 at 11:56):

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

#### Eric Wieser (Oct 06 2020 at 11:57):

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 (Oct 06 2020 at 12:12):

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 (Oct 06 2020 at 12:23):

Moved discussion to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60sorry.60.20tactic.20fails/near/212418947 - even `sorry`

is failing, so this looks like a deeper problem

#### Reid Barton (Oct 06 2020 at 12:56):

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

#### Reid Barton (Oct 06 2020 at 12:58):

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 (Oct 06 2020 at 13:00):

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 (Oct 06 2020 at 13:03):

You can probably just map into the `mv_polynomial`

ring.

#### Reid Barton (Oct 06 2020 at 13:03):

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 (Oct 06 2020 at 13:03):

That's a ring into which `M`

maps injectively :)

#### Adam Topaz (Oct 06 2020 at 13:04):

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

#### Adam Topaz (Oct 06 2020 at 13:04):

The `mv_polynomial`

ring is another one.

#### Adam Topaz (Oct 06 2020 at 13:04):

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

#### Reid Barton (Oct 06 2020 at 13:04):

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 (Oct 06 2020 at 13:04):

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

#### Eric Wieser (Oct 06 2020 at 13:12):

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 (Oct 06 2020 at 13:14):

Oh this should be easier.

#### Reid Barton (Oct 06 2020 at 13:14):

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

#### Adam Topaz (Oct 06 2020 at 13:14):

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 (Oct 06 2020 at 13:15):

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

#### Eric Wieser (Oct 06 2020 at 13:16):

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

#### Adam Topaz (Oct 06 2020 at 13:17):

And you give me some code with imports?

#### Eric Wieser (Oct 06 2020 at 13:17):

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 (Oct 06 2020 at 13:17):

I'll try to put something together.

#### Eric Wieser (Oct 06 2020 at 13:21):

```
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 (Oct 06 2020 at 13:24):

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 (Oct 06 2020 at 13:25):

Of course, I'm cheating because I know the construction of `free_algebra`

which I'm not supposed to use.

#### Adam Topaz (Oct 06 2020 at 13:25):

Hence the `local attribute [reducible] free_algebra`

.

#### Eric Wieser (Oct 06 2020 at 13:26):

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

#### Eric Wieser (Oct 06 2020 at 13:26):

Is the stronger statement `(lift R f).range = algebra.adjoin R (set.range f)`

also true? (generalizing `ι R`

to `f`

)

#### Adam Topaz (Oct 06 2020 at 13:27):

Yeah that's also true.

#### Reid Barton (Oct 06 2020 at 13:28):

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 (Oct 06 2020 at 13:30):

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 (Oct 06 2020 at 13:30):

I don't understand the proof in #4335

What proof?

#### Reid Barton (Oct 06 2020 at 13:31):

everything after line 303

#### Reid Barton (Oct 06 2020 at 13:33):

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 (Oct 06 2020 at 13:33):

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

#### Reid Barton (Oct 06 2020 at 13:40):

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

#### Eric Wieser (Oct 06 2020 at 14:22):

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 (Oct 06 2020 at 15:18):

Or rather, something wacky going on with typeclass resolution

#### Eric Wieser (Oct 06 2020 at 15:19):

#4335 updated, the proof is now much shorter

#### Eric Wieser (Oct 07 2020 at 10:46):

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 (Oct 07 2020 at 11:47):

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 (Oct 07 2020 at 11:54):

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 (Oct 07 2020 at 11:56):

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

#### Reid Barton (Oct 07 2020 at 12:28):

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 (Oct 07 2020 at 12:31):

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 (Oct 07 2020 at 12:35):

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 (Oct 07 2020 at 12:37):

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 (Oct 07 2020 at 12:39):

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 (Oct 07 2020 at 12:40):

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 (Oct 07 2020 at 12:42):

Should that be an `ext`

lemma for `alg_hom`

?

#### Eric Wieser (Oct 07 2020 at 12:43):

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

#### Eric Wieser (Oct 07 2020 at 12:44):

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 (Oct 07 2020 at 12:44):

I mean this already exists as a specialization of `ext`

#### Reid Barton (Oct 07 2020 at 12:46):

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 (Oct 07 2020 at 12:47):

Right, hence your suggestion to use `have`

#### Reid Barton (Oct 07 2020 at 12:48):

Right, or I suppose you could pass the `alg_hom`

s using `@`

notation but there would probably be a lot of `_`

s involved

#### Reid Barton (Oct 07 2020 at 12:49):

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

#### Reid Barton (Oct 07 2020 at 12:49):

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

#### Eric Wieser (Oct 07 2020 at 12:50):

Anywhere I can read about those?

#### Reid Barton (Oct 07 2020 at 12:50):

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

#### Reid Barton (Oct 07 2020 at 12:56):

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 (Oct 07 2020 at 12:57):

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

#### Eric Wieser (Oct 07 2020 at 13:01):

Oh, that looks interesting

#### Eric Wieser (Oct 07 2020 at 13:02):

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 (Oct 07 2020 at 13:08):

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

#### Kevin Buzzard (Oct 07 2020 at 13:53):

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

#### Eric Wieser (Nov 06 2020 at 11:49):

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 (Nov 18 2020 at 09:10):

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 (Nov 18 2020 at 09:24):

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

Last updated: May 11 2021 at 16:22 UTC