Grace/Cumulus/Algebra/Group/Action.g17

Open in Workbench Download source

Imports

Lagrange · Homomorphism

Declarations

Source

1-- Group actions: an action act : G ↷ X of a group on a set, written2-- g ·ₐ x, its orbits and stabilizers, the stabilizer a subgroup, the orbit3-- of a point in bijection with the cosets of its stabilizer, so the4-- orbit–stabilizer theorem, the orbits a partition of the set, the fixed5-- points, and the count of the points outside the fixed points6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Group.Action12import Lagrange13import Homomorphism1415-- act : G ↷ X: a function act : G.carrier × X → X under which the unit16-- acts trivially and a product acts by composition. The form is a17-- transparent guard, so a hypothesis act : G ↷ X also supplies the group G18-- and its operation a * b; the action of g on x is written g ·ₐ x.19predicate Action (act G X : Set) :=20  Group(G) ∧ (act : G.carrier × X → X) ∧21  (∀ x ∈ X, act(G.one, x) = x) ∧22  (∀ g h ∈ G.carrier, ∀ x ∈ X, act(g * h, x) = act(g, act(h, x)))2324notation guard "_ : _ ↷ _" => Action25notation infixr 73 "·ₐ" => call2(act, _, _) via hypothesis Action(act, G, X) for G.carrier2627-- The orbit of x, its stabilizer, the fixed points of the action, the set28-- of all orbits, and the elements carrying x to y.29def orbit (act G X x : Set) : Set := { y ∈ X | ∃ g ∈ G.carrier, y = act(g, x) }30def stabilizer (act G X x : Set) : Set := { g ∈ G.carrier | act(g, x) = x }31def fixedPoints (act G X : Set) : Set :=32  { x ∈ X | ∀ g ∈ G.carrier, act(g, x) = x }33def orbits (act G X : Set) : Set :=34  { O ∈ 𝒫(X) | ∃ x ∈ X, O = orbit(act, G, X, x) }35def transporters (act G x y : Set) : Set := { g ∈ G.carrier | act(g, x) = y }3637-- The orbit and the stabilizer of x are written orbit(x) and stabilizer(x)38-- wherever a hypothesis in scope supplies the action.39notation function "orbit(x)" => orbit(act, G, X, x) via hypothesis Action(act, G, X)40notation function "stabilizer(x)" => stabilizer(act, G, X, x) via hypothesis Action(act, G, X)4142theorem Action.mk (act G X : Set)43  requires group : Group(G)44  requires function : act : G.carrier × X → X45  requires unit : ∀ x ∈ X, act(G.one, x) = x46  requires compatible : ∀ g h ∈ G.carrier, ∀ x ∈ X, act(g * h, x) = act(g, act(h, x))47  shows act : G ↷ X48proof49  unfold Action50  refine ⟨group, function, unit, compatible⟩5152theorem orbit.subset (act G X x : Set)53  shows orbit(act, G, X, x) ⊆ X54proof55  intros y hy56  have parts := orbit.membership.forward with hy57  exact parts.left5859theorem stabilizer.subset (act G X x : Set)60  shows stabilizer(act, G, X, x) ⊆ G.carrier61proof62  intros g hg63  have parts := stabilizer.membership.forward with hg64  exact parts.left6566theorem fixedPoints.subset (act G X : Set)67  shows fixedPoints(act, G, X) ⊆ X68proof69  intros x hx70  have parts := fixedPoints.membership.forward with hx71  exact parts.left7273theorem orbits.subset_powerset (act G X : Set)74  shows orbits(act, G, X) ⊆ 𝒫(X)75proof76  intros O hO77  have parts := orbits.membership.forward with hO78  exact parts.left7980theorem orbits.orbit_member (act G X x : Set)81  requires hx : x ∈ X82  shows orbit(act, G, X, x) ∈ orbits(act, G, X)83proof84  have subset := orbit.subset at act, G, X, x85  have bounded := powerset.membership_iff.backward with subset86  exact orbits.membership.backward with ⟨bounded, x, hx, rfl⟩8788section ActionLaws89variable (act G X : Set)90hypothesis action : act : G ↷ X9192theorem Action.group93  shows Group(G)94proof95  obtain ⟨group, rest⟩ := action96  exact group9798theorem Action.function99  shows act : G.carrier × X → X100proof101  obtain ⟨group, function, rest⟩ := action102  exact function103104theorem one_act (x : Set)105  requires hx : x ∈ X106  shows G.one ·ₐ x = x107proof108  obtain ⟨group, function, unit, compatible⟩ := action109  exact unit with x, hx110111theorem mul_act (g h : G) (x : Set)112  requires hx : x ∈ X113  shows (g * h) ·ₐ x = g ·ₐ h ·ₐ x114proof115  obtain ⟨group, function, unit, compatible⟩ := action116  have gIn : g ∈ G by assumption117  have hIn : h ∈ G by assumption118  exact compatible with g, gIn, h, hIn, x, hx119120-- Closure: the action of an element on a point is a point, so the121-- membership of a compound term is synthesized.122instance Action.act_mem (g : G) (x : Set)123  requires hx : x ∈ X124  shows g ·ₐ x ∈ X125proof126  have function := Action.function with action127  have gIn : g ∈ G by assumption128  have pair := product.pair at g, x, G.carrier, X with *129  unfold call2130  exact FunctionBetween.apply_closed with function, pair131132theorem inv_act_cancel (g : G) (x : Set)133  requires hx : x ∈ X134  shows g⁻¹ ·ₐ g ·ₐ x = x135proof136  have group := Action.group with action137  have merged : (g⁻¹ * g) ·ₐ x = g⁻¹ ·ₐ g ·ₐ x := mul_act with *138  rw [← merged, Group.inv_mul, one_act]139  rfl140141theorem act_inv_cancel (g : G) (x : Set)142  requires hx : x ∈ X143  shows g ·ₐ g⁻¹ ·ₐ x = x144proof145  have group := Action.group with action146  have merged : (g * g⁻¹) ·ₐ x = g ·ₐ g⁻¹ ·ₐ x := mul_act with *147  rw [← merged, Group.mul_inv, one_act]148  rfl149150theorem act_left_cancel (g : G) (x y : Set)151  requires hx : x ∈ X152  requires hy : y ∈ X153  requires equal : g ·ₐ x = g ·ₐ y154  shows x = y155proof156  have group := Action.group with action157  calc158    x = g⁻¹ ·ₐ g ·ₐ x := by rw inv_act_cancel159    _ = g⁻¹ ·ₐ g ·ₐ y := by rw equal160    _ = y := by rw inv_act_cancel161162theorem act_eq_iff (g : G) (x y : Set)163  requires hx : x ∈ X164  requires hy : y ∈ X165  shows g ·ₐ x = y ↔ x = g⁻¹ ·ₐ y166proof167  have group := Action.group with action168  constructor169  . intro equal170    rw [← equal, inv_act_cancel]171    rfl172  . intro equal173    rw [equal, act_inv_cancel]174    rfl175176-- Orbits: every point lies in its own orbit, orbits are closed under the177-- action, any member of an orbit generates it, and two orbits are equal or178-- disjoint.179instance orbit.act_mem (g : G) (x : Set)180  requires hx : x ∈ X181  shows g ·ₐ x ∈ orbit(x)182proof183  have moved : g ·ₐ x ∈ X := Action.act_mem with *184  have gIn : g ∈ G by assumption185  exact orbit.membership.backward with ⟨moved, g, gIn, rfl⟩186187theorem orbit.self (x : Set)188  requires hx : x ∈ X189  shows x ∈ orbit(x)190proof191  have group := Action.group with action192  have member : G.one ·ₐ x ∈ orbit(x) := orbit.act_mem with *193  have fixed : G.one ·ₐ x = x := one_act with *194  rwa fixed at member195196theorem orbit.act_mem_of_mem (g : G) (x y : Set)197  requires hx : x ∈ X198  requires hy : y ∈ orbit(x)199  shows g ·ₐ y ∈ orbit(x)200proof201  have group := Action.group with action202  obtain ⟨yIn, h, hIn, yEq⟩ := orbit.membership.forward with hy203  have merged : (g * h) ·ₐ x = g ·ₐ h ·ₐ x := mul_act with *204  have member : (g * h) ·ₐ x ∈ orbit(x) := orbit.act_mem with *205  rw [yEq, ← merged]206  exact member207208theorem orbit.of_member (x y : Set)209  requires hx : x ∈ X210  requires hy : y ∈ orbit(x)211  shows orbit(y) = orbit(x)212proof213  have group := Action.group with action214  obtain ⟨yIn, h, hIn, yEq⟩ := orbit.membership.forward with hy215  ext z216  constructor217  . intro hz218    obtain ⟨zIn, g, gIn, zEq⟩ := orbit.membership.forward with hz219    have merged : (g * h) ·ₐ x = g ·ₐ h ·ₐ x := mul_act with *220    have member : (g * h) ·ₐ x ∈ orbit(x) := orbit.act_mem with *221    rw [zEq, yEq, ← merged]222    exact member223  . intro hz224    obtain ⟨zIn, g, gIn, zEq⟩ := orbit.membership.forward with hz225    have back : h⁻¹ ·ₐ y = x226      rw [yEq, inv_act_cancel]227      rfl228    have merged : (g * h⁻¹) ·ₐ y = g ·ₐ h⁻¹ ·ₐ y := mul_act with *229    have member : (g * h⁻¹) ·ₐ y ∈ orbit(y) := orbit.act_mem with *230    rw [zEq, ← back, ← merged]231    exact member232233theorem orbit.eq_of_common (x y z : Set)234  requires hx : x ∈ X235  requires hy : y ∈ X236  requires hzx : z ∈ orbit(x)237  requires hzy : z ∈ orbit(y)238  shows orbit(x) = orbit(y)239proof240  have first : orbit(z) = orbit(x) := orbit.of_member with *241  have second : orbit(z) = orbit(y) := orbit.of_member with *242  rwa first at second243244theorem orbit.eq_or_disjoint (x y : Set)245  requires hx : x ∈ X246  requires hy : y ∈ X247  shows orbit(x) = orbit(y) ∨ Disjoint(orbit(x), orbit(y))248proof249  by_contra neither250  apply neither251  right252  apply Disjoint.iff.backward253  intros z hzx hzy254  apply neither255  left256  exact orbit.eq_of_common with *257258theorem orbit.finite (x : Set)259  requires finite : Finite(X)260  shows Finite(orbit(x))261proof262  exact Finite.subset with finite, (orbit.subset at act, G, X, x)263264-- The orbits partition the set.265theorem orbits.cover266  shows ⋃(orbits(act, G, X)) = X267proof268  ext x269  constructor270  . intro hx271    obtain ⟨O, hO, hxO⟩ := union.membership.forward with hx272    have bounded := orbits.subset_powerset at act, G, X273    have subset := powerset.membership_iff.forward with (bounded with O, hO)274    exact subset with x, hxO275  . intro hx276    have self : x ∈ orbit(x) := orbit.self with *277    have member := orbits.orbit_member at act, G, X, x with hx278    exact union.membership.backward with ⟨orbit(x), member, self⟩279280theorem orbits.pairwise_disjoint281  shows PairwiseDisjoint(orbits(act, G, X))282proof283  intros O hO P hP different284  obtain ⟨boundO, x, hx, OEq⟩ := orbits.membership.forward with hO285  obtain ⟨boundP, y, hy, PEq⟩ := orbits.membership.forward with hP286  rw [OEq, PEq] at different287  rw [OEq, PEq]288  have split := orbit.eq_or_disjoint at act, G, X, x, y with *289  cases split with equal | disjoint290  . exfalso291    exact different with equal292  . exact disjoint293294theorem orbits.finite295  requires finite : Finite(X)296  shows Finite(orbits(act, G, X))297proof298  have finitePowerset := Finite.powerset with finite299  exact Finite.subset with finitePowerset, (orbits.subset_powerset at act, G, X)300301theorem orbits.member_finite (O : Set)302  requires hO : O ∈ orbits(act, G, X)303  requires finite : Finite(X)304  shows Finite(O)305proof306  have bounded := orbits.subset_powerset at act, G, X307  have subset := powerset.membership_iff.forward with (bounded with O, hO)308  exact Finite.subset with finite, subset309310-- Stabilizers are subgroups.311theorem stabilizer.fixes (g x : Set)312  requires hg : g ∈ stabilizer(x)313  shows g ·ₐ x = x314proof315  have parts := stabilizer.membership.forward with hg316  exact parts.right317318theorem stabilizer.of_fixes (g : G) (x : Set)319  requires fixed : g ·ₐ x = x320  shows g ∈ stabilizer(x)321proof322  have gIn : g ∈ G by assumption323  exact stabilizer.membership.backward with ⟨gIn, fixed⟩324325theorem stabilizer.subgroup (x : Set)326  requires hx : x ∈ X327  shows Subgroup(stabilizer(x), G)328proof329  have group := Action.group with action330  have unitIn : G.one ∈ stabilizer(x)331    have fixed : G.one ·ₐ x = x := one_act with *332    exact stabilizer.of_fixes with *333  apply Subgroup.mk with group, (stabilizer.subset at act, G, X, x), unitIn334  . intros g hg h hh335    have gIn := stabilizer.subset at act, G, X, x with g, hg336    have hIn := stabilizer.subset at act, G, X, x with h, hh337    have fixedG : g ·ₐ x = x := stabilizer.fixes with *338    have fixedH : h ·ₐ x = x := stabilizer.fixes with *339    have fixed : (g * h) ·ₐ x = x340      rw [mul_act, fixedH, fixedG]341      rfl342    exact stabilizer.of_fixes with *343  . intros g hg344    have gIn := stabilizer.subset at act, G, X, x with g, hg345    have fixedG : g ·ₐ x = x := stabilizer.fixes with *346    have fixed : g⁻¹ ·ₐ x = x347      calc348        g⁻¹ ·ₐ x = g⁻¹ ·ₐ g ·ₐ x := by rw fixedG349        _ = x := by rw inv_act_cancel350    exact stabilizer.of_fixes with *351352-- The elements carrying x to g ·ₐ x form the coset of the stabilizer by g.353theorem transporters.eq_coset (g : G) (x : Set)354  requires hx : x ∈ X355  shows transporters(act, G, x, g ·ₐ x) = g • stabilizer(x)356proof357  have group := Action.group with action358  have subgroup := stabilizer.subgroup with *359  ext h360  constructor361  . intro hh362    obtain ⟨hIn, carries⟩ := transporters.membership.forward with hh363    have criterion : h ∈ g • stabilizer(x) ↔ g⁻¹ * h ∈ stabilizer(x) :=364      leftCoset.mem_iff with *365    have fixed : (g⁻¹ * h) ·ₐ x = x366      rw [mul_act, carries, inv_act_cancel]367      rfl368    have member : g⁻¹ * h ∈ stabilizer(x) := stabilizer.of_fixes with *369    exact criterion.backward with member370  . intro hh371    have hIn := leftCoset.subset at G, g, stabilizer(x) with h, hh372    have criterion : h ∈ g • stabilizer(x) ↔ g⁻¹ * h ∈ stabilizer(x) :=373      leftCoset.mem_iff with *374    have member := criterion.forward with hh375    have fixed : (g⁻¹ * h) ·ₐ x = x := stabilizer.fixes with *376    have merged : (g * (g⁻¹ * h)) ·ₐ x = g ·ₐ (g⁻¹ * h) ·ₐ x := mul_act with *377    rw [mul_inv_cancel_left, fixed] at merged378    exact transporters.membership.backward with ⟨hIn, merged⟩379380end ActionLaws381382-- Each point of the orbit of x is sent to the coset of the elements383-- carrying x to it.384defgraph orbitCosetMap (act G X x : Set) (y ∈ orbit(act, G, X, x)) :385    leftCosets(G, stabilizer(act, G, X, x)) := transporters(act, G, x, y)386requires action : act : G ↷ X387requires hx : x ∈ X388proof389  obtain ⟨yIn, g, gIn, yEq⟩ := orbit.membership.forward with member390  have coset := transporters.eq_coset with action, hx, gIn391  rw [yEq, coset]392  exact leftCosets.coset_member with gIn393394section OrbitStabilizer395variable (act G X : Set)396hypothesis action : act : G ↷ X397398theorem orbitCosetMap.injective (x : Set)399  requires hx : x ∈ X400  shows InjectiveBetween(orbitCosetMap(act, G, X, x), orbit(x),401    leftCosets(G, stabilizer(x)))402proof403  have function := orbitCosetMap.function at act, G, X, x with *404  constructor405  . exact function406  . intros y hy z hz C hC hyC hzC407    have yValue := FunctionBetween.apply_value with function, hy, hyC408    have zValue := FunctionBetween.apply_value with function, hz, hzC409    have yImage := orbitCosetMap.value at act, G, X, x, y with *410    have zImage := orbitCosetMap.value at act, G, X, x, z with *411    have same : transporters(act, G, x, y) = transporters(act, G, x, z) by cc412    obtain ⟨yIn, g, gIn, yEq⟩ := orbit.membership.forward with hy413    have carriesY : g ·ₐ x = y414      symm415      exact yEq416    have carries : g ∈ transporters(act, G, x, y) :=417      transporters.membership.backward with ⟨gIn, carriesY⟩418    rw same at carries419    have parts := transporters.membership.forward with carries420    rw ← carriesY421    exact parts.right422423theorem orbitCosetMap.surjective (x : Set)424  requires hx : x ∈ X425  shows SurjectiveBetween(orbitCosetMap(act, G, X, x), orbit(x),426    leftCosets(G, stabilizer(x)))427proof428  have function := orbitCosetMap.function at act, G, X, x with *429  constructor430  . exact function431  . intros C hC432    obtain ⟨bound, g, gIn, CEq⟩ := leftCosets.membership.forward with hC433    have moved : g ·ₐ x ∈ orbit(x) := orbit.act_mem with *434    have coset := transporters.eq_coset with action, hx, gIn435    have value := orbitCosetMap.value at act, G, X, x, g ·ₐ x with *436    have edge := FunctionBetween.relates_apply with function, moved437    witness g ·ₐ x438    constructor439    . exact moved440    . rw [value, coset, ← CEq] at edge441      exact edge442443theorem orbitCosetMap.bijective (x : Set)444  requires hx : x ∈ X445  shows BijectiveBetween(orbitCosetMap(act, G, X, x), orbit(x),446    leftCosets(G, stabilizer(x)))447proof448  constructor449  . exact orbitCosetMap.injective with *450  . exact orbitCosetMap.surjective with *451452theorem orbit.equipotent_cosets (x : Set)453  requires hx : x ∈ X454  shows orbit(x) ≃ leftCosets(G, stabilizer(x))455proof456  witness orbitCosetMap(act, G, X, x)457  exact orbitCosetMap.bijective with *458459theorem orbit.finite_of_group (x : Set)460  requires hx : x ∈ X461  requires finite : Finite(G)462  shows Finite(orbit(x))463proof464  have group := Action.group with action465  have subgroup := stabilizer.subgroup with *466  have finiteCosets := leftCosets.finite with *467  have equipotent := orbit.equipotent_cosets with *468  exact Finite.of_equipotent with469    finiteCosets, (Equipotent.symmetric with equipotent)470471theorem orbit.cardinality_eq_index (x : Set)472  requires hx : x ∈ X473  requires finite : Finite(G)474  shows cardinality(orbit(x)) = index(G, stabilizer(x))475proof476  have finiteOrbit := orbit.finite_of_group with *477  have bijective := orbitCosetMap.bijective with *478  rw index.value479  exact cardinality.bijective with finiteOrbit, bijective480481-- The orbit–stabilizer theorem.482theorem orbit_stabilizer (x : Set)483  requires hx : x ∈ X484  requires finite : Finite(G)485  shows cardinality(orbit(x)) * cardinality(stabilizer(x)) = order(G)486proof487  have group := Action.group with action488  have subgroup := stabilizer.subgroup with *489  have count := lagrange with *490  have same := orbit.cardinality_eq_index with *491  rw [same, count]492  rfl493494theorem orbit.cardinality_dvd (x : Set)495  requires hx : x ∈ X496  requires finite : Finite(G)497  shows cardinality(orbit(x)) ∣ order(G)498proof499  have group := Action.group with action500  have subgroup := stabilizer.subgroup with *501  have finiteStabilizer := Subgroup.finite with *502  have stabilizerNat := cardinality.nat with finiteStabilizer503  have orbitNat := cardinality.nat with (orbit.finite_of_group with *)504  witness cardinality(stabilizer(x))505  exact orbit_stabilizer with *506507end OrbitStabilizer508509section FixedPoints510variable (act G X : Set)511hypothesis action : act : G ↷ X512513-- A fixed point is a point whose orbit is itself alone.514theorem fixedPoints.fixes (g : G) (x : Set)515  requires hx : x ∈ fixedPoints(act, G, X)516  shows g ·ₐ x = x517proof518  have parts := fixedPoints.membership.forward with hx519  have gIn : g ∈ G by assumption520  exact parts.right with g, gIn521522theorem fixedPoints.orbit (x : Set)523  requires hx : x ∈ fixedPoints(act, G, X)524  shows orbit(x) = {x}525proof526  have xIn := fixedPoints.subset at act, G, X with x, hx527  ext y528  constructor529  . intro hy530    obtain ⟨yIn, g, gIn, yEq⟩ := orbit.membership.forward with hy531    have fixed : g ·ₐ x = x := fixedPoints.fixes with *532    rw [yEq, fixed]533    exact singleton.self534  . intro hy535    have equal := singleton.membership.forward with hy536    rw equal537    exact orbit.self with *538539theorem fixedPoints.of_orbit (x : Set)540  requires hx : x ∈ X541  requires single : orbit(x) = {x}542  shows x ∈ fixedPoints(act, G, X)543proof544  apply fixedPoints.membership.backward545  refine ⟨hx, ?_⟩546  intros g gIn547  have member : g ·ₐ x ∈ orbit(x) := orbit.act_mem with *548  rw single at member549  exact singleton.membership.forward with member550551theorem fixedPoints.iff_orbit (x : Set)552  requires hx : x ∈ X553  shows x ∈ fixedPoints(act, G, X) ↔ orbit(x) = {x}554proof555  constructor556  . intro fixed557    exact fixedPoints.orbit with *558  . intro single559    exact fixedPoints.of_orbit with *560561theorem fixedPoints.finite562  requires finite : Finite(X)563  shows Finite(fixedPoints(act, G, X))564proof565  exact Finite.subset with finite, (fixedPoints.subset at act, G, X)566567end FixedPoints568569-- The orbits not inside the fixed points.570def movedOrbits (act G X : Set) : Set :=571  { O ∈ orbits(act, G, X) | ¬(O ⊆ fixedPoints(act, G, X)) }572573theorem movedOrbits.subset (act G X : Set)574  shows movedOrbits(act, G, X) ⊆ orbits(act, G, X)575proof576  intros O hO577  have parts := movedOrbits.membership.forward with hO578  exact parts.left579580-- A sum of multiples of d is a multiple of d.581theorem natSum.dvd_of_cardinality (n : Nat)582  shows ∀ V, ∀ w, ∀ d, Nat(d) → HasCardinality(V, n) → (∀ v ∈ V, w(v) ∈ ℕ) →583    (∀ v ∈ V, d ∣ w(v)) → d ∣ natSum(V, w)584proof585  induction n586  | zero =>587    intros V w d dNat counted weights divisible588    have empty := HasCardinality.empty_of_zero at V with counted589    rw [empty, natSum.empty]590    exact divides.zero at d591  | k + 1 using ih =>592    intros V w d dNat counted weights divisible593    have hk : k + 1 = succ(k) := add.right_one with *594    rw hk at counted595    obtain ⟨a, member⟩ := HasCardinality.exists_member with counted596    have rest := HasCardinality.remove at V, a, k with counted, member597    have fresh : ¬a ∈ V ∖ {a} by simp [difference.membership, singleton.membership]598    have restored := insert.restore with member599    have restSubset := difference.subset_left at V, {a}600    have restWeights : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ601      intros v hv602      exact weights with v, (restSubset with v, hv)603    have restDivisible : ∀ v ∈ V ∖ {a}, d ∣ w(v)604      intros v hv605      exact divisible with v, (restSubset with v, hv)606    have restSum := ih with V ∖ {a}, w, d, dNat, rest, restWeights, restDivisible607    have restFinite := Finite.from_cardinality with rest608    have weight := weights with a, member609    have weightA := divisible with a, member610    have split := natSum.insert at V ∖ {a}, w, a with611      restFinite, restWeights, weight, fresh612    rw restored at split613    rw split614    have weightNat := nat.omega.backward with weight615    have sumNat := natSum.natural at V ∖ {a}, w with restFinite, restWeights616    exact divides.add with restSum, weightA617618theorem natSum.dvd (V w : Set) (d : Nat)619  requires finite : Finite(V)620  requires weights : ∀ v ∈ V, w(v) ∈ ℕ621  requires divisible : ∀ v ∈ V, d ∣ w(v)622  shows d ∣ natSum(V, w)623proof624  have counted := cardinality.correct with finite625  have natV := cardinality.nat with finite626  have all := natSum.dvd_of_cardinality at cardinality(V)627  exact all with V, w, d, assumption, counted, weights, divisible628629-- A disjoint union of finite sets each of size divisible by d has size630-- divisible by d.631theorem cardinality.big_union_dvd (F : Set) (d : Nat)632  requires finite : Finite(F)633  requires members : ∀ S ∈ F, Finite(S)634  requires disjoint : PairwiseDisjoint(F)635  requires sizes : ∀ S ∈ F, d ∣ cardinality(S)636  shows d ∣ cardinality(⋃F)637proof638  have count := cardinality.big_union_disjoint with finite, members, disjoint639  have weights : ∀ S ∈ F, sizeMap(F)(S) ∈ ℕ640    intros S hS641    have value := sizeMap.value at F, S with members, hS642    rw value643    exact nat.omega.forward with (cardinality.nat with (members with S, hS))644  have divisible : ∀ S ∈ F, d ∣ sizeMap(F)(S)645    intros S hS646    have value := sizeMap.value at F, S with members, hS647    rw value648    exact sizes with S, hS649  rw count650  exact natSum.dvd with finite, weights, divisible651652section MovedPoints653variable (act G X : Set)654hypothesis action : act : G ↷ X655656-- The orbits not inside the fixed points cover exactly the points outside657-- the fixed points, and each is the orbit of such a point.658theorem movedOrbits.cover659  shows ⋃(movedOrbits(act, G, X)) = X ∖ fixedPoints(act, G, X)660proof661  ext x662  constructor663  . intro hx664    obtain ⟨O, hO, hxO⟩ := union.membership.forward with hx665    obtain ⟨orbitO, moved⟩ := movedOrbits.membership.forward with hO666    obtain ⟨bound, y, hy, OEq⟩ := orbits.membership.forward with orbitO667    have xInOrbit : x ∈ orbit(y)668      rw OEq at hxO669      exact hxO670    have xIn := orbit.subset at act, G, X, y with x, xInOrbit671    apply difference.membership.backward672    refine ⟨xIn, ?_⟩673    intro fixed674    apply moved675    have single : orbit(x) = {x} := fixedPoints.orbit with *676    have same : orbit(x) = orbit(y) := orbit.of_member with action, hy, xInOrbit677    rw [OEq, ← same, single]678    intros z hz679    have equal := singleton.membership.forward with hz680    rw equal681    exact fixed682  . intro hx683    obtain ⟨xIn, notFixed⟩ := difference.membership.forward with hx684    have self : x ∈ orbit(x) := orbit.self with *685    have member := orbits.orbit_member at act, G, X, x with xIn686    have moved : ¬(orbit(x) ⊆ fixedPoints(act, G, X))687      intro included688      exact notFixed with (included with x, self)689    have inMoved := movedOrbits.membership.backward at act, G, X, orbit(x) with690      ⟨member, moved⟩691    exact union.membership.backward with ⟨orbit(x), inMoved, self⟩692693theorem movedOrbits.representative (O : Set)694  requires hO : O ∈ movedOrbits(act, G, X)695  shows ∃ x ∈ X, ¬x ∈ fixedPoints(act, G, X) ∧ O = orbit(x)696proof697  obtain ⟨orbitO, moved⟩ := movedOrbits.membership.forward with hO698  obtain ⟨bound, y, hy, OEq⟩ := orbits.membership.forward with orbitO699  witness y700  refine ⟨hy, ?_, OEq⟩701  intro fixed702  apply moved703  have single : orbit(y) = {y} := fixedPoints.orbit with *704  rw [OEq, single]705  intros z hz706  have equal := singleton.membership.forward with hz707  rw equal708  exact fixed709710-- If every orbit outside the fixed points has size divisible by d, so has711-- the set of points outside the fixed points.712theorem fixedPoints.difference_dvd (d : Nat)713  requires finite : Finite(X)714  requires orbitsDivisible : ∀ x ∈ X,715    ¬x ∈ fixedPoints(act, G, X) → d ∣ cardinality(orbit(x))716  shows d ∣ cardinality(X ∖ fixedPoints(act, G, X))717proof718  have movedSubset := movedOrbits.subset at act, G, X719  have finiteMoved := Finite.subset with (orbits.finite with *), movedSubset720  have members : ∀ O ∈ movedOrbits(act, G, X), Finite(O)721    intros O hO722    exact orbits.member_finite with action, (movedSubset with O, hO), finite723  have disjoint := PairwiseDisjoint.subset with724    movedSubset, (orbits.pairwise_disjoint with action)725  have sizes : ∀ O ∈ movedOrbits(act, G, X), d ∣ cardinality(O)726    intros O hO727    obtain ⟨x, hx, notFixed, OEq⟩ := movedOrbits.representative with *728    rw OEq729    exact orbitsDivisible with x, hx, notFixed730  have count := cardinality.big_union_dvd with finiteMoved, members, disjoint, sizes731  rwa movedOrbits.cover at count732733end MovedPoints734