## Stream: new members

### Topic: get the two maps from an isomorphism

#### Vasily Ilin (Apr 15 2022 at 20:45):

given an isomorphism, e.g. here: https://leanprover-community.github.io/mathlib_docs/ring_theory/tensor_product.html#algebra.tensor_product.assoc, how do I extract the forward and backward maps? I tried .hom but it does not work

#### Yaël Dillies (Apr 15 2022 at 20:47):

Simply use the isomorphism as a function to get the forward map. For the backward map, notice that it is the forward map of the reverse isomorphism (e.symm if e is the isomorphism) and do the same as before.

#### Adam Topaz (Apr 15 2022 at 20:50):

If you want to do it explicitly (e.g. if you need to pass in a linear map I to some other function) you can use docs#linear_equiv.to_linear_map (best to do this with dot notation, i.e. e.to_linear_map)

#### Adam Topaz (Apr 15 2022 at 20:51):

And similarly e.symm.to_linear_map for the inverse.

#### Adam Topaz (Apr 15 2022 at 20:52):

OTOH it looks like there is a coe from linear equivs to linear maps, so you probably can just use e with no further decorations (hopefully)

#### Vasily Ilin (Apr 15 2022 at 20:52):

I am trying to follow the first advice, and getting type mismatch:
def map2_1 : (K[X] ⊗[K] K[X] ⊗[K] K[X] →ₐ K[X] ⊗[K] (K[X] ⊗[K] K[X]) ) := (algebra.tensor_product.assoc K K[X] K[X] K[X]) gets me

type mismatch, term
algebra.tensor_product.assoc K K[X] K[X] K[X]
has type
K[X] ⊗ K[X] ⊗ K[X] ≃ₐ[K] K[X] ⊗ (K[X] ⊗ K[X])
but is expected to have type
K[X] ⊗ K[X] ⊗ K[X] →ₐ[?m_1] K[X] ⊗ (K[X] ⊗ K[X])


#### Vasily Ilin (Apr 15 2022 at 20:56):

If you want to do it explicitly (e.g. if you need to pass in a linear map I to some other function) you can use docs#linear_equiv.to_linear_map (best to do this with dot notation, i.e. e.to_linear_map)

What if I want to have an algebra map from the algebra isomorphism? I tried .to_algebra_map but got

invalid field notation, 'to_algebra_map' is not a valid "field" because environment does not contain 'alg_equiv.to_algebra_map'
algebra.tensor_product.assoc K K[X] K[X] K[X]
which has type
K[X] ⊗ K[X] ⊗ K[X] ≃ₐ[K] K[X] ⊗ (K[X] ⊗ K[X])


#### Adam Topaz (Apr 15 2022 at 20:57):

It might be called docs#algebra_equiv.to_algebra_hom ?

#### Eric Wieser (Apr 15 2022 at 20:58):

docs#alg_equiv.to_alg_hom

Aha!

#### Eric Wieser (Apr 15 2022 at 20:58):

Since the types are respectively docs#alg_equiv and docs#alg_hom

#### Eric Wieser (Apr 15 2022 at 20:59):

The naming of all these conversions should be the obvious ones given the names of the types

#### Eric Wieser (Apr 15 2022 at 20:59):

The names of the types are a bit harder to guess

#### Vasily Ilin (Apr 15 2022 at 21:02):

Hmm, that worked but now a composition of algebra homs is not an algebra hom...

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

variables (K : Type) [comm_semiring K]

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := polynomial.aeval ((polynomial.X ⊗ₜ 1) + (1 ⊗ₜ polynomial.X))

noncomputable def map2_1 : (K[X] ⊗[K] K[X] ⊗[K] K[X] →ₐ K[X] ⊗[K] (K[X] ⊗[K] K[X]) ) := (algebra.tensor_product.assoc K K[X] K[X] K[X]).to_alg_hom

noncomputable def map2_2 : (K[X] ⊗[K] K[X] →ₐ K[X] ⊗[K] K[X] ⊗[K] K[X] ) := map (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) (alg_hom.id K K[X])

noncomputable def map2_3 : K[X] →ₐ K[X] ⊗[K] K[X] := (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X])

noncomputable def map2 : (K[X] →ₐ K[X] ⊗[K] (K[X] ⊗[K] K[X]) ) := (map2_1 K) ∘ (map2_2 K) ∘ (map2_3 K)


#### Yaël Dillies (Apr 15 2022 at 21:03):

You have to use docs#alg_hom.comp, not ∘ which is docs#function.comp.

#### Adam Topaz (Apr 15 2022 at 21:04):

You can also compose algebra isoms using docs#alg_equiv.trans

#### Vasily Ilin (Apr 15 2022 at 21:07):

So many new things! Thank you so much! Is there a nicer notation for alg_hom.comp? Something like ∘\_a?

Got it, thanks!

#### Vasily Ilin (Apr 15 2022 at 21:09):

Off-topic: would it make sense to create a stream called "help" so I don't flood "new members" with specific questions like this one?

#### Jireh Loreaux (Apr 15 2022 at 21:12):

Note: even though there is no nice notation for alg_hom.comp there is dot notation. So, if f and g are alg_homs, then you can write f.comp g for alg_hom.comp f g.

#### Jireh Loreaux (Apr 15 2022 at 21:12):

As for the stream, I think the purpose of new members is mostly for helping new members.

#### Vasily Ilin (Apr 15 2022 at 21:16):

While I have your attention, could I get advice on how to make Lean faster? I have this file here, which is 30 lines long, and takes over ten seconds to compile. Each time I change anything, I have to wait for a few seconds to see if it compiles, which really adds up. Here is the file:

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

variables (K : Type) [comm_semiring K]

noncomputable def counit : K[X] →ₐ[K] K := polynomial.aeval 0

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := polynomial.aeval ((polynomial.X ⊗ₜ 1) + (1 ⊗ₜ polynomial.X))

noncomputable def map1 : K[X] →ₐ K[X] ⊗ (K[X] ⊗ K[X]) := alg_hom.comp (map (alg_hom.id K K[X]) (comul K)) (comul K)

noncomputable def map2_1 : (K[X] ⊗[K] K[X] ⊗[K] K[X] →ₐ K[X] ⊗[K] (K[X] ⊗[K] K[X]) ) := (algebra.tensor_product.assoc K K[X] K[X] K[X]).to_alg_hom

noncomputable def map2_2 : (K[X] ⊗[K] K[X] →ₐ K[X] ⊗[K] K[X] ⊗[K] K[X] ) := map (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) (alg_hom.id K K[X])

noncomputable def map2_3 : K[X] →ₐ K[X] ⊗[K] K[X] := (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X])

noncomputable def map2 : (K[X] →ₐ K[X] ⊗[K] (K[X] ⊗[K] K[X]) ) := alg_hom.comp (map2_1 K) (alg_hom.comp (map2_2 K) (map2_3 K))

lemma coassoc : map1 K = map2 K :=
begin
have P : map1 K X = map2 K X,
unfold map1,
unfold comul,

sorry,

end


#### Vasily Ilin (Apr 15 2022 at 21:16):

The reason I split map2 into three different definitions is that otherwise it times out on compilation...

#### Jireh Loreaux (Apr 15 2022 at 21:17):

That's not an #mwe, so I can't really tell what's going on.

#### Jireh Loreaux (Apr 15 2022 at 21:18):

First guess: try putting a . on the line after the imports.

#### Vasily Ilin (Apr 15 2022 at 21:19):

I know it's not a MWE. The problem is that each line takes a second or two, so as I try to make this example more minimal, the problem goes away

#### Jireh Loreaux (Apr 15 2022 at 21:20):

@Kyle Miller is this something that noncomputable! is supposed to help with? I don't really know the purpose of that yet.

#### Jireh Loreaux (Apr 15 2022 at 21:20):

By MWE, I mean that I don't have the Hopf file, so I can't open up what you sent me on my machine and have it compile to see if I can figure out where the problem is.

#### Vasily Ilin (Apr 15 2022 at 21:20):

I don't really understand why my maps aren't computable, by the way. Mathematically, they are very explicit

#### Yaël Dillies (Apr 15 2022 at 21:21):

This is because polynomials in mathlib are noncomputable by design.

#### Vasily Ilin (Apr 15 2022 at 21:22):

Jireh Loreaux said:

By MWE, I mean that I don't have the Hopf file, so I can't open up what you sent me on my machine and have it compile to see if I can figure out where the problem is.

My bad! I changed it now. Hopf just imports ring_theory.tensor_product

#### Vasily Ilin (Apr 15 2022 at 21:24):

Jireh Loreaux said:

First guess: try putting a . on the line after the imports.

What does that do?

#### Jireh Loreaux (Apr 15 2022 at 21:28):

I think it tells Lean to stop recompiling the stuff above, but I can't seem to find documentation to point you to. Maybe someone else can provide a better answer.

#### Yaël Dillies (Apr 15 2022 at 21:35):

The . prevents Lean from recompiling everything that's before in the same file. No point putting it just after the imports.

#### Yaël Dillies (Apr 15 2022 at 21:36):

What it does precisely is preventing Lean from recompiling what's before on a keystroke.

#### Kyle Miller (Apr 15 2022 at 21:41):

The way . works is that it's part of the definition syntax -- when it's there then Lean says to itself "ok, this is definitely the end of the definition." That way when you change stuff after the ., Lean can restart processing from that checkpoint without reprocessing starting from the checkpoint immediately preceding the definition.

#### Vasily Ilin (Apr 15 2022 at 21:44):

Ah, now that I put it after my definition, it works a lot faster! Thanks.

#### Jireh Loreaux (Apr 15 2022 at 21:45):

You can also use set_option profiler true to figure out where Lean is spending its time.

#### Kyle Miller (Apr 15 2022 at 21:46):

@Jireh Loreaux It seems like noncomputable! doesn't help. The breakdown from set_option profiler true is that it's spending most of the time elaborating (I'm guessing typeclass search?). What noncomputable! helps with is time spent compiling VM code by not spending time doing that, but it doesn't do very much when Lean tells you you need noncomputable (in that case, it's already not doing VM compilation).

#### Vasily Ilin (Apr 15 2022 at 21:47):

I am sorry but I have more questions. I am trying to use docs#polynomial.aeval_X. It uses a coersion of aeval. But my state has only a non-coerced aeval. Here is my state:

K: Type
_inst_1: comm_semiring K
⊢ ⇑((algebra.tensor_product.assoc K K[X] K[X] K[X]).symm.to_alg_hom.comp ((map (alg_hom.id K K[X]) (aeval (X ⊗ₜ[K] 1 + 1 ⊗ₜ[K] X))).comp (aeval (X ⊗ₜ[K] 1 + 1 ⊗ₜ[K] X)))) X = ⇑((map (aeval (X ⊗ₜ[K] 1 + 1 ⊗ₜ[K] X)) (alg_hom.id K K[X])).comp (aeval (X ⊗ₜ[K] 1 + 1 ⊗ₜ[K] X))) X


I want to rewrite aeval (X ⊗ₜ[K] 1 + 1 ⊗ₜ[K] X) X as X ⊗ₜ[K] 1 + 1 ⊗ₜ[K] X. Here is the full file:

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

variables (K : Type) [comm_semiring K]

noncomputable def counit : K[X] →ₐ[K] K := polynomial.aeval 0

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := polynomial.aeval ((polynomial.X ⊗ₜ 1) + (1 ⊗ₜ polynomial.X))

noncomputable def map1 : K[X] →ₐ K[X] ⊗ K[X] ⊗ K[X] := (algebra.tensor_product.assoc K K[X] K[X] K[X]).symm.to_alg_hom.comp ((map (alg_hom.id K K[X]) (comul K)).comp (comul K))

noncomputable def map2 : (K[X] →ₐ K[X] ⊗[K] K[X] ⊗[K] K[X] ) :=  (map (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) (alg_hom.id K K[X])).comp (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X])
.

lemma coassoc : map1 K = map2 K :=
begin
have P : map1 K X = map2 K X,
unfold map1,
unfold map2,
unfold comul,
rw aeval_X (X ⊗ₜ[K] 1 + 1 ⊗ₜ[K] X), -- why does this not work?
unfold algebra.tensor_product.assoc,

sorry,

end


#### Kyle Miller (Apr 15 2022 at 21:47):

The only thing noncomputable! does when Lean already wants noncomputable to be there is to skip a certain check that tends not to be very expensive.

#### Jireh Loreaux (Apr 15 2022 at 21:49):

docs#polynomial.aeval_X sorry, I didn't read well enough.

#### Jireh Loreaux (Apr 15 2022 at 21:58):

Right, so in this case, you have aeval as an alg_hom, because it's composed with other alg_homs. What you need is the lemma that says for alg_homs f and g, ⇑(f.comp g) x = ⇑f (⇑g x). However, you can instead do a squeeze_simp after your first three unfolds to get a nicer goal, and this also takes care of your issue. The result of squeeze_simp for me was:

simp only [alg_equiv.to_alg_hom_eq_coe, alg_hom.coe_comp, alg_equiv.coe_alg_hom, function.comp_app, aeval_X, _root_.map_add, map_tmul, alg_hom.coe_id, id.def, aeval_one],


#### Jireh Loreaux (Apr 15 2022 at 21:58):

The lemma I was mentioning is in this list: alg_hom.coe_comp as well as polynomial.aeval_X because they are both simp lemmas.

#### Vasily Ilin (Apr 15 2022 at 22:34):

Another question (sorry!):
how to I extract the actual map sending $a \otimes (b \otimes c)$ to $(a \otimes b) \otimes c$ from docs#algebra.tensor_product.assoc?

#### Adam Topaz (Apr 15 2022 at 22:41):

I suppose that map should do that on basic tensors by definition.

#### Alex J. Best (Apr 15 2022 at 23:44):

Yaël Dillies said:

The . prevents Lean from recompiling everything that's before in the same file. No point putting it just after the imports.

At least from the orange sidebars it looks like putting the . after the imports does do something, it stops lean thinking the imports have changed and rechecking them when you work near the top of a file

#### Alex J. Best (Apr 15 2022 at 23:45):

And the fact that the map on basic tensors does what it should is docs#algebra.tensor_product.assoc_tmul

#### Kyle Miller (Apr 15 2022 at 23:57):

It turns out . is a "command-like" that does nothing, so you can put in anywhere top-level commands can go, including right after the imports. That supports what @Alex J. Best suggests about it preventing import reprocessing. https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/parser.cpp#L2877

This is in addition to it being part of the syntax for definition commands. It signals "end of equations." https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/definition_cmds.cpp#L579

#### Kyle Miller (Apr 15 2022 at 23:58):

That's good to know. I usually put #check 37 or something right after the imports if I'm editing the first definition/theorem of a new file.

#### Kyle Miller (Apr 16 2022 at 00:00):

(I think the reason for . in the definition syntax is to let you write zero-equation definitions like example : false → false .. This reprocessing stuff is a side-effect.)

#### Yaël Dillies (Apr 16 2022 at 08:03):

Oh, so the two . are actually one and the same? Interesting!

#### Kevin Buzzard (Apr 16 2022 at 08:48):

@Vasily Ilin don't apologise for question spamming. We don't yet have extensive documentation and learning is made easier if you ask questions. The people subscribed to this stream are happy to help -- those that don't want to see a bunch of new members questions simply have this stream muted.

#### Kyle Miller (Apr 16 2022 at 16:35):

Yaël Dillies said:

Oh, so the two . are actually one and the same? Interesting!

I'm not sure what you mean exactly, but to be clear there are two different meanings for .: the first signifies end-of-equations for the def/theorem/lemma/instance/example commands, and the second is a do-nothing command (which is actually older! It was added by Leo in 2014 before you could even define or prove anything -- I'd guess the end-of-equations . was meant to feel like a special use of the do-nothing command). Lean makes checkpoints between commands, so in the end all that matters is that the . character is able to clearly demarcate the end of a command (or, in the case of an isolated ., the clear beginning and end of an entire command).

. is pretty overloaded, though, so it being clear depends on the command preceding it being complete. I was able to think of the following uses of .: separators for names, inaccessible patterns, tactic default arguments, decimal points for numeric literals, projection notation, end-of-equations, and the dot command.

#### Yaël Dillies (Apr 16 2022 at 16:38):

I got confused then. What you're describing is my understanding of things pre Kyle's yesterday message.

#### Kyle Miller (Apr 16 2022 at 16:40):

Yaël Dillies said:

The . prevents Lean from recompiling everything that's before in the same file. No point putting it just after the imports.

There's sometimes a point putting . right after the imports, since, being a command, it induces Lean to create a checkpoint that prevents import re-processing, which feels like it sometimes takes a few seconds.

#### Kyle Miller (Apr 16 2022 at 16:41):

But in the example, you were right that it wouldn't do anything, but it's since open_locale is a command, too, so editing further down in the file won't reprocess imports anyway.

#### Kyle Miller (Apr 16 2022 at 16:47):

Anyway, this has been another episode of Saturday morning Lean archaeology. (Morning for me at least, and while 2014 wasn't that long ago, it's a long time in Lean years.)

Last updated: Dec 20 2023 at 11:08 UTC