injections to equiv

Stream: Is there code for X?

[Joachim Breitner]

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

[Adam Topaz]

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

[Eric Wieser]

That's not going to be computable, right?

[Adam Topaz]

No of course not.

[Joachim Breitner]

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

[Eric Wieser]

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]

docs#cardinal.eq

[Eric Wieser]

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

[Eric Wieser]

docs#function.embedding.cardinal_le also seems helpful

[Adam Topaz]

docs#cardinal.mk_le_of_injective

[Eric Wieser]

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

[Adam Topaz]

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]

Oh yeah, nice trick with the embedding.cardinal_le

[Joachim Breitner]

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

[Joachim Breitner]

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

[Adam Topaz]

open_locale cardinal should before the statement

[Eric Wieser]

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

[Reid Barton]

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]

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]

And Reid's proof:

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

[Adam Topaz]

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

[Joachim Breitner]

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]

docs#nonempty.some

[Anne Baanen]

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

[Joachim Breitner]

Thanks! :-)

[Adam Topaz]

@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 $X \to F(X) \to F(X)^{ab}$ gives a basis for $F(X)^{ab}$ when considered as a $\mathbb{Z}$-module. I think that could be a useful construction anyway (if we don't already have it).

[Adam Topaz]

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]

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(F_X, C_2)$ in the finite case.

[Adam Topaz]

The basis structure is a relatively recent addition to mathlib!

[Joachim Breitner]

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]

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

[Joachim Breitner]

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]

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

[Adam Topaz]

docs#basis.index_equiv

[Adam Topaz]

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]

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]

It's docs#basis.index_equiv

[Anne Baanen]

In particular, docs#invariant_basis_number_of_nontrivial_of_comm_ring

[Joachim Breitner]

Ah, different file. Thanks!

[Adam Topaz]

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]

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

[Anne Baanen]

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]

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]

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

[Adam Topaz]

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

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

Adding those three is definitely a beginner-friendly PR

[Eric Wieser]

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

[Eric Wieser]

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

[Joachim Breitner]

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]

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

[Adam Topaz]

(And your review time ;))

[Joachim Breitner]

So one for each independent lemma?

[Eric Wieser]

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

[Adam Topaz]

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]

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]

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]

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]

I think close to free_abelian_group_finsupp would make sense.

[Johan Commelin]

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.