Working "through" an isomorphism

Stream: new members

[Philippe Duchon]

It is common in informal mathematics to say something like, "we know these two [groups/rings/whatever] $A$ and $B$ are isomorphic, and we proved this property in $A$, so it also holds in $B$" (or even to not say it explicitly), but what is the Lean way of doing it formally?

Here is a concrete example (equidivisibility in monoids, which is part of some existing characterizations of free monoids; it seems like a good example since it includes existential and universal quantifiers):

mwe:

import Mathlib

variable (A B: Type) [Monoid A] [Monoid B] (hAB: A ≃* B)

def equidivisible (A: Type) [Monoid A] := ∀ u v u' v': A, u * v = u' * v' →
  ∃ w, (u' = u * w ∧ v = w * v') ∨ (u = u' * w ∧ v' = w * v)

theorem by_iso (hAB: A ≃* B) (hA: equidivisible A) : equidivisible B := by
  intro U V U' V' hUV
  sorry

The plan is clear: use the reverse isomorphism hAB.symm to obtain terms of type $A$ corresponding to my variables of type $B$, prove the $A$ variant of hUV, apply hA to obtain the relevant term of type $A$, and prove that its image by hAB satisfies the required condition. This is already pretty tedious, and it's just with a few quantifiers and a single premise.

Is there a tactic to automate this, or should one do it on a case by case basis, using the API for the relevant algebraic structure (here, monoids)?

[Kevin Buzzard]

There was a tactic for this once, but I don't think it ever got ported, because (much to my surprise) this concept turned out to be less common than we thought, and often when we did need it we could deduce it from a more general result. I'll explain the more general result in your case now.

Here's four maths questions. Are any of the following true? (I pretty sure that none of them are, unfortunately). If A injects into B then A equidivisible => B equidivisible. If A surjects onto B then A equidivisible => B equidivisible. If A injects into B then B equidivisible => A equidivisible. If A surjects onto B then B equidivisible => A equidivisible. If any of these are true then such a result would need to go into the API for equidivisibility and one would not expect an isomorphism tactic to magically prove such a result because it lies deeper. However any such result would imply the isomorphism result which you want. In practice in Lean for many examples, one of the four analogous results is true, so we prove that manually and deduce the isomorophism result from it.

[Kevin Buzzard]

One person's tedious is another person's "fun problem to distract them because their next job is to plough through their email" (which is even more tedious):

import Mathlib

variable (A B : Type) [Monoid A] [Monoid B]

def equidivisible (A : Type) [Monoid A] := ∀ u v u' v' : A, u * v = u' * v' →
  ∃ w, (u' = u * w ∧ v = w * v') ∨ (u = u' * w ∧ v' = w * v)

theorem by_iso (e : A ≃* B) (hB : equidivisible B) : equidivisible A := by
  intro U V U' V' hUV
  obtain ⟨w, hw⟩ := hB (e U) (e V) (e U') (e V') (by simp [← map_mul, hUV])
  use (e.symm w)
  rcases hw with ⟨hw1a, hw1b⟩ | ⟨hw2a, hw2b⟩
  · left
    constructor
    · apply_fun e.symm at hw1a
      simp_all
    · apply_fun e.symm at hw1b
      simp_all
  · right
    constructor
    · apply_fun e.symm at hw2a
      simp_all
    · apply_fun e.symm at hw2b
      simp_all

[Kenny Lau]

Kevin Buzzard said:

There was a tactic for this once, but I don't think it ever got ported, because (much to my surprise) this concept turned out to be less common than we thought, and often when we did need it we could deduce it from a more general result

this seems like a case of local optimisation vs global optimisation, sure for each individual lemma the surjective/injective form is more useful, but as a whole i think we should have transport tactics

[Philippe Duchon]

Kevin Buzzard said:

One person's tedious is another person's "fun problem to distract them because their next job is to plough through their email" (which is even more tedious):

Never underestimate the threat of emails when it comes to making people work for you (thanks!).

So maybe tedious wasn't the right word, but it's repetitive enough. And I suspect doing the same for a property with more quantifier alternations would be even more so (though I don't have a good example at hand).

[Kevin Buzzard]

Kenny Lau said:

but as a whole i think we should have transport tactics

There is a cost-benefit analysis to be done here; right now tactics are hard to write and there are only a small number of experts who can do it (far far fewer than the number of people who can knock off that proof above). I think the fact that we've got this far without such a tactic is an indication that it's not high priority, and because there are so many more high priority things for the tactic people (did you see field by the way, it's awesome and it just landed) stuff like transport tends not to get done.

IIRC @Kim Morrison even had some prototype transport working that would even prove that compactness transferred along continuous surjections (the thing which I said above that a transport tactic would obviously not do, because surjections aren't bijections in general). Or am I dreaming?

[Ruben Van de Velde]

Did you try if grind helped with any of those?

[Philippe Duchon]

I just did (I'm totally unfamiliar with grind, having only read about it a bit here), but it doesn't work straight out of the box.

[Ruben Van de Velde]

It tends to be good at "quantifier shuffling", but I guess there's a little too much mathematical content

[Bryan Wang]

There was a related thread about transport here

[Anthony Wang]

Kevin Buzzard said:

One person's tedious is another person's "fun problem to distract them because their next job is to plough through their email" (which is even more tedious):

import Mathlib

variable (A B : Type) [Monoid A] [Monoid B]

def equidivisible (A : Type) [Monoid A] := ∀ u v u' v' : A, u * v = u' * v' →
  ∃ w, (u' = u * w ∧ v = w * v') ∨ (u = u' * w ∧ v' = w * v)

theorem by_iso (e : A ≃* B) (hB : equidivisible B) : equidivisible A := by
  intro U V U' V' hUV
  obtain ⟨w, hw⟩ := hB (e U) (e V) (e U') (e V') (by simp [← map_mul, hUV])
  use (e.symm w)
  rcases hw with ⟨hw1a, hw1b⟩ | ⟨hw2a, hw2b⟩
  · left
    constructor
    · apply_fun e.symm at hw1a
      simp_all
    · apply_fun e.symm at hw1b
      simp_all
  · right
    constructor
    · apply_fun e.symm at hw2a
      simp_all
    · apply_fun e.symm at hw2b
      simp_all

You can replace the rcases block with just a single line, so it's actually not even that tedious.

theorem by_iso (e : A ≃* B) (hB : equidivisible B) : equidivisible A := by
  intro U V U' V' hUV
  obtain ⟨w, hw⟩ := hB (e U) (e V) (e U') (e V') (by simp [← map_mul, hUV])
  simp [← EmbeddingLike.apply_eq_iff_eq e.symm] at hw
  use (e.symm w)

[Eric Wieser]

I would guess that e.surjective.exists is useful here too

[Aaron Liu]

easy, no stress

import Mathlib

variable (A B : Type) [Monoid A] [Monoid B]

def equidivisible (A : Type) [Monoid A] := ∀ u v u' v' : A, u * v = u' * v' →
  ∃ w, (u' = u * w ∧ v = w * v') ∨ (u = u' * w ∧ v' = w * v)

theorem by_iso (e : A ≃* B) (hB : equidivisible B) : equidivisible A := by
  unfold equidivisible at hB ⊢
  simp_rw [e.forall_congr_left, e.exists_congr_left]
  simp_rw [← e.symm.injective.eq_iff, map_mul] at hB
  exact hB

[Kenny Lau]

one could make that into a tactic