get the two maps from an isomorphism

Stream: new members

[Vasily Ilin]

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]

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]

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]

And similarly e.symm.to_linear_map for the inverse.

[Adam Topaz]

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]

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]

Adam Topaz said:

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]

It might be called docs#algebra_equiv.to_algebra_hom ?

[Eric Wieser]

docs#alg_equiv.to_alg_hom

[Adam Topaz]

Aha!

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

The names of the types are a bit harder to guess

[Vasily Ilin]

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]

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

[Adam Topaz]

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

[Vasily Ilin]

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

[Yaël Dillies]

No, unfortunately not :sad:

[Vasily Ilin]

Got it, thanks!

[Vasily Ilin]

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]

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]

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

[Vasily Ilin]

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]

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

[Jireh Loreaux]

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

[Jireh Loreaux]

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

[Vasily Ilin]

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]

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

[Jireh Loreaux]

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]

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

[Yaël Dillies]

This is because polynomials in mathlib are noncomputable by design.

[Vasily Ilin]

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]

Jireh Loreaux said:

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

What does that do?

[Jireh Loreaux]

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]

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

[Yaël Dillies]

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

[Kyle Miller]

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]

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

[Jireh Loreaux]

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

[Kyle Miller]

@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]

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]

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]

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

[Jireh Loreaux]

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]

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]

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]

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

[Alex J. Best]

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]

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

[Kyle Miller]

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]

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]

(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]

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

[Kevin Buzzard]

@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]

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]

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

[Kyle Miller]

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]

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]

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