Zulip Chat Archive

Stream: maths

Topic: Free stuff


view this post on Zulip 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 RR-algebra on a type SS is the RR-tensor-algebra on the free module generated by SS, 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 RR-algebra on a type SS as a quotient of the free (semi)ring on generated by the disjoint union of RR and SS. 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 09 2020 at 12:29):

@Kenny Lau @Chris Hughes what do you think?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 09 2020 at 13:48):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 09 2020 at 14:07):

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

view this post on Zulip Reid Barton (Sep 09 2020 at 14:08):

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

view this post on Zulip Chris Hughes (Sep 09 2020 at 14:10):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 09 2020 at 14:13):

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

view this post on Zulip Johan Commelin (Sep 09 2020 at 14:14):

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

view this post on Zulip Johan Commelin (Sep 09 2020 at 14:14):

And similarly for the rest of the algebraic hierarchy.

view this post on Zulip Adam Topaz (Sep 09 2020 at 14:14):

Oh cool! Is there a repo somewhere?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 09 2020 at 14:14):

@Fabian Glöckle is your code available somewhere?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.]

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 09 2020 at 14:33):

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

view this post on Zulip 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.

view this post on Zulip 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, 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.

view this post on Zulip Johan Commelin (Sep 09 2020 at 14:37):

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

view this post on Zulip Johan Commelin (Sep 09 2020 at 14:37):

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

view this post on Zulip Jacques Carette (Sep 09 2020 at 14:37):

slides-1.pdf

view this post on Zulip Jacques Carette (Sep 09 2020 at 14:38):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jacques Carette (Sep 09 2020 at 14:46):

We are actively targeting Agda.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Adam Topaz (Sep 09 2020 at 22:54):

Sorry, the discussion wandered a little bit :)

view this post on Zulip Scott Morrison (Sep 09 2020 at 22:57):

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

view this post on Zulip Scott Morrison (Sep 10 2020 at 02:44):

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

view this post on Zulip Chris Hughes (Sep 10 2020 at 02:59):

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

view this post on Zulip Scott Morrison (Sep 10 2020 at 03:04):

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

view this post on Zulip Scott Morrison (Sep 10 2020 at 03:05):

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

view this post on Zulip 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:

  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.

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 10 2020 at 14:33):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 10 2020 at 14:34):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 10 2020 at 14:36):

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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Sep 10 2020 at 14:39):

Use type class inference? Inspect group.to_monoid.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 16:00):

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

view this post on Zulip Adam Topaz (Sep 10 2020 at 16:01):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 16:03):

Adam Topaz said:

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

I might get a bit confused about parameters vs extension

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 11 2020 at 12:54):

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

view this post on Zulip Reid Barton (Sep 11 2020 at 12:55):

What API though?

view this post on Zulip 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".

view this post on Zulip 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>

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 11 2020 at 12:59):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 11 2020 at 13:01):

That's exactly Reid's point.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 11 2020 at 13:13):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Sep 11 2020 at 13:16):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 11 2020 at 14:02):

Assuming the metacode produces is_subfoo classes...

view this post on Zulip Adam Topaz (Sep 11 2020 at 14:19):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Sep 11 2020 at 14:27):

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

view this post on Zulip Reid Barton (Sep 11 2020 at 14:28):

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

view this post on Zulip 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)]

view this post on Zulip Reid Barton (Sep 11 2020 at 14:31):

maybe together with some more stuff

view this post on Zulip Reid Barton (Sep 11 2020 at 14:31):

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

view this post on Zulip Adam Topaz (Sep 11 2020 at 14:32):

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

view this post on Zulip Adam Topaz (Sep 11 2020 at 14:33):

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

view this post on Zulip 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.

view this post on Zulip 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.

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

view this post on Zulip Reid Barton (Sep 11 2020 at 14:35):

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

view this post on Zulip Adam Topaz (Sep 11 2020 at 14:35):

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

view this post on Zulip Adam Topaz (Sep 11 2020 at 14:36):

Hence the is_submodule

view this post on Zulip Adam Topaz (Sep 11 2020 at 14:37):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 11 2020 at 14:42):

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

view this post on Zulip Adam Topaz (Sep 11 2020 at 14:42):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 11 2020 at 15:09):

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

view this post on Zulip 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.

view this post on Zulip 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 A\mathcal{A} such that for every open UU, A(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".

view this post on Zulip 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)?

view this post on Zulip Adam Topaz (Sep 11 2020 at 16:38):

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 ...).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 11 2020 at 16:41):

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

view this post on Zulip Adam Topaz (Sep 11 2020 at 16:42):

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

view this post on Zulip Kevin Buzzard (Sep 11 2020 at 16:43):

That's an interesting approach!

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 11 2020 at 16:44):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 11 2020 at 16:48):

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

view this post on Zulip Kenny Lau (Sep 11 2020 at 16:49):

then you start getting equality of types

view this post on Zulip Reid Barton (Sep 11 2020 at 16:50):

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

view this post on Zulip 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 }

view this post on Zulip Reid Barton (Sep 11 2020 at 21:08):

I think you'd want to use pseudofunctors anyways

view this post on Zulip Adam Topaz (Sep 11 2020 at 21:09):

Yeah for sure.

view this post on Zulip Reid Barton (Sep 11 2020 at 21:10):

although this is probably not that bad to prove

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 11 2020 at 21:10):

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

view this post on Zulip Adam Topaz (Sep 11 2020 at 21:10):

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

view this post on Zulip Adam Topaz (Sep 11 2020 at 21:17):

Ha. tidy is happy with the second sorry.

view this post on Zulip Reid Barton (Sep 11 2020 at 21:18):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Sep 11 2020 at 21:25):

Yeah I agree.

view this post on Zulip Adam Topaz (Sep 11 2020 at 21:25):

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

view this post on Zulip Adam Topaz (Sep 11 2020 at 21:25):

Which doesn't have pseudofunctors, right?

view this post on Zulip Adam Topaz (Sep 11 2020 at 21:25):

Or 2 categories.

view this post on Zulip Reid Barton (Sep 11 2020 at 21:26):

I don't think so.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 11 2020 at 21:34):

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

view this post on Zulip 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.

view this post on Zulip 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, Xfor us.

view this post on Zulip 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 (Ab,)(\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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 12 2020 at 09:39):

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

view this post on Zulip Johan Commelin (Sep 12 2020 at 09:39):

@Adam Topaz :up:

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 06 2020 at 11:47):

I guess you need nontrivial R, right?

view this post on Zulip 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

view this post on Zulip Anne Baanen (Oct 06 2020 at 11:55):

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

view this post on Zulip Eric Wieser (Oct 06 2020 at 11:56):

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

view this post on Zulip 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,

view this post on Zulip 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

view this post on Zulip 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 sorryis failing, so this looks like a deeper problem

view this post on Zulip 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?

view this post on Zulip 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 RR-algebras with an RR-module map from MM.

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:00):

This function is injective assuming R is nontrivial. If you can construct some ring AA with a map XAX \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.

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:03):

You can probably just map into the mv_polynomialring.

view this post on Zulip 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 RR-module MM defines a square-zero extension RMR \oplus M by defining the product of two elements of MM to be zero.

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:03):

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

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:04):

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

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:04):

The mv_polynomialring is another one.

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:04):

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

view this post on Zulip Reid Barton (Oct 06 2020 at 13:04):

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

view this post on Zulip Reid Barton (Oct 06 2020 at 13:04):

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

view this post on Zulip 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)) = ⊤

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:14):

Oh this should be easier.

view this post on Zulip Reid Barton (Oct 06 2020 at 13:14):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:15):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:17):

And you give me some code with imports?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:17):

I'll try to put something together.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:25):

Hence the local attribute [reducible] free_algebra.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:27):

Yeah that's also true.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Oct 06 2020 at 13:30):

I don't understand the proof in #4335

What proof?

view this post on Zulip Reid Barton (Oct 06 2020 at 13:31):

everything after line 303

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Oct 06 2020 at 13:33):

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

view this post on Zulip Reid Barton (Oct 06 2020 at 13:40):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Oct 06 2020 at 15:18):

Or rather, something wacky going on with typeclass resolution

view this post on Zulip Eric Wieser (Oct 06 2020 at 15:19):

#4335 updated, the proof is now much shorter

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Eric Wieser (Oct 07 2020 at 11:56):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?"

view this post on Zulip Eric Wieser (Oct 07 2020 at 12:42):

Should that be an ext lemma for alg_hom?

view this post on Zulip Eric Wieser (Oct 07 2020 at 12:43):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 07 2020 at 12:44):

I mean this already exists as a specialization of ext

view this post on Zulip 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

view this post on Zulip Eric Wieser (Oct 07 2020 at 12:47):

Right, hence your suggestion to use have

view this post on Zulip Reid Barton (Oct 07 2020 at 12:48):

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

view this post on Zulip Reid Barton (Oct 07 2020 at 12:49):

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

view this post on Zulip Reid Barton (Oct 07 2020 at 12:49):

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

view this post on Zulip Eric Wieser (Oct 07 2020 at 12:50):

Anywhere I can read about those?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Oct 07 2020 at 13:01):

Oh, that looks interesting

view this post on Zulip 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

view this post on Zulip Eric Wieser (Oct 07 2020 at 13:08):

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

view this post on Zulip Kevin Buzzard (Oct 07 2020 at 13:53):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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