From 3c6f16c35fb0ea0fc127e369d08b324828a758ee Mon Sep 17 00:00:00 2001 From: Eric Rodriguez Date: Thu, 19 May 2022 19:16:15 +0000 Subject: [PATCH] feat(algebra/group/conj): instances + misc (#13943) Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com> --- src/algebra/group/conj.lean | 60 +++++++++++++++++++-- src/group_theory/commuting_probability.lean | 11 ++-- 2 files changed, 63 insertions(+), 8 deletions(-) diff --git a/src/algebra/group/conj.lean b/src/algebra/group/conj.lean index ba3037ca353b0..e96f4e7ab18d0 100644 --- a/src/algebra/group/conj.lean +++ b/src/algebra/group/conj.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2018 Patrick Massot. All rights reserved. +Copyright (c) 2018 Patrick Massot. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Patrick Massot, Chris Hughes, Michael Howes -/ @@ -31,6 +31,9 @@ def is_conj (a b : α) := ∃ c : αˣ, semiconj_by ↑c a b @[symm] lemma is_conj.symm {a b : α} : is_conj a b → is_conj b a | ⟨c, hc⟩ := ⟨c⁻¹, hc.units_inv_symm_left⟩ +lemma is_conj_comm {g h : α} : is_conj g h ↔ is_conj h g := +⟨is_conj.symm, is_conj.symm⟩ + @[trans] lemma is_conj.trans {a b c : α} : is_conj a b → is_conj b c → is_conj a c | ⟨c₁, hc₁⟩ ⟨c₂, hc₂⟩ := ⟨c₂ * c₁, hc₂.mul_left hc₁⟩ @@ -46,9 +49,11 @@ protected lemma monoid_hom.map_is_conj (f : α →* β) {a b : α} : is_conj a b end monoid section cancel_monoid + variables [cancel_monoid α] --- These lemmas hold for either `left_cancel_monoid` or `right_cancel_monoid`, --- with slightly different proofs; so far these don't seem necessary. +-- These lemmas hold for `right_cancel_monoid` with the current proofs, but for the sake of +-- not duplicating code (these lemmas also hold for `left_cancel_monoids`) we leave these +-- not generalised. @[simp] lemma is_conj_one_right {a : α} : is_conj 1 a ↔ a = 1 := ⟨λ ⟨c, hc⟩, mul_right_cancel (hc.symm.trans ((mul_one _).trans (one_mul _).symm)), λ h, by rw [h]⟩ @@ -172,6 +177,43 @@ instance [fintype α] [decidable_rel (is_conj : α → α → Prop)] : fintype (conj_classes α) := quotient.fintype (is_conj.setoid α) +/-- +Certain instances trigger further searches when they are considered as candidate instances; +these instances should be assigned a priority lower than the default of 1000 (for example, 900). + +The conditions for this rule are as follows: + * a class `C` has instances `instT : C T` and `instT' : C T'` + * types `T` and `T'` are both specializations of another type `S` + * the parameters supplied to `S` to produce `T` are not (fully) determined by `instT`, + instead they have to be found by instance search +If those conditions hold, the instance `instT` should be assigned lower priority. + +For example, suppose the search for an instance of `decidable_eq (multiset α)` tries the +candidate instance `con.quotient.decidable_eq (c : con M) : decidable_eq c.quotient`. +Since `multiset` and `con.quotient` are both quotient types, unification will check +that the relations `list.perm` and `c.to_setoid.r` unify. However, `c.to_setoid` depends on +a `has_mul M` instance, so this unification triggers a search for `has_mul (list α)`; +this will traverse all subclasses of `has_mul` before failing. +On the other hand, the search for an instance of `decidable_eq (con.quotient c)` for `c : con M` +can quickly reject the candidate instance `multiset.has_decidable_eq` because the type of +`list.perm : list ?m_1 → list ?m_1 → Prop` does not unify with `M → M → Prop`. +Therefore, we should assign `con.quotient.decidable_eq` a lower priority because it fails slowly. +(In terms of the rules above, `C := decidable_eq`, `T := con.quotient`, +`instT := con.quotient.decidable_eq`, `T' := multiset`, `instT' := multiset.has_decidable_eq`, +and `S := quot`.) + +If the type involved is a free variable (rather than an instantiation of some type `S`), +the instance priority should be even lower, see Note [lower instance priority]. +-/ +library_note "slow-failing instance priority" + +@[priority 900] -- see Note [slow-failing instance priority] +instance [decidable_rel (is_conj : α → α → Prop)] : decidable_eq (conj_classes α) := +quotient.decidable_eq + +instance [decidable_eq α] [fintype α] : decidable_rel (is_conj : α → α → Prop) := +λ a b, by { delta is_conj semiconj_by, apply_instance } + end monoid section comm_monoid @@ -215,6 +257,9 @@ lemma is_conj_iff_conjugates_of_eq {a b : α} : rwa ← h at ha, end⟩ +instance [fintype α] [decidable_rel (is_conj : α → α → Prop)] {a : α} : fintype (conjugates_of a) := +@subtype.fintype _ _ (‹decidable_rel is_conj› a) _ + end monoid namespace conj_classes @@ -243,4 +288,13 @@ lemma carrier_eq_preimage_mk {a : conj_classes α} : a.carrier = conj_classes.mk ⁻¹' {a} := set.ext (λ x, mem_carrier_iff_mk_eq) +section fintype + +variables [fintype α] [decidable_rel (is_conj : α → α → Prop)] + +instance {x : conj_classes α} : fintype (carrier x) := +quotient.rec_on_subsingleton x $ λ a, conjugates_of.fintype + +end fintype + end conj_classes diff --git a/src/group_theory/commuting_probability.lean b/src/group_theory/commuting_probability.lean index deda527d2a0b1..f9298ee2b22f7 100644 --- a/src/group_theory/commuting_probability.lean +++ b/src/group_theory/commuting_probability.lean @@ -56,9 +56,9 @@ end variables (G : Type*) [group G] [fintype G] -lemma card_comm_eq_card_conj_classes_mul_card : - card {p : G × G // p.1 * p.2 = p.2 * p.1} = card (conj_classes G) * card G := -calc card {p : G × G // p.1 * p.2 = p.2 * p.1} = card (Σ g, {h // g * h = h * g}) : +lemma card_comm_eq_card_conj_classes_mul_card [h : fintype (conj_classes G)] : + card {p : G × G // p.1 * p.2 = p.2 * p.1} = @card (conj_classes G) h * card G := +by convert calc card {p : G × G // p.1 * p.2 = p.2 * p.1} = card (Σ g, {h // g * h = h * g}) : card_congr (equiv.subtype_prod_equiv_sigma_subtype (λ g h : G, g * h = h * g)) ... = ∑ g, card {h // g * h = h * g} : card_sigma _ ... = ∑ g, card (mul_action.fixed_by (conj_act G) G g) : sum_equiv conj_act.to_conj_act.to_equiv @@ -97,8 +97,9 @@ begin conjugacy classes as `G ⧸ H`. -/ rw [comm_prob_def', comm_prob_def', div_le_iff, mul_assoc, ←nat.cast_mul, mul_comm (card H), ←subgroup.card_eq_card_quotient_mul_card_subgroup, div_mul_cancel, nat.cast_le], - { exact card_le_of_surjective (conj_classes.map (quotient_group.mk' H)) - (conj_classes.map_surjective quotient.surjective_quotient_mk') }, + { apply card_le_of_surjective, + show function.surjective (conj_classes.map (quotient_group.mk' H)), + exact (conj_classes.map_surjective quotient.surjective_quotient_mk') }, { exact nat.cast_ne_zero.mpr card_ne_zero }, { exact nat.cast_pos.mpr card_pos }, end