Zulip Chat Archive

Stream: Is there code for X?

Topic: injections to equiv


Joachim Breitner (Jan 14 2022 at 15:43):

Where would I find A ↪ B → B ↪ A → A ≃ B?

Adam Topaz (Jan 14 2022 at 15:44):

This would involve cardinals, so I would look in that part of mathlib.

Eric Wieser (Jan 14 2022 at 15:44):

That's not going to be computable, right?

Adam Topaz (Jan 14 2022 at 15:44):

No of course not.

Joachim Breitner (Jan 14 2022 at 15:46):

Hmm, should I try harder to think about computable proofs to have an easier time finding lemmas :-)

Eric Wieser (Jan 14 2022 at 15:46):

I would say that if your conclusion is an equiv that is obviously not computable, in general you should probably be looking for lemmas with the conclusion #A = #B

Adam Topaz (Jan 14 2022 at 15:46):

docs#cardinal.eq

Eric Wieser (Jan 14 2022 at 15:46):

(or fintype.card A = fintype.card B)

Eric Wieser (Jan 14 2022 at 15:47):

docs#function.embedding.cardinal_le also seems helpful

Adam Topaz (Jan 14 2022 at 15:47):

docs#cardinal.mk_le_of_injective

Eric Wieser (Jan 14 2022 at 15:48):

So (cardinal.eq.1 (le_antisymm f.cardinal_le g.cardinal_le)).some?

Adam Topaz (Jan 14 2022 at 15:50):

Ungolfed:

import set_theory.cardinal

open_locale cardinal classical

noncomputable example {α β : Type*} : (α  β)  (β  α)  (α  β) :=
begin
  intros h1 h2,
  suffices : #α = #β, by { rw cardinal.eq at this, exact this.some },
  apply le_antisymm,
  apply cardinal.mk_le_of_injective h1.2,
  apply cardinal.mk_le_of_injective h2.2,
end

Adam Topaz (Jan 14 2022 at 15:51):

Oh yeah, nice trick with the embedding.cardinal_le

Joachim Breitner (Jan 14 2022 at 15:51):

Good point, may be more natural via inequality on cardinals. I’ll try that.

Joachim Breitner (Jan 14 2022 at 15:51):

Do I have to do something special to get the # syntax? Is this the open_local cardinal? Can I do that within beginend?

Adam Topaz (Jan 14 2022 at 15:52):

open_locale cardinal should before the statement

Eric Wieser (Jan 14 2022 at 15:52):

inequality on cardinals is just le_antisymm f.cardinal_le g.cardinal_le, so definitely more natural

Reid Barton (Jan 14 2022 at 15:53):

This is actually nearly the exact statement of docs#function.embedding.antisymm which is what is used to prove le_antisymm for cardinal in the first place.

Adam Topaz (Jan 14 2022 at 15:53):

Here is Eric's code, in mwe form:

import set_theory.cardinal

open_locale cardinal

noncomputable example {α β : Type*} : (α  β)  (β  α)  (α  β) := λ h1 h2,
(cardinal.eq.1 $ le_antisymm h1.cardinal_le h2.cardinal_le).some

Adam Topaz (Jan 14 2022 at 15:54):

And Reid's proof:

noncomputable example {α β : Type*} : (α  β)  (β  α)  (α  β) := λ h1 h2,
(h1.antisymm h2).some

Adam Topaz (Jan 14 2022 at 15:55):

We have docs#function.embedding.schroeder_bernstein if you want the bare statements with injective hypotheses.

Joachim Breitner (Jan 14 2022 at 16:03):

Ok, beginner question, hope that's ok: how do I go from

Hcard : nonempty (A  free_group A)
 A  free_group A

(it’s all noncomputable anyways here.)

Anne Baanen (Jan 14 2022 at 16:03):

docs#nonempty.some

Anne Baanen (Jan 14 2022 at 16:04):

(Which is sugar for docs#classical.choice, which is the axiom of choice in Lean)

Joachim Breitner (Jan 14 2022 at 16:04):

Thanks! :-)

Adam Topaz (Jan 14 2022 at 16:11):

@Joachim Breitner Do I understand correctly that you're proving the fact that free_group A being isomorphic to free_grroup B implies that A is in bijection with B? If so, then I should mention that we have docs#basis and it might be worthwhile to prove that the image of the canonical map XF(X)F(X)abX \to F(X) \to F(X)^{ab} gives a basis for F(X)abF(X)^{ab} when considered as a Z\mathbb{Z}-module. I think that could be a useful construction anyway (if we don't already have it).

Adam Topaz (Jan 14 2022 at 16:13):

It looks like we don't have the statement in terms of a basis, but we do have docs#free_abelian_group.equiv_finsupp

Joachim Breitner (Jan 14 2022 at 16:13):

That’s my goal indeed. I guess I am am unreasonably attached to the proof that I did in Isabelle before, arguing via cardinalities in the infinite case, and via Hom(FX,C2)Hom(F_X, C_2) in the finite case.

Adam Topaz (Jan 14 2022 at 16:14):

The basis structure is a relatively recent addition to mathlib!

Joachim Breitner (Jan 14 2022 at 16:14):

But I see it it’s hard to defend doing it that way (as much fun as it is) when an easier proof is possible…

Adam Topaz (Jan 14 2022 at 16:15):

I just think that the proof could be 1-2 lines long with the results we already have in mathlib.

Joachim Breitner (Jan 14 2022 at 16:19):

Fair enough. So I go from free_group A to free_abelian_group X (by def) then to X →₀ ℤ, and then find the lemma that shows that a basis of X →₀ ℤ is X, and that bases are in bijection.

Kevin Buzzard (Jan 14 2022 at 16:25):

Do we have that all bases are the same size for free Z\Z-modules?

Adam Topaz (Jan 14 2022 at 16:25):

docs#basis.index_equiv

Adam Topaz (Jan 14 2022 at 16:26):

I started trying out some code, but it looks like we're missing some API for abelianizations:

import linear_algebra.dimension
import group_theory.free_abelian_group_finsupp

variables {α β : Type*} (e : free_group α ≃* free_group β)

noncomputable def free_abelian_group.basis {α : Type*} : basis α  (free_abelian_group α) :=
⟨(free_abelian_group.equiv_finsupp α).to_linear_equiv $ by tidy

include e

def free_abelian_group.equiv_of_free_group : free_abelian_group α ≃+ free_abelian_group β :=
mul_equiv.to_additive $ sorry

Joachim Breitner (Jan 14 2022 at 16:32):

Do we have that all bases are the same size for free Z\ZZ-modules?

I’m looking for that, but I can’t find it (not that I have practice looking for stuff)

Adam Topaz (Jan 14 2022 at 16:33):

It's docs#basis.index_equiv

Anne Baanen (Jan 14 2022 at 16:35):

In particular, docs#invariant_basis_number_of_nontrivial_of_comm_ring

Joachim Breitner (Jan 14 2022 at 16:38):

Ah, different file. Thanks!

Adam Topaz (Jan 14 2022 at 16:40):

import linear_algebra.dimension
import group_theory.free_abelian_group_finsupp

variables {α β : Type*} (e : free_group α ≃* free_group β)

def int_linear_equiv_of_add_equiv {α β : Type*} [add_comm_group α] [add_comm_group β]
  (e : α ≃+ β) : α ≃ₗ[] β :=
e.to_linear_equiv $ λ c a, by { erw e.to_add_monoid_hom.map_zsmul, refl }

noncomputable def free_abelian_group.basis (α : Type*) : basis α  (free_abelian_group α) :=
int_linear_equiv_of_add_equiv (free_abelian_group.equiv_finsupp α)⟩


def abelianization.equiv_of_equiv {G H : Type*} [group G] [group H] (e : G ≃* H) :
  abelianization G ≃* abelianization H :=
{ to_fun := abelianization.lift $ abelianization.of.comp e.to_monoid_hom,
  inv_fun := abelianization.lift $ abelianization.of.comp e.symm.to_monoid_hom,
  left_inv := begin
    rintros a⟩,
    -- Missing dsimp lemma `quot.mk _ a = abelianization.of a`,
    change abelianization.lift _ (abelianization.lift _ (abelianization.of a)) = abelianization.of a,
    simp,
  end,
  right_inv := begin
    rintros a⟩,
    -- Missing dsimp lemma `quot.mk _ a = abelianization.of a`,
    change abelianization.lift _ (abelianization.lift _ (abelianization.of a)) = abelianization.of a,
    simp,
  end,
  map_mul' := by tidy }

include e

def free_abelian_group.equiv_of_free_group : free_abelian_group α ≃+ free_abelian_group β :=
mul_equiv.to_additive $ abelianization.equiv_of_equiv e

def free_abelian_group.linear_equiv_of_free_group : free_abelian_group α ≃ₗ[] free_abelian_group β :=
int_linear_equiv_of_add_equiv (free_abelian_group.equiv_of_free_group e)

noncomputable
def equiv.of_free_group_equiv : α  β :=
let t : basis α  (free_abelian_group β) := (free_abelian_group.basis α).map $
  free_abelian_group.linear_equiv_of_free_group e in t.index_equiv $ free_abelian_group.basis _

Adam Topaz (Jan 14 2022 at 16:42):

I'm surprised that these various initial constructions are not in mathlib already (or maybe I missed them?).

Anne Baanen (Jan 14 2022 at 16:44):

I hope we can get int_linear_equiv_of_add_equiv for free by instead instantiating something like [add_comm_group A] [add_comm_group B] : linear_equiv_class ℤ (A →+ B) A B. But that will take a bit more development effort.

Eric Wieser (Jan 14 2022 at 16:44):

We have docs#add_monoid_hom.to_int_linear_map but seemingly not the equiv version (which would live in file#data/equiv/module)

Joachim Breitner (Jan 14 2022 at 16:44):

Nice. I’ll look for beginner-friendly low-hanging fruit elsewhere :-)

Adam Topaz (Jan 14 2022 at 16:45):

There is plenty of low hanging fruit in the proof above, since the first few constructions should have already been in mathlib.

Eric Wieser (Jan 14 2022 at 16:46):

And the related nat and rat versions of to_int_linear_equiv should also be added

Adam Topaz (Jan 14 2022 at 16:46):

I was hoping to just be able to write the last 4 lines :)

Eric Wieser (Jan 14 2022 at 16:46):

Adding those three is definitely a beginner-friendly PR

Eric Wieser (Jan 14 2022 at 16:48):

I guess abelianization.equiv_of_equiv could be mul_equiv.abelianization_congr to match docs#equiv.finset_congr and enable dot notation?

Eric Wieser (Jan 14 2022 at 16:49):

I think we're pretty inconsistent about how to name those though (eg docs#free_group.free_group_congr)

Joachim Breitner (Jan 14 2022 at 16:50):

Shall I copy these lines into a PR and paste the link here, and you can comment there how to name them and where to put them? Or is that not faster than if one of you just puts them there?

Eric Wieser (Jan 14 2022 at 16:51):

I would probably make separate PRs for the unrelated content. Your build time will be shorter

Adam Topaz (Jan 14 2022 at 16:51):

(And your review time ;))

Joachim Breitner (Jan 14 2022 at 16:51):

So one for each independent lemma?

Eric Wieser (Jan 14 2022 at 16:53):

Is the actual noncomputable bit in the example above docs#basis.index_equiv?

Adam Topaz (Jan 14 2022 at 16:53):

I would say, one PR for the int_linear_equiv_of_add_equiv (or whatever other name we want), one for free_abelian_group.basis, one for abelianization.equiv_of_equiv (or whatever name we want) which should include the missing dsimp lemma, and one for the final result.

Eric Wieser (Jan 14 2022 at 16:53):

It annoys me that basis terms, which are in my mind a computable way to do linear algebra, are noncomputable by default due to the design of finsupp.

Patrick Massot (Jan 14 2022 at 16:54):

Joachim, it's pretty common for new user to open mathlib PRs whose content was mostly written by other people here while answering questions. You still save work for Adam by putting those lemmas or definitions in their correct location and think a bit about possible generalization or a couple of extra helper lemma (for instance I see comments in Adam's code saying some lemmas are missing). And then you'll experience the PR process, which requires some time to get used to.

Joachim Breitner (Jan 14 2022 at 17:19):

Where would you expect free_abelian_group.basis to end up? It depends on free_abelian_group_finsupp and on wherever int_linear_equiv_of_add_equiv ends up (maybe algebra/algebra/basic), neither of which depend on each other so far.

Johan Commelin (Jan 14 2022 at 17:37):

I think close to free_abelian_group_finsupp would make sense.

Johan Commelin (Jan 14 2022 at 17:38):

That's in a leaf file of mathlib, I think. It's fine to add a dependency to it, so that int_linear_equiv_of_add_equiv is available there.


Last updated: Dec 20 2023 at 11:08 UTC