lost in confusion

Stream: new members

[Antoine Chambert-Loir]

After some upgrade of mathlib, some of my code broke with an error message of the form:

term
  hf
has type
  function.bijective ⇑f
but is expected to have type
  function.bijective ⇑?m_5

If I try to fill some implicit arguments, I get a different error,

term
  f
has type
  ↥s →ₑ[φ] ↥s : Type u_1
but is expected to have type
  ?m_1 →ₑ[φ] ?m_2 : Type (max ? ?)

Can anybody help me guess what happens…

[Adam Topaz]

Possibly a universe issue?

[Adam Topaz]

do you have a #mwe you can share?

[Antoine Chambert-Loir]

It's hard to give a #mwe, because this happens after many many files of sthing which is not yet in mathlib.

[Adam Topaz]

I guess I don't even know what →ₑ[φ] is notation for...

[Antoine Chambert-Loir]

I just tried to build a #mwe by introducing the notation and some sorry, but even there I have a problem:

import tactic

def is_preprimitive (M : Type*) [group M] (α : Type*) [mul_action M α] : Prop := sorry

structure equivariant_map {M N : Type*} (φ : M → N)
  (α : Type*) (β : Type*) [has_smul M α] [has_smul N β] :=
(to_fun : α → β)
(map_smul' : ∀ (m : M) (a : α), to_fun (m • a) = φ(m) • to_fun (a))

notation α ` →ₑ[`:25 φ:25 `] `:0 β:0 := equivariant_map φ α β
notation α ` →[`:25 M:25 `] `:0 β:0 := equivariant_map (@id M) α β

variables (M N : Type*) [group M] [group N] (α β : Type*) [mul_action M α] [mul_action N β]

lemma is_preprimitive_of_bijective_map_iff
  {φ : M → N} {f : α →ₑ[φ] β}
  (hφ : function.surjective φ) (hf : function.bijective f) :
  is_preprimitive M α ↔ is_preprimitive N β := sorry

[Antoine Chambert-Loir]

On the hf : function.bijective f, Lean complains:

type mismatch at application
  function.bijective f
term
  f
has type
  α →ₑ[φ] β : Type (max u_3 u_4)
but is expected to have type
  ?m_1 → ?m_2 : Sort (imax ? ?)

[Adam Topaz]

import tactic

def is_preprimitive (M : Type*) [group M] (α : Type*) [mul_action M α] : Prop := sorry

structure equivariant_map {M N : Type*} (φ : M → N)
  (α : Type*) (β : Type*) [has_smul M α] [has_smul N β] :=
(to_fun : α → β)
(map_smul' : ∀ (m : M) (a : α), to_fun (m • a) = φ(m) • to_fun (a))

notation α ` →ₑ[`:25 φ:25 `] `:0 β:0 := equivariant_map φ α β
notation α ` →[`:25 M:25 `] `:0 β:0 := equivariant_map (@id M) α β

variables (M N : Type*) [group M] [group N] (α β : Type*) [mul_action M α] [mul_action N β]

instance {φ : M → N} : has_coe_to_fun (α →ₑ[φ] β) (λ _, α → β) := ⟨equivariant_map.to_fun⟩

lemma is_preprimitive_of_bijective_map_iff
  {φ : M → N} {f : α →ₑ[φ] β}
  (hφ : function.surjective φ) (hf : function.bijective f) :
  is_preprimitive M α ↔ is_preprimitive N β := sorry

[Adam Topaz]

you need to tell lean how it should think of terms of α →ₑ[φ] β as functions

[Adam Topaz]

presumably using docs#fun_like is the right approach in this case.

[Adam Topaz]

So:

import tactic

def is_preprimitive (M : Type*) [group M] (α : Type*) [mul_action M α] : Prop := sorry

structure equivariant_map {M N : Type*} (φ : M → N)
  (α : Type*) (β : Type*) [has_smul M α] [has_smul N β] :=
(to_fun : α → β)
(map_smul' : ∀ (m : M) (a : α), to_fun (m • a) = φ(m) • to_fun (a))

notation α ` →ₑ[`:25 φ:25 `] `:0 β:0 := equivariant_map φ α β
notation α ` →[`:25 M:25 `] `:0 β:0 := equivariant_map (@id M) α β

variables (M N : Type*) [group M] [group N] (α β : Type*) [mul_action M α] [mul_action N β]

instance foo {φ : M → N} : fun_like (α →ₑ[φ] β) α (λ _, β) :=
{ coe := equivariant_map.to_fun,
  coe_injective' := λ f g h, by { cases f, cases g, simpa } }

lemma is_preprimitive_of_bijective_map_iff
  {φ : M → N} {f : α →ₑ[φ] β}
  (hφ : function.surjective φ) (hf : function.bijective f) :
  is_preprimitive M α ↔ is_preprimitive N β := sorry

[Adam Topaz]

Does that solve the original issue?

[Antoine Chambert-Loir]

I'm polishing my mwe, I hadn't copied enough…

[Antoine Chambert-Loir]

This seems to replicate my issue (and bring no other…)

import tactic


import algebra.group.defs
import data.set.pointwise
import group_theory.group_action.defs
import group_theory.specific_groups.alternating


def is_preprimitive (M : Type*) [group M] (α : Type*) [mul_action M α] : Prop := sorry

variables (M N : Type*) [group M] [group N] (α β : Type*) [mul_action M α] [mul_action N β]

open_locale pointwise classical

/-- The instance that makes the stabilizer of a set acting on that set -/
instance mul_action.of_stabilizer (s : set α) :
  mul_action (mul_action.stabilizer M s) s := sorry

structure equivariant_map {M N : Type*} (φ : M → N)
  (α : Type*) (β : Type*) [has_smul M α] [has_smul N β] :=
(to_fun : α → β)
(map_smul' : ∀ (m : M) (a : α), to_fun (m • a) = φ(m) • to_fun (a))

notation α ` →ₑ[`:25 φ:25 `] `:0 β:0 := equivariant_map φ α β
notation α ` →[`:25 M:25 `] `:0 β:0 := equivariant_map (@id M) α β

class equivariant_map_class (F : Type*) (α β : out_param $ Type*)
  (M N : Type*) (φ : M → N) [has_smul M α] [has_smul N β]
  extends fun_like F α (λ _, β) :=
(map_smul : ∀ (f : F) (m : M) (a : α), f (m • a) = φ(m) • f(a))


instance (M N : Type*) [group M] [group N] (α β : Type*) [mul_action M α] [mul_action N β] (φ: M → N): has_coe_to_fun (α →ₑ[φ] β) (λ _, α → β) := ⟨equivariant_map.to_fun⟩


lemma is_preprimitive_of_bijective_map_iff
  {φ : M → N} {f : α →ₑ[φ] β}
  (hφ : function.surjective φ) (hf : function.bijective f) :
  is_preprimitive M α ↔ is_preprimitive N β := sorry


variables [fintype α] [decidable_eq α]

lemma stabilizer.is_preprimitive (s : set α) (hs : (sᶜ : set α).nontrivial):
  is_preprimitive (mul_action.stabilizer (alternating_group α) s) s :=
begin
  let φ : mul_action.stabilizer (alternating_group α) s → equiv.perm s := mul_action.to_perm,
  suffices hφ : function.surjective φ,

  let f : s →ₑ[φ] s := {
  to_fun := id,
  map_smul' := sorry },
  have hf : function.bijective f := function.bijective_id,
  rw is_preprimitive_of_bijective_map_iff hφ hf,
  sorry,
end

[Antoine Chambert-Loir]

The problem appears at the very end, Lean doesn't want to use hf…

[Adam Topaz]

I can get rid of the error by replacing rw is_preprimitive_of_bijective_map_iff hφ hf, with rw is_preprimitive_of_bijective_map_iff _ _ _ _ hφ hf,

[Antoine Chambert-Loir]

You're right. This shows that my #mwe does not make the problem appear, while it appears in real life…

[Adam Topaz]

if you have your actual code in a branch of mathlib or some separate repo, you could share a link?

[Antoine Chambert-Loir]

Yes, this is branch#acl-Wielandt
The problem is in alternating_iwasawa.lean
It appears on line 350, and there are similar issues below.

[Antoine Chambert-Loir]

I'm totally confused and so grateful for your help…

[Adam Topaz]

I got the branch and I'm trying to build that file now.

[Adam Topaz]

I'm getting could not resolve import: mul_action_finset. Is there a file missing?

[Antoine Chambert-Loir]

Yes… I had forgotten to add this file to the commit…

[Adam Topaz]

it's not an issue for the error in question, I'm just wondering

[Adam Topaz]

it looks like there might be a diamond.

[Antoine Chambert-Loir]

I have moved the contentious lemma in another file, and I get different problems…

[Adam Topaz]

example (s : set α) : true :=
begin
  let I1 : has_smul (stabilizer (alternating_group α) s) s :=
    mul_action.to_has_smul,
  let I2 : has_smul (stabilizer (alternating_group α) s) s :=
    has_smul.stabilizer _ _,
  have : I1 = I2 := rfl -- FAILS
end

[Adam Topaz]

let me try to extract a minimal example

[Antoine Chambert-Loir]

I might have defined twice this has_smul ?

[Adam Topaz]

no I think these are both in mathlib somewhere

[Adam Topaz]

oh maybe has_smul.stabilizer is not?

[Adam Topaz]

Ah! Yeah, this is from your file jordan/for_mathlib/stabilizer

[Adam Topaz]

Okay, so I think we understand the issue -- it's a diamond caused by this isntance

[Adam Topaz]

The reason that the has_smul instances are not defeq is because your version of has_smul.stabilizer uses pattern matching whereas mathlib's version uses projections. For example, if you change your definition to

/-- The instance that makes the stabilizer of a set acting on that set -/
instance has_smul.stabilizer (s : set α) :
  has_smul ↥(stabilizer G s) ↥s := {
smul := λ g x, ⟨(g : G) • x,
  begin
    sorry
  end⟩, }

then the error problematic diamond disappears.

Of course, the correct solution is to just use mathlib's instance :)

[Adam Topaz]

hmmm actually I can't seem to find the action of the stabilizer of a set on the set itself. Is that something that was recently added to mathlib?

[Adam Topaz]

Ah no it's not in mathlib! But the difference is caused by the internals of docs#sub_mul_action.mul_action

[Adam Topaz]

again, it stems from the pattern-matching vs. projection issue

[Eric Wieser]

I think there is a recent PR where I discussed adding stabilizer actions

[Eric Wieser]

Annoyingly they don't generalize and we have to repeat them for every subobject

[Antoine Chambert-Loir]

Thank you so much !

[Eric Wieser]

The discussion was https://github.com/leanprover-community/mathlib/pull/17086#issuecomment-1293833495