Fintype.card_subype rw problem

Stream: mathlib4

[Michael Stoll]

Recently I came across the following problem.

import Mathlib.GroupTheory.Perm.Cycle.Type

variable {F} [DecidableEq F] [Fintype F]

open Finset

def φ : F → F := sorry

def φ_end {s : Finset F} (hs : Set.BijOn φ s.toSet s.toSet) : Function.End s.toSet := fun
      | ⟨x, hx⟩ => ⟨φ x, hs.mapsTo hx⟩

lemma help₃ {s : Finset F} (hs : Set.BijOn φ s.toSet s.toSet) : (φ_end hs) ^ 3 = 1 := sorry

lemma help_fix {s : Finset F} (hs : Set.BijOn φ s.toSet s.toSet) :
    Function.fixedPoints (φ_end hs) = ∅ := sorry

lemma card_s {s : Finset F} (hs : Set.BijOn φ s.toSet s.toSet) :
    ∃ n, s.card = 3 * n := by
  have := Equiv.Perm.card_fixedPoints_modEq (p := 3) (n := 1) <| help₃ hs
  -- simplify right hand side of congruence to zero:
  simp only [coe_sort_coe, Fintype.card_subtype, help_fix hs, Fintype.card_of_isEmpty] at this
  -- now try to change left hand side to `s.card`
  rw [Fintype.card_subtype] at this
  -- tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  --   Fintype.card { x // ?p x }
  -- F: Type u_1
  -- inst✝: DecidableEq F
  -- s: Finset F
  -- hs: Set.BijOn φ ↑s ↑s
  -- this: Fintype.card { x // x ∈ s } ≡ 0 [MOD 3]
  --
  -- In `this`: @Fintype.card { x // x ∈ s } (FinsetCoe.fintype s) : ℕ
  -- Expected: @Fintype.card { x // ?p x } (Subtype.fintype fun x => ?p x) : ℕ
  sorry

Note that rewriting with Fintype.card_subtype works on the right hand side of the congruence.
I found a way around this, but I wanted to ask whether there is a recommended way of dealing with / avoiding this problem. I must admit I have no idea where the two different Fintype instances are coming from. I do realize that Fintype carries data (a Finset that contains all elements), which is probably the reason why the two do not get unified. On the other hand, #synth Subsingleton (Fintype F) does work, so I wonder why this is not resolved by subsingleton elemination?

[Eric Wieser]

card_subtype can't work here because F is not finite

[Michael Stoll]

Adding [Fintype F] does not change the problem (I guess I minimized too much). (Now added above.)

[Eric Wieser]

You're looking for docs#Fintype.card_coe (which doesn't mention univ). Fintype.card_subtype is for when working with a subtype of a finite type, which is not what you're doing.

[Kevin Buzzard]

convert will use subsingleton facts but not rw. We have Finite if you don't want to get bogged down with constructive stuff

[Michael Stoll]

docs#Equiv.Perm.card_fixedPoints_modEq needs Fintypes, however...

[Michael Stoll]

Eric Wieser said:

You're looking for docs#Fintype.card_coe (which doesn't mention univ). Fintype.card_subtype is for when working with a subtype of a finite type, which is not what you're doing.

Still, it is rather confusing that there are two different lemmas for "the same" thing. Could this be avoided?

[Kevin Buzzard]

Yeah but you'll be able to prove a noncomputable Finite version of this by using the Fintype version and then PR it and make everyone's lives better.

[Eric Wieser]

Michael Stoll said:

Eric Wieser said:

You're looking for docs#Fintype.card_coe (which doesn't mention univ). Fintype.card_subtype is for when working with a subtype of a finite type, which is not what you're doing.

Still, it is rather confusing that there are two different lemmas for "the same" thing. Could this be avoided?

They're not really the same thing though; the RHS is different

[Eric Wieser]

It's like how there are two lemmas with (x * y)\inv on the RHS, depending on whether you want to assume that the multiplication is commutative

[Michael Stoll]

The RHS of docs#Fintype.card_subtype simplifies when p = (· ∈ s)to the RHS of docs#Fintype.card_coe, though.
Anyway, in my use case, it looked like {x // f x = r}, and so docs#Fintype.card_coe does not apply.
Maybe I should un-M my MWE a bit...

[Eric Wieser]

The RHS of card_subtype is a type error without Fintype F though, because there is no univ. The same is not true of card_coe

[Michael Stoll]

Ah, I now realize that simp first simplified Fintype.card { x // x ∈ univ.filter (f · = r)} to Fintype.card { x // f x = r} and then got stuck. This seems to be another non-confluence problem with simp...
But anyway, it should be possible to get simp or rw to change Fintype.card { x // f x = r} to (univ.filter (f · = r)).card (assuming we have [Fintype F] around).

[Eric Wieser]

Can you make a mwe for that statement?

[Michael Stoll]

My impression is that the problem is caused by docs#Fintype.card_subtype using a specific Fintype instance, which is different from the one showing up on the LHS of docs#Equiv.Perm.card_fixedPoints_modEq . I guess I should look into how the latter comes about...

[Michael Stoll]

import Mathlib.GroupTheory.Perm.Cycle.Type

variable {F} [DecidableEq F] [Fintype F]

def φ : F → F := sorry

def φ_end {s : Finset F} (hs : Set.BijOn φ s.toSet s.toSet) : Function.End s.toSet := fun
      | ⟨x, hx⟩ => ⟨φ x, hs.mapsTo hx⟩

lemma help₃ {s : Finset F} (hs : Set.BijOn φ s.toSet s.toSet) : (φ_end hs) ^ 3 = 1 := sorry

lemma card_fix {s : Finset F} (hs : Set.BijOn φ s.toSet s.toSet) :
    s.card ≡  0 [MOD 3] := by
  have H₁ := @Equiv.Perm.card_fixedPoints_modEq _ (Subtype.fintype ..) _ _ 3 1 _ <| help₃ hs
  have H₂ := Equiv.Perm.card_fixedPoints_modEq (p := 3) (n := 1) <| help₃ hs
  simp only [Fintype.card_subtype] at H₁
  -- (filter (fun x => x ∈ ↑s) univ).card ≡ Fintype.card ↑(Function.fixedPoints (φ_end hs)) [MOD 3]
  simp only [Fintype.card_subtype] at H₂
  -- Fintype.card ↑↑s ≡ (filter (fun x => x ∈ Function.fixedPoints (φ_end hs)) univ).card [MOD 3]
  sorry

It is a bit strange that Fintype.card_subtype works either on the left or on the right, depending on which Fintype instance docs#Equiv.Perm.card_fixedPoints_modEq uses, but not on both.

[Michael Stoll]

A variant:

import Mathlib.GroupTheory.Perm.Cycle.Type

variable {F} [DecidableEq F] [Fintype F]

def φ : F → F := sorry

def φ_end {s : Finset F} (hs : Set.BijOn φ s.toSet s.toSet) : Function.End s.toSet := fun
      | ⟨x, hx⟩ => ⟨φ x, hs.mapsTo hx⟩

lemma help₃ {s : Finset F} (hs : Set.BijOn φ s.toSet s.toSet) : (φ_end hs) ^ 3 = 1 := sorry

lemma card_fix {s : Finset F} (hs : Set.BijOn φ s.toSet s.toSet) :
    s.card ≡  0 [MOD 3] := by
  have H₁ := @Equiv.Perm.card_fixedPoints_modEq _ (Subtype.fintype ..) _ _ 3 1 _ <| help₃ hs
  have H₂ := Equiv.Perm.card_fixedPoints_modEq (p := 3) (n := 1) <| help₃ hs
  simp? [Fintype.card_subtype] at H₁
       says simp only [Finset.mem_coe, Finset.coe_sort_coe, Fintype.card_subtype,
      Finset.filter_congr_decidable, Finset.filter_univ_mem, Fintype.card_ofFinset,
      Function.mem_fixedPoints] at H₁
  -- s.card ≡ (Finset.filter (fun x => Function.IsFixedPt (φ_end hs) x) Finset.univ).card [MOD 3]
  simp? [Fintype.card_subtype] at H₂
       says simp only [Finset.coe_sort_coe, Fintype.card_coe, Fintype.card_subtype,
      Function.mem_fixedPoints, Finset.univ_eq_attach] at H₂
  -- s.card ≡ (Finset.filter (fun x => Function.IsFixedPt (φ_end hs) x) (Finset.attach s)).card [MOD 3]
  sorry

We end up at slightly different statements.

[Yaël Dillies]

Michael Stoll said:

My impression is that the problem is caused by docs#Fintype.card_subtype using a specific Fintype instance

This is indeed a problem. That means Fintype.card_subtype is misstated. It should take a [Fintype {x // p x}] argument.

[Kevin Buzzard]

Michael Stoll said:

docs#Equiv.Perm.card_fixedPoints_modEq needs Fintypes, however...

So because I think Fintype is evil (precisely because of all the pain you're going through above) I just thought I'd mention explicitly how to avoid all this:

import Mathlib

noncomputable def Equiv.Perm.cycleType' {α : Type*} [Finite α] (f : Equiv.Perm α) : Multiset ℕ := by
  classical
    letI : Fintype α := Fintype.ofFinite α
    exact Equiv.Perm.cycleType f

noncomputable def Equiv.Perm.cycleFactorsFinset' {α : Type*} [Finite α] (f : Equiv.Perm α) :
    Finset (Equiv.Perm α) := by
  classical
    letI : Fintype α := Fintype.ofFinite α
    exact Equiv.Perm.cycleFactorsFinset f

theorem Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub' {α : Type*} [Finite α]
    {f g : Equiv.Perm α} (hf : f ∈ Equiv.Perm.cycleFactorsFinset' g) :
    Equiv.Perm.cycleType' (g * f⁻¹) = Equiv.Perm.cycleType' g - Equiv.Perm.cycleType' f := by
  classical
    letI : Fintype α := Fintype.ofFinite α
    exact Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub hf

You use the primed version of everything and all your problems disappear.

[Kevin Buzzard]

In fact I guess all this could be done by some [to_Finite] attribute.

[Eric Wieser]

Yaël Dillies said:

This is indeed a problem. That means Fintype.card_subtype is misstated. It should take a [Fintype {x // p x}] argument.

In particular, there is an instance diamond here between "sets that are finite because their elements belong to a finite type" and "set that are finite because their elements satisfy a finite predicate". I don't think "use the most general Fintype argument possible" is a good idea in general, because it makes the library weird; but in cases where a diamond like this is present, it's the right choice.

[Michael Stoll]

The statement I really want is

lemma card_fixedPoints_modEq {α} [Fintype α] [DecidableEq α] {s : Finset α} {f : α → α}
    (hf : Set.MapsTo f s.toSet s.toSet) {p : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)]
    (h : Set.EqOn f^[p ^ n] id s) :
    s.card ≡ (s.filter fun a ↦ f a = a).card [MOD p] := by sorry

or something along these lines.

While trying to put together a proof of that, I found that there is not much API to speak of for Function.End. Why is that?

Anyway, my attempt currently looks like this.

import Mathlib.GroupTheory.Perm.Cycle.Type

@[ext]
lemma Function.End.ext {α} {f g : Function.End α} (h : ∀ a, f a = g a) : f = g := funext h

def Function.End.of_mapsTo {α} {s : Set α} {f : α → α} (h : Set.MapsTo f s s) :
    Function.End s := fun ⟨a, ha⟩ ↦ ⟨f a, h ha⟩

lemma Function.End.of_mapsTo_id {α} {s : Set α} : of_mapsTo (Set.mapsTo_id s) = 1 := rfl

@[simp]
lemma Function.End.of_mapsTo_apply {α} {s : Set α} {f : α → α} (h : Set.MapsTo f s s) {a : α}
    (ha : a ∈ s) :
    of_mapsTo h ⟨a, ha⟩ = ⟨f a, h ha⟩  := rfl

@[simp]
lemma Function.End.of_mapsTo_apply_val {α} {s : Set α} {f : α → α} (h : Set.MapsTo f s s) {a : α}
    (ha : a ∈ s) :
    (of_mapsTo h ⟨a, ha⟩).val = f a := rfl

@[simp]
lemma Function.End.of_mapsTo_apply' {α} {s : Set α} {f : α → α} (h : Set.MapsTo f s s) (a : s) :
    of_mapsTo h a = ⟨f a.val, h a.prop⟩ := rfl

@[simp]
lemma Function.End.of_mapsTo_apply'_val {α} {s : Set α} {f : α → α} (h : Set.MapsTo f s s) (a : s) :
    (of_mapsTo h a).val = f a.val := rfl

lemma Function.End.eq_of_eqOn {α} {s : Set α} {f g : α → α} (h : Set.EqOn f g s)
    (hf : Set.MapsTo f s s) (hg : Set.MapsTo g s s) :
    of_mapsTo hf = of_mapsTo hg := by
  ext a
  simp_rw [of_mapsTo_apply']
  exact h a.prop

lemma Function.End.iterate {α} (f : Function.End α) (n : ℕ) : (f ^ n : α → α) = f^[n] := by
  induction' n with n ih
  · simp only [Nat.zero_eq, pow_zero, one_def, iterate_zero]
  · rw [pow_succ, Function.iterate_succ', ih, mul_def]

lemma Function.End.of_mapsTo_comp {α} {s : Set α} {f g : α → α} (hf : Set.MapsTo f s s)
    (hg : Set.MapsTo g s s) :
    (of_mapsTo hf) * (of_mapsTo hg) = of_mapsTo (Set.MapsTo.comp hf hg) := rfl

lemma Function.End.of_mapsTo_pow {α} {s : Set α} {f : α → α} (h : Set.MapsTo f s s) (n : ℕ) :
    (of_mapsTo h) ^ n = of_mapsTo (Set.MapsTo.iterate h n) := by
  rw [iterate]
  induction' n with n hn
  · simp only [Nat.zero_eq, iterate_zero]
    ext a
    simp only [id_eq, of_mapsTo_apply']
  · ext a
    simp only [iterate_succ, hn, comp_apply, of_mapsTo_apply']

open Function.End in
lemma card_fixedPoints_modEq {α} [Fintype α] [DecidableEq α] {s : Finset α} {f : α → α}
    (hf : Set.MapsTo f s.toSet s.toSet) {p : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)]
    (h : Set.EqOn f^[p ^ n] id s) :
    s.card ≡ (s.filter fun a ↦ f a = a).card [MOD p] := by
  let F := of_mapsTo hf
  have hF : F ^ (p ^ n) = 1
  · rw [of_mapsTo_pow, ← of_mapsTo_id]
    exact eq_of_eqOn h ..
  have H := Equiv.Perm.card_fixedPoints_modEq hF
  simp? [Fintype.card_subtype, Function.IsFixedPt] at H
       says simp only [Finset.coe_sort_coe, Fintype.card_coe, Fintype.card_subtype,
      Function.mem_fixedPoints, Function.IsFixedPt, Finset.univ_eq_attach] at H
  convert H
  rw [eq_comm]
  refine Finset.card_congr (fun (x : { x // x ∈ s }) _ ↦ x.val) (fun a ha ↦ ?_)
    (fun _ _ _ _ ↦ SetCoe.ext) (fun b hb ↦ ?_)
  · simpa only [Finset.mem_filter, Finset.mem_attach, Finset.coe_mem, Subtype.ext_iff, true_and]
      using ha
  · refine ⟨⟨b, Finset.mem_of_mem_filter b hb⟩, ?_, rfl⟩
    simp only [Finset.mem_filter] at hb
    simpa only [of_mapsTo_apply', Finset.filter_congr_decidable, Finset.mem_filter,
      Finset.mem_attach, Subtype.mk.injEq, true_and] using hb.2

I think it would make sense to have something like card_fixedPoints_modEq in Mathlib, to save the user from having to go through the Function.End clunkiness.

[Eric Wieser]

Michael Stoll said:

While trying to put together a proof of that, I found that there is not much API to speak of for Function.End. Why is that?

I proposed we add Function.End in !3#8253, where we really only needed a small bit of API around MulAction; I agree that it could probably do with some more thought around the API

[Michael Stoll]

I guess I'm really asking why docs#Equiv.Perm.card_fixedPoints_modEq is formulated in terms of Function.End (it's not even in the right namespace for that!).

[Eric Wieser]

I think that's a question for git blame :)

[Michael Stoll]

Eric Wieser said:

I think that's a question for git blame :)

git blame can tell me who wrote it, but not why...

[Michael Stoll]

I have now produced a variant of docs#Equiv.Perm.card_fixedPoints_modEq that talks about functions leaving a Finset invariant. It looks like this:

import Mathlib.GroupTheory.Perm.Cycle.Type

-- A version of `Equiv.Perm.card_fixedPoints_modEq` for sub-`Finset`s and a function `f : α → α`.

namespace Finset

/-- If a function `f` maps a `Finset` into itself, all its iterates do so as well. -/
lemma iterate_mem {α} {s : Finset α} {f : α → α}
    (hf : ∀ a ∈ s, f a ∈ s) (n : ℕ) {a : α} (ha : a ∈ s) : f^[n] a ∈ s := by
  induction' n with n ih
  · simp [ha]
  · simp only [Function.iterate_succ', Function.comp_apply, ih, hf]

open Function Equiv in
/-- We can turn a function `f` that maps a `Finset` `s` into itself and has order dividing `n`
when restricted to `s` into an equivalence of `s` considered as a type. -/
def equivOfFiniteOrderOn {α} {s : Finset α} {f : α → α} (hf : ∀ a ∈ s, f a ∈ s) {n : ℕ}
    (hn : 1 ≤ n) (h : ∀ a ∈ s, f^[n] a = a) : Equiv s s := by
  refine ⟨fun ⟨a, ha⟩ ↦ ⟨f a, hf a ha⟩, fun ⟨a, ha⟩ ↦ ⟨f^[n - 1] a, iterate_mem hf _ ha⟩,
     leftInverse_iff_comp.mpr ?_, leftInverse_iff_comp.mpr ?_⟩ <;>
  { ext a
    simpa only [comp_apply, id_eq, ← iterate_succ_apply, ← iterate_succ_apply' (f := f),
      ← Nat.succ_sub hn, Nat.succ_sub_one] using h a.val a.prop }

@[simp]
lemma equivOf_apply {α} {s : Finset α} {f : α → α} (hf : ∀ a ∈ s, f a ∈ s) {n : ℕ}
    (hn : 1 ≤ n) (h : ∀ a ∈ s, f^[n] a = a) (a : {x // x ∈ s}) :
    equivOfFiniteOrderOn hf hn h a = ⟨f a.val, hf a.val a.prop⟩ := rfl

open Function Equiv in
/-- The `m`th power of an equivalence on `s` obtained by restricting a function `f`
can be obtained by restricting the `m`th iterate of `f`. -/
lemma equivOf_pow_eq_iterate {α} {s : Finset α} {f : α → α} (hf : ∀ a ∈ s, f a ∈ s) {n : ℕ}
    (hn : 1 ≤ n) (h : ∀ a ∈ s, f^[n] a = a) (m : ℕ) (a : {x // x ∈ s}) :
    ((equivOfFiniteOrderOn hf hn h) ^ m) a = ⟨f^[m] a, iterate_mem hf m a.prop⟩ := by
  induction' m with m ih
  · simp only [Nat.zero_eq, pow_zero, Perm.coe_one, id_eq, iterate_zero, Subtype.coe_eta]
  · rw [pow_succ, Perm.coe_mul, comp_apply, equivOf_apply, Subtype.mk.injEq, ih,
      iterate_succ_apply']

open Function Equiv in
/-- If `f` has order dividing `n` and maps a `Finset` `s` into itself, then the equivalence
on `s` obtained by restricting `f` also has order dividing `n`. -/
lemma equivOf_order {α} {s : Finset α} {f : α → α} (hf : ∀ a ∈ s, f a ∈ s) {n : ℕ}
    (hn : 1 ≤ n) (h : ∀ a ∈ s, f^[n] a = a) :
    (equivOfFiniteOrderOn hf hn h) ^ n = 1 := by
  ext a
  simpa only [equivOf_pow_eq_iterate, coe_one, id_eq] using h a.val a.prop

open Function Equiv Perm in
/-- If `f : α → α` maps a `Finset` `s` to itself and its `p^n`th iterate is the identity on `s`,
where `p` is a prime number, then the cardinality of `s` is congruent mod `p` to the number of
fixed points of `f` on `s` . -/
lemma card_fixedPoints_modEq {α} [Fintype α] [DecidableEq α] {s : Finset α} {f : α → α}
    (hf : ∀ a ∈ s, f a ∈ s) {p n : ℕ} [hp : Fact p.Prime] (h : ∀ a ∈ s, f^[p ^ n] a = a) :
    s.card ≡ (s.filter fun a ↦ f a = a).card [MOD p] := by
  have hpn : 1 ≤ p ^ n := n.one_le_pow p hp.out.one_lt.le
  suffices : (s.filter fun a ↦ f a = a).card = (support <| equivOfFiniteOrderOn hf hpn h)ᶜ.card
  · convert Fintype.card_coe s ▸ (card_compl_support_modEq <| equivOf_order hf hpn h).symm
  refine (card_congr (fun (x : { x // x ∈ s }) _ ↦ x.val) (fun a ha ↦ ?_)
    (fun _ _ _ _ ↦ SetCoe.ext) (fun _ hb ↦ ?_)).symm
  · simp only [mem_compl, Perm.mem_support, coe_fn_mk, ne_eq, not_not, mem_filter, coe_mem,
      true_and] at ha ⊢
    exact congr_arg Subtype.val ha
  · simpa only [mem_filter, mem_compl, Perm.mem_support, equivOf_apply, ne_eq, not_not,
      exists_prop, Subtype.exists, Subtype.mk.injEq, exists_and_left, exists_eq_right_right]
      using hb

/-- If `f : α → α` maps a `Finset` `s` to itself and its `p`th iterate is the identity on `s`,
where `p` is a prime number, then the cardinality of `s` is congruent mod `p` to the number of
fixed points of `f` on `s` . -/
lemma card_fixedPoints_modEq_prime {α} [Fintype α] [DecidableEq α] {s : Finset α} {f : α → α}
    (hf : ∀ a ∈ s, f a ∈ s) {p : ℕ} [Fact p.Prime] (h : ∀ a ∈ s, f^[p] a = a) :
    s.card ≡ (s.filter fun a ↦ f a = a).card [MOD p] :=
  card_fixedPoints_modEq hf <| (pow_one p).symm ▸ h

end Finset

Would this be welcome as a PR?

[Michael Stoll]

:up: @Yaël Dillies @Eric Wieser

[Yaël Dillies]

Your equivOfFiniteOrderOn is very close to docs#Equiv.Perm.subtypePerm

[Yaël Dillies]

Also this has nothing to do with this topic anymore, right?

[Michael Stoll]

Yaël Dillies said:

Your equivOfFiniteOrderOn is very close to docs#Equiv.Perm.subtypePerm

Not really: I do not want to assume that f is a permutation on α, only that it induces one on a (finite) subset.

[Michael Stoll]

Yaël Dillies said:

Also this has nothing to do with this topic anymore, right?

It simplifies the application that originally led to the problem I encountered, which prompted this thread. But strictly speaking, you are right.

[Yaël Dillies]

... which is why I said "very close to", not "special case of"

[Michael Stoll]

One could dispute the "very" :smile:
But what did you want to imply with this statement? I'm trying to decide whether it makes sense to submit a PR, and I can't tell whether to take this as en- or discouragement.

[Yaël Dillies]

I don't know. It was a remark that I hoped would spark you to find a common abstraction, but I'm not sure there is one. At least, it should prompt you to harmonize the names.

[Antoine Chambert-Loir]

Regarding the initial question, I think that for the same reason I switched from docs#Fintype.card to #Nat.card in a proof, to be able to apply ‘congr‘ or something like that. — in branch#ACL/ConjClassCount