Zulip Chat Archive

Stream: new members

Topic: Coercion nightmares


Antoine Chambert-Loir (Apr 05 2022 at 12:57):

A subgroup of a subgroup is a subgroup, but this proof looks ridiculous. Am I that much ignorant ?

import tactic

import group_theory.subgroup.basic

variable (α : Type*)

example :  (s : set α) (t : set s),  (u : set α),
   (a : α), a  u   (hs : a  s), (⟨a, hs : s)  t :=
begin
  intros s t,
  let j : s  α := λ x, x,
  use j '' t,
  intro a,
  split,
  { intro ha,
    simp only [set.mem_image, set_coe.exists] at ha,
    obtain b, hb, hb', hb'' := ha,
    suffices : a = b,
    { rw this, use hb, exact hb' },
    rw  hb'',
    refl },
  { rintro hs', hs''⟩,
    simp only [set.mem_image, set_coe.exists],
    use a, use hs', apply and.intro hs'',
    refl }
end

variable [ : group α]

example :  (G : @subgroup α ) (H : subgroup G),
   (H' : subgroup α),  (a : α), a  H' 
   (ha : a  G), (⟨a, ha : G)  H :=
begin
  intros G H,
  have j : G →* α := subgroup.subtype G,
  use H.map (G.subtype),
  intro a,
  split,
  { intro ha,
    simp only [subgroup.mem_map, exists_prop] at ha,
    obtain b, hb, hb' := ha,
    suffices : a = b,
    { have this': a  G,
      { rw this, exact set_like.coe_mem b, },
      use this',
      have this' : b = a, this'⟩,
      { exact subtype.eq (eq.symm this), },
      rw this' at hb, exact hb },
    rw  hb',
    refine congr _ rfl,
    refine subgroup.coe_subtype G },
  { rintro ha, ha'⟩,
    simp only [subgroup.mem_map, subgroup.coe_subtype, exists_prop],
    use (⟨a, ha⟩),
    apply and.intro ha',
    exact subtype.coe_mk a ha },
end

Kevin Buzzard (Apr 05 2022 at 13:01):

The trick is to use map and comap to push sets forwards and backwards along the map from \u s to alpha

Johan Commelin (Apr 05 2022 at 13:04):

And sometimes it turns out to be better to work with injective group homs.

Riccardo Brasca (Apr 05 2022 at 13:04):

The map is docs#subgroup.subtype

Antoine Chambert-Loir (Apr 05 2022 at 13:18):

The whole role of this is to be able teach Lean that fixing_subgroup (fixing_subgroup M s) t = fixing_subgroup M (s \cup t), but Lean resists…

Kevin Buzzard (Apr 05 2022 at 13:18):

example (s : set α) (t : set s) :  (u : set α),
   (a : α), a  u   (hs : a  s), (⟨a, hs : s)  t :=
begin
  -- move s, t before the colon to save `intro`
  use (coe : s  α) '' t, -- the map is already there and this is the simp normal form
  finish, -- this is now just logic nonsense, unpacking and repacking
end

some tips @Antoine Chambert-Loir

Antoine Chambert-Loir (Apr 05 2022 at 13:27):

I learn about finish!

Antoine Chambert-Loir (Apr 05 2022 at 13:30):

By the way, do you understand why I needed to specify @subgroup hM M (where hM : group M) in the second proof above ? — subgroup M didn't suffice to find an instance of group M.

Riccardo Brasca (Apr 05 2022 at 13:30):

This is weird

Riccardo Brasca (Apr 05 2022 at 13:32):

ah, wait, this is because you named the instance

Riccardo Brasca (Apr 05 2022 at 13:33):

variable [group α]

example :  (G : subgroup α) (H : subgroup G),
   (H' : subgroup α),  (a : α), a  H' 
   (ha : a  G), (⟨a, ha : G)  H :=

should be OK

Riccardo Brasca (Apr 05 2022 at 13:34):

If you give a name to a variable between square brackets, then Lean will not include it unless you mention it. So with variable [hα : group α] it doesn't know that α is a group

Antoine Chambert-Loir (Apr 05 2022 at 13:35):

In any case, now I can at least state what I wish to prove :

lemma certainly_easy_to_prove_nightmare_to_state {s t : set α} : fixing_subgroup M (s  t) =
  (fixing_subgroup (fixing_subgroup M s) t).map (fixing_subgroup M s).subtype :=
sorry

Riccardo Brasca (Apr 05 2022 at 13:35):

If you need to give it a name and use it several time you can write include hα.

Riccardo Brasca (Apr 05 2022 at 13:49):

It seems we are missing a reasonable API for fixing_subgroup. For example the first sorry here

variables {M : Type*} [group M] [mul_action M α]

lemma certainly_easy_to_prove_nightmare_to_state {s t : set α} : fixing_subgroup M (s  t) =
  (fixing_subgroup (fixing_subgroup M s) t).map (fixing_subgroup M s).subtype :=
begin
  ext x,
  split,
  { intros hx,
    refine ⟨⟨x, _⟩, _, _⟩⟩,
    { sorry },
    { sorry },
    { sorry } },
  { rintros hx y, hy₁ | hy₂⟩,
    { sorry },
    { sorry } }
end

should follow from some monotonicity of fixing_subgroup, that I don't find.

Kevin Buzzard (Apr 05 2022 at 13:50):

@Antoine Chambert-Loir

import tactic

import group_theory.subgroup.basic

variable (α : Type*)

example (s : set α) (t : set s) :  (u : set α),
   (a : α), a  u   (hs : a  s), (⟨a, hs : s)  t :=
begin
  use (coe : s  α) '' t,
  intro a,
  split,
  { -- We begin by abusing definitional equality and use the `rfl` trick.
    rintro ⟨⟨b, hbs⟩, hbt, rfl⟩, -- The `rfl` trick *defines* `a` to be `b`, substitutes in and then just rerases `a`.
    exact hbs, hbt }, -- Can now just make the term
  { rintro has, hat⟩,
    -- the proof should now be one line, of the form `exact ⟨⟨t₁, t₂⟩, ⟨t₃, t₄, t₅⟩⟩`.
    -- Let's *experiment* now in tactic mode, and then use the `refine` tactic to make the
    -- term we need.
    -- `use a`, Oh this made progress. I now randomly have two goals but they
    -- both look pretty simple. I'll take that.
    -- But actually `use` just ran the `refine` tactic on something else.
    -- Let's see what `use a` actually did:
    refine ⟨⟨a, _⟩, _⟩,  -- The two underscores are the new goals.
    { -- two goals so make a new bracket
      -- `use has` closes this goal! Now let's think about how to write it using `refine`
      exact has, }, -- the first `_` was just the term `has`.
    { -- second goal
      -- `apply and.intro hat,` looks like a good first move. But `apply` just used `refine`:
      refine and.intro hat _,
      refl -- now solves the goal!
       -- but if the proof was refl we can just use `rfl` on the previous line
    }
  }
  -- Therefore, the one line proof is `exact ⟨⟨a, has⟩, and.intro hat rfl⟩`,
end

Antoine Chambert-Loir (Apr 05 2022 at 13:53):

@Riccardo Brasca , Yes, docs#fixing_subgroup `is defined « par la bande » in the files devoted to Galois theory. I believe one needs to transfer them somewhere in the files related to docs#mul_action, as well as adding much stuff. For example, I found useful to have

lemma mem_fixing_subgroup_iff (s : set α) (g : M) :
  g  fixing_subgroup M s   (y : α) (hy : y  s), g  y = y := λ hg y hy, hg y, hy⟩, λ h y, hy⟩, h y hy

Riccardo Brasca (Apr 05 2022 at 13:54):

I totally agree that lemma should be immediately after the definition, that should be elsewhere

Riccardo Brasca (Apr 05 2022 at 13:55):

There is docs#mul_action.stabilizer

Riccardo Brasca (Apr 05 2022 at 13:56):

With an API, but it is for a singleton (I didn't check the whole file).

Kevin Buzzard (Apr 05 2022 at 13:59):

example (s : set α) (t : set s) :  (u : set α),
   (a : α), a  u   (hs : a  s), (⟨a, hs : s)  t :=
⟨(coe : s  α) '' t,λ a, by {rintro ⟨⟨b, hbs⟩, hbt, rfl⟩,exact hbs, hbt⟩},
  -- no rfl trick here so can do it all in term mode
  λ ha, ⟨⟨a, ha.some⟩, ha.some_spec, rfl⟩⟩⟩⟩

Kevin Buzzard (Apr 05 2022 at 14:01):

The rfl trick in rintro involves a "deep eq.rec" so you don't want to translate it into term mode, my guess is that the term generated by the rintro rfl tactic is really nasty.

Kevin Buzzard (Apr 05 2022 at 14:01):

Oh by the way I used the axiom of choice with exists.some and exists.some_spec

Reid Barton (Apr 05 2022 at 15:02):

quite unnecessarily though: λ ⟨ha₁, ha₂⟩, ⟨⟨a, ha₁⟩, ⟨ha₂, rfl⟩⟩

Kevin Buzzard (Apr 05 2022 at 16:48):

I thought that term mode lambda pointies were discouraged!

Reid Barton (Apr 05 2022 at 16:48):

Only for defining data

Reid Barton (Apr 05 2022 at 16:51):

It will produce a term with a whatever.rec in a place that usually isn't the best place for it

Reid Barton (Apr 05 2022 at 16:51):

but for a proof we don't care


Last updated: Dec 20 2023 at 11:08 UTC