From 3527e4ad96d4424170c863419706c438792e5f90 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 19 Jul 2022 09:10:17 +0000 Subject: [PATCH] refactor(group_theory/group_action/basic): Make `mul_action.self_equiv_sigma_orbits` computable (#14591) This introduces a new `mul_action.orbit_rel.quotient.orbit` definition to avoid the need for `.out`. --- src/group_theory/group_action/basic.lean | 64 ++++++++++++++++----- src/group_theory/group_action/quotient.lean | 6 +- 2 files changed, 54 insertions(+), 16 deletions(-) diff --git a/src/group_theory/group_action/basic.lean b/src/group_theory/group_action/basic.lean index e264febc6ba9c..5948759be8e00 100644 --- a/src/group_theory/group_action/basic.lean +++ b/src/group_theory/group_action/basic.lean @@ -226,30 +226,66 @@ lemma image_inter_image_iff (U V : set β) : (quotient.mk '' U) ∩ (quotient.mk '' V) = ∅ ↔ ∀ x ∈ U, ∀ a : α, a • x ∉ V := set.disjoint_iff_inter_eq_empty.symm.trans disjoint_image_image_iff +variables (α β) + +/-- The quotient by `mul_action.orbit_rel`, given a name to enable dot notation. -/ +@[reducible, to_additive "The quotient by `add_action.orbit_rel`, given a name to enable dot +notation."] +def orbit_rel.quotient : Type* := quotient $ orbit_rel α β + +variables {α β} + +/-- The orbit corresponding to an element of the quotient by `mul_action.orbit_rel` -/ +@[to_additive "The orbit corresponding to an element of the quotient by `add_action.orbit_rel`"] +def orbit_rel.quotient.orbit (x : orbit_rel.quotient α β) : set β := +quotient.lift_on' x (orbit α) $ λ _ _, mul_action.orbit_eq_iff.2 + +@[simp, to_additive] +lemma orbit_rel.quotient.orbit_mk (b : β) : + orbit_rel.quotient.orbit (quotient.mk' b : orbit_rel.quotient α β) = orbit α b := rfl + +@[to_additive] +lemma orbit_rel.quotient.mem_orbit {b : β} {x : orbit_rel.quotient α β} : + b ∈ x.orbit ↔ quotient.mk' b = x := +by { induction x using quotient.induction_on', rw quotient.eq', refl } + +/-- Note that `hφ = quotient.out_eq'` is a useful choice here. -/ +@[to_additive "Note that `hφ = quotient.out_eq'` is a useful choice here."] +lemma orbit_rel.quotient.orbit_eq_orbit_out (x : orbit_rel.quotient α β) + {φ : orbit_rel.quotient α β → β} (hφ : right_inverse φ quotient.mk') : + orbit_rel.quotient.orbit x = orbit α (φ x) := +begin + conv_lhs { rw ←hφ x }, + induction x using quotient.induction_on', + refl, +end + variables (α) (β) -local notation `Ω` := (quotient $ orbit_rel α β) + +local notation `Ω` := orbit_rel.quotient α β /-- Decomposition of a type `X` as a disjoint union of its orbits under a group action. -This version works with any right inverse to `quotient.mk'` in order to stay computable. In most -cases you'll want to use `quotient.out'`, so we provide `mul_action.self_equiv_sigma_orbits` as -a special case. -/ + +This version is expressed in terms of `mul_action.orbit_rel.quotient.orbit` instead of +`mul_action.orbit`, to avoid mentioning `quotient.out'`. -/ @[to_additive "Decomposition of a type `X` as a disjoint union of its orbits under an additive group -action. This version works with any right inverse to `quotient.mk'` in order to stay computable. -In most cases you'll want to use `quotient.out'`, so we provide `add_action.self_equiv_sigma_orbits` -as a special case."] -def self_equiv_sigma_orbits' {φ : Ω → β} (hφ : right_inverse φ quotient.mk') : - β ≃ Σ (ω : Ω), orbit α (φ ω) := +action. + +This version is expressed in terms of `add_action.orbit_rel.quotient.orbit` instead of +`add_action.orbit`, to avoid mentioning `quotient.out'`. "] +def self_equiv_sigma_orbits' : β ≃ Σ ω : Ω, ω.orbit := calc β ≃ Σ (ω : Ω), {b // quotient.mk' b = ω} : (equiv.sigma_fiber_equiv quotient.mk').symm -... ≃ Σ (ω : Ω), orbit α (φ ω) : - equiv.sigma_congr_right (λ ω, equiv.subtype_equiv_right $ - λ x, by {rw [← hφ ω, quotient.eq', hφ ω], refl }) +... ≃ Σ (ω : Ω), ω.orbit : + equiv.sigma_congr_right $ λ ω, equiv.subtype_equiv_right $ λ x, + orbit_rel.quotient.mem_orbit.symm /-- Decomposition of a type `X` as a disjoint union of its orbits under a group action. -/ @[to_additive "Decomposition of a type `X` as a disjoint union of its orbits under an additive group action."] -noncomputable def self_equiv_sigma_orbits : β ≃ Σ (ω : Ω), orbit α ω.out' := -self_equiv_sigma_orbits' α β quotient.out_eq' +def self_equiv_sigma_orbits : β ≃ Σ (ω : Ω), orbit α ω.out' := +(self_equiv_sigma_orbits' α β).trans $ equiv.sigma_congr_right $ λ i, + equiv.set.of_eq $ orbit_rel.quotient.orbit_eq_orbit_out _ quotient.out_eq' variables {α β} diff --git a/src/group_theory/group_action/quotient.lean b/src/group_theory/group_action/quotient.lean index b0e68712cc1c3..838ae21358d95 100644 --- a/src/group_theory/group_action/quotient.lean +++ b/src/group_theory/group_action/quotient.lean @@ -167,9 +167,11 @@ as a special case. "] noncomputable def self_equiv_sigma_orbits_quotient_stabilizer' {φ : Ω → β} (hφ : left_inverse quotient.mk' φ) : β ≃ Σ (ω : Ω), α ⧸ (stabilizer α (φ ω)) := calc β - ≃ Σ (ω : Ω), orbit α (φ ω) : self_equiv_sigma_orbits' α β hφ + ≃ Σ (ω : Ω), orbit_rel.quotient.orbit ω : self_equiv_sigma_orbits' α β ... ≃ Σ (ω : Ω), α ⧸ (stabilizer α (φ ω)) : - equiv.sigma_congr_right (λ ω, orbit_equiv_quotient_stabilizer α (φ ω)) + equiv.sigma_congr_right (λ ω, + (equiv.set.of_eq $ orbit_rel.quotient.orbit_eq_orbit_out _ hφ).trans $ + orbit_equiv_quotient_stabilizer α (φ ω)) /-- **Class formula** for a finite group acting on a finite type. See `mul_action.card_eq_sum_card_group_div_card_stabilizer` for a specialized version using