Skip to content

Commit 2414ba0

Browse files
committed
chore(GroupTheory/Perm): drop DecidableEq, Fintype -> Finite (#10917)
1 parent 3c1a814 commit 2414ba0

File tree

2 files changed

+34
-42
lines changed

2 files changed

+34
-42
lines changed

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

Lines changed: 21 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1218,12 +1218,10 @@ end CycleOf
12181218
### `cycleFactors`
12191219
-/
12201220

1221-
variable [DecidableEq α]
1222-
12231221
open scoped List in
12241222
/-- Given a list `l : List α` and a permutation `f : perm α` whose nonfixed points are all in `l`,
12251223
recursively factors `f` into cycles. -/
1226-
def cycleFactorsAux [Fintype α] :
1224+
def cycleFactorsAux [DecidableEq α] [Fintype α] :
12271225
∀ (l : List α) (f : Perm α),
12281226
(∀ {x}, f x ≠ x → x ∈ l) →
12291227
{ l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } := by
@@ -1325,15 +1323,15 @@ def cycleFactors [Fintype α] [LinearOrder α] (f : Perm α) :
13251323

13261324
/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`,
13271325
without a linear order. -/
1328-
def truncCycleFactors [Fintype α] (f : Perm α) :
1326+
def truncCycleFactors [DecidableEq α] [Fintype α] (f : Perm α) :
13291327
Trunc { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
13301328
Quotient.recOnSubsingleton (@univ α _).1 (fun l h => Trunc.mk (cycleFactorsAux l f (h _)))
13311329
(show ∀ x, f x ≠ x → x ∈ (@univ α _).1 from fun _ _ => mem_univ _)
13321330
#align equiv.perm.trunc_cycle_factors Equiv.Perm.truncCycleFactors
13331331

13341332
section CycleFactorsFinset
13351333

1336-
variable [Fintype α] (f : Perm α)
1334+
variable [DecidableEq α] [Fintype α] (f : Perm α)
13371335

13381336
/-- Factors a permutation `f` into a `Finset` of disjoint cyclic permutations that multiply to `f`.
13391337
-/
@@ -1547,7 +1545,7 @@ theorem cycle_induction_on [Finite β] (P : Perm β → Prop) (σ : Perm β) (ba
15471545
(ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)
15481546
#align equiv.perm.cycle_induction_on Equiv.Perm.cycle_induction_on
15491547

1550-
theorem cycleFactorsFinset_mul_inv_mem_eq_sdiff [Fintype α] {f g : Perm α}
1548+
theorem cycleFactorsFinset_mul_inv_mem_eq_sdiff [DecidableEq α] [Fintype α] {f g : Perm α}
15511549
(h : f ∈ cycleFactorsFinset g) : cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f} := by
15521550
revert f
15531551
refine'
@@ -1607,7 +1605,7 @@ theorem closure_isCycle : closure { σ : Perm β | IsCycle σ } = ⊤ := by
16071605
top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))
16081606
#align equiv.perm.closure_is_cycle Equiv.Perm.closure_isCycle
16091607

1610-
variable [Fintype α]
1608+
variable [DecidableEq α] [Fintype α]
16111609

16121610
theorem closure_cycle_adjacent_swap {σ : Perm α} (h1 : IsCycle σ) (h2 : σ.support = ⊤) (x : α) :
16131611
closure ({σ, swap x (σ x)} : Set (Perm α)) = ⊤ := by
@@ -1692,15 +1690,14 @@ end Generation
16921690

16931691
section
16941692

1695-
variable [Fintype α] {σ τ : Perm α}
1696-
16971693
noncomputable section
16981694

1695+
variable [DecidableEq α] [Fintype α] {σ τ : Perm α}
1696+
16991697
theorem isConj_of_support_equiv
17001698
(f : { x // x ∈ (σ.support : Set α) } ≃ { x // x ∈ (τ.support : Set α) })
1701-
(hf :
1702-
∀ (x : α) (hx : x ∈ (σ.support : Set α)),
1703-
(f ⟨σ x, apply_mem_support.2 hx⟩ : α) = τ ↑(f ⟨x, hx⟩)) :
1699+
(hf : ∀ (x : α) (hx : x ∈ (σ.support : Set α)),
1700+
(f ⟨σ x, apply_mem_support.2 hx⟩ : α) = τ ↑(f ⟨x, hx⟩)) :
17041701
IsConj σ τ := by
17051702
refine' isConj_iff.2 ⟨Equiv.extendSubtype f, _⟩
17061703
rw [mul_inv_eq_iff_eq_mul]
@@ -1762,7 +1759,7 @@ theorem card_support_conj : (σ * τ * σ⁻¹).support.card = τ.support.card :
17621759

17631760
end
17641761

1765-
theorem Disjoint.isConj_mul {α : Type*} [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π)
1762+
theorem Disjoint.isConj_mul [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π)
17661763
(hc2 : IsConj τ ρ) (hd1 : Disjoint σ τ) (hd2 : Disjoint π ρ) : IsConj (σ * τ) (π * ρ) := by
17671764
classical
17681765
cases nonempty_fintype α
@@ -1816,7 +1813,7 @@ section FixedPoints
18161813
-/
18171814

18181815

1819-
theorem fixed_point_card_lt_of_ne_one [Fintype α] {σ : Perm α} (h : σ ≠ 1) :
1816+
theorem fixed_point_card_lt_of_ne_one [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ ≠ 1) :
18201817
(filter (fun x => σ x = x) univ).card < Fintype.card α - 1 := by
18211818
rw [lt_tsub_iff_left, ← lt_tsub_iff_right, ← Finset.card_compl, Finset.compl_filter]
18221819
exact one_lt_card_support_of_ne_one h
@@ -1866,9 +1863,8 @@ variable [DecidableEq α] [Fintype α]
18661863

18671864
theorem _root_.Finset.exists_cycleOn (s : Finset α) :
18681865
∃ f : Perm α, f.IsCycleOn s ∧ f.support ⊆ s := by
1869-
refine'
1870-
⟨s.toList.formPerm, _, fun x hx => by
1871-
simpa using List.mem_of_formPerm_apply_ne _ _ (Perm.mem_support.1 hx)⟩
1866+
refine ⟨s.toList.formPerm, ?_, fun x hx => by
1867+
simpa using List.mem_of_formPerm_apply_ne _ _ (Perm.mem_support.1 hx)⟩
18721868
convert s.nodup_toList.isCycleOn_formPerm
18731869
simp
18741870
#align finset.exists_cycle_on Finset.exists_cycleOn
@@ -1882,18 +1878,16 @@ variable {f : Perm α} {s : Set α}
18821878
theorem _root_.Set.Countable.exists_cycleOn (hs : s.Countable) :
18831879
∃ f : Perm α, f.IsCycleOn s ∧ { x | f x ≠ x } ⊆ s := by
18841880
classical
1885-
obtain hs' | hs' := s.finite_or_infinite
1886-
· refine'
1887-
⟨hs'.toFinset.toList.formPerm, _, fun x hx => by
1888-
simpa using List.mem_of_formPerm_apply_ne _ _ hx⟩
1889-
convert hs'.toFinset.nodup_toList.isCycleOn_formPerm
1890-
simp
1891-
haveI := hs.to_subtype
1881+
obtain hs' | hs' := s.finite_or_infinite
1882+
· refine ⟨hs'.toFinset.toList.formPerm, ?_, fun x hx => by
1883+
simpa using List.mem_of_formPerm_apply_ne _ _ hx⟩
1884+
convert hs'.toFinset.nodup_toList.isCycleOn_formPerm
1885+
simp
1886+
· haveI := hs.to_subtype
18921887
haveI := hs'.to_subtype
18931888
obtain ⟨f⟩ : Nonempty (ℤ ≃ s) := inferInstance
1894-
refine'
1895-
⟨(Equiv.addRight 1).extendDomain f, _, fun x hx =>
1896-
of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
1889+
refine ⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
1890+
of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
18971891
convert Int.addRight_one_isCycle.isCycleOn.extendDomain f
18981892
rw [Set.image_comp, Equiv.image_eq_preimage]
18991893
ext

Mathlib/GroupTheory/Perm/Sign.lean

Lines changed: 13 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -322,8 +322,6 @@ def signBijAux {n : ℕ} (f : Perm (Fin n)) (a : Σ_ : Fin n, Fin n) : Σ_ : Fin
322322
if _ : f a.2 < f a.1 then ⟨f a.1, f a.2else ⟨f a.2, f a.1
323323
#align equiv.perm.sign_bij_aux Equiv.Perm.signBijAux
324324

325-
-- porting note: Lean insists `ha` and `hb` are unused despite obvious uses
326-
set_option linter.unusedVariables false in
327325
theorem signBijAux_injOn {n : ℕ} {f : Perm (Fin n)} :
328326
(finPairsLT n : Set (Σ _, Fin n)).InjOn (signBijAux f) := by
329327
rintro ⟨a₁, a₂⟩ ha ⟨b₁, b₂⟩ hb h
@@ -526,6 +524,19 @@ theorem signAux3_mul_and_swap [Finite α] (f g : Perm α) (s : Multiset α) (hs
526524
rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hexy]
527525
#align equiv.perm.sign_aux3_mul_and_swap Equiv.Perm.signAux3_mul_and_swap
528526

527+
theorem signAux3_symm_trans_trans [Finite α] [DecidableEq β] [Finite β] (f : Perm α) (e : α ≃ β)
528+
{s : Multiset α} {t : Multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) :
529+
signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs := by
530+
-- porting note: switched from term mode to tactic mode
531+
induction' t, s using Quotient.inductionOn₂ with t s ht hs
532+
show signAux2 _ _ = signAux2 _ _
533+
rcases Finite.exists_equiv_fin β with ⟨n, ⟨e'⟩⟩
534+
rw [← signAux_eq_signAux2 _ _ e' fun _ _ => ht _,
535+
← signAux_eq_signAux2 _ _ (e.trans e') fun _ _ => hs _]
536+
exact congr_arg signAux
537+
(Equiv.ext fun x => by simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply])
538+
#align equiv.perm.sign_aux3_symm_trans_trans Equiv.Perm.signAux3_symm_trans_trans
539+
529540
/-- `SignType.sign` of a permutation returns the signature or parity of a permutation, `1` for even
530541
permutations, `-1` for odd permutations. It is the unique surjective group homomorphism from
531542
`Perm α` to the group with two elements.-/
@@ -581,19 +592,6 @@ theorem IsSwap.sign_eq {f : Perm α} (h : f.IsSwap) : sign f = -1 :=
581592
hxy.2.symm ▸ sign_swap hxy.1
582593
#align equiv.perm.is_swap.sign_eq Equiv.Perm.IsSwap.sign_eq
583594

584-
theorem signAux3_symm_trans_trans [DecidableEq β] [Fintype β] (f : Perm α) (e : α ≃ β)
585-
{s : Multiset α} {t : Multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) :
586-
signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs := by
587-
-- porting note: switched from term mode to tactic mode
588-
induction' t, s using Quotient.inductionOn₂ with t s ht hs
589-
show signAux2 _ _ = signAux2 _ _
590-
let n := equivFin β
591-
rw [← signAux_eq_signAux2 _ _ n fun _ _ => ht _,
592-
← signAux_eq_signAux2 _ _ (e.trans n) fun _ _ => hs _]
593-
exact congr_arg signAux
594-
(Equiv.ext fun x => by simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply])
595-
#align equiv.perm.sign_aux3_symm_trans_trans Equiv.Perm.signAux3_symm_trans_trans
596-
597595
@[simp]
598596
theorem sign_symm_trans_trans [DecidableEq β] [Fintype β] (f : Perm α) (e : α ≃ β) :
599597
sign ((e.symm.trans f).trans e) = sign f :=

0 commit comments

Comments
 (0)