Grace/Cumulus/Algebra/Group/Translation.g17

Open in Workbench Download source

Imports

Conjugation · Combinatorics.Basics

Declarations

Source

1-- Translation: the action of a group on a family of its subsets by left2-- multiplication, a translate of a finite subset having its size, the3-- subsets of a given size and the cosets of a subgroup closed under4-- translation, the stabilizer of a subset no larger than the subset, and5-- the restriction of an action to a subgroup or to an invariant subset6-- 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.Translation12import Conjugation13import Combinatorics.Basics1415-- Left multiplication on a family F of subsets of G, as a graph on16-- (G.carrier × F) × F, and the families closed under it.17def translation (G F : Set) : Set :=18  { p ∈ (G.carrier × F) × F |19    ∃ g ∈ G.carrier, ∃ S ∈ F, p = ((g, S) ↦ leftCoset(G, g, S)) }2021predicate TranslationClosed (G F : Set) :=22  ∀ g ∈ G.carrier, ∀ S ∈ F, leftCoset(G, g, S) ∈ F2324theorem subsetsOfSize.subset_powerset (A k : Set)25  shows subsetsOfSize(A, k) ⊆ 𝒫(A)26proof27  intros S hS28  have parts := subsetsOfSize.membership.forward with hS29  exact parts.left3031theorem subsetsOfSize.nonempty (A S : Set) (k : Nat)32  requires hS : S ∈ subsetsOfSize(A, k)33  requires nonzero : k ≠ 034  shows Nonempty(S)35proof36  obtain ⟨bound, counted⟩ := subsetsOfSize.membership.forward with hS37  have shape := natural.zero_or_successor at k38  cases shape with zero | successor39  . exfalso40    exact nonzero with zero41  . obtain ⟨j, jNat, kEq⟩ := successor42    rw kEq at counted43    exact HasCardinality.exists_member with counted4445section Translation46variable (G : Set)47hypothesis group : Group(G)4849-- Translating a subset of G: the translate of s ∈ S by g is g * s, the50-- unit translates trivially, and translating twice translates by the51-- product.52theorem leftCoset.mul_mem_of_subset (g : G) (S s : Set)53  requires bounded : S ⊆ G54  requires hs : s ∈ S55  shows g * s ∈ g • S56proof57  have sIn := bounded with s, hs58  have product : g * s ∈ G by typecheck59  exact leftCoset.membership.backward with ⟨product, s, hs, rfl⟩6061theorem leftCoset.one_of_subset (S : Set)62  requires bounded : S ⊆ G63  shows G.one • S = S64proof65  ext y66  constructor67  . intro hy68    obtain ⟨yIn, s, hs, yEq⟩ := leftCoset.membership.forward with hy69    have sIn := bounded with s, hs70    rw [yEq, one_mul]71    exact hs72  . intro hy73    have yIn := bounded with y, hy74    have identity : G.one * y = y := one_mul with *75    apply leftCoset.membership.backward76    refine ⟨yIn, y, hy, ?_⟩77    symm78    exact identity7980theorem leftCoset.mul_of_subset (g h : G) (S : Set)81  requires bounded : S ⊆ G82  shows g • (h • S) = (g * h) • S83proof84  ext y85  constructor86  . intro hy87    obtain ⟨yIn, z, hz, yEq⟩ := leftCoset.membership.forward with hy88    obtain ⟨zIn, s, hs, zEq⟩ := leftCoset.membership.forward with hz89    have sIn := bounded with s, hs90    apply leftCoset.membership.backward91    refine ⟨yIn, s, hs, ?_⟩92    rw [yEq, zEq, mul_assoc]93    rfl94  . intro hy95    obtain ⟨yIn, s, hs, yEq⟩ := leftCoset.membership.forward with hy96    have sIn := bounded with s, hs97    have inner : h * s ∈ h • S := leftCoset.mul_mem_of_subset with *98    apply leftCoset.membership.backward99    refine ⟨yIn, h * s, inner, ?_⟩100    rw [yEq, mul_assoc]101    rfl102103-- The translation graph is a function, and an action on a family closed104-- under translation.105theorem translation.relates (F g S : Set)106  requires closed : TranslationClosed(G, F)107  requires hg : g ∈ G108  requires hS : S ∈ F109  shows relates(translation(G, F), (g, S), g • S)110proof111  have moved := closed with g, hg, S, hS112  have input := product.pair at g, S, G.carrier, F with *113  have bounded := product.pair at (g, S), g • S, G.carrier × F, F with *114  unfold relates115  apply translation.membership.backward116  refine ⟨bounded, g, hg, S, hS, rfl⟩117118theorem translation.function (F : Set)119  requires closed : TranslationClosed(G, F)120  shows translation(G, F) : G.carrier × F → F121proof122  unfold FunctionBetween123  refine ⟨?_, ?_, ?_⟩124  . intros p hp125    have parts := translation.membership.forward with hp126    exact parts.left127  . intros p y edge z edge2128    unfold relates at edge129    unfold relates at edge2130    obtain ⟨bounded, g, hg, S, hS, shape⟩ :=131      translation.membership.forward with edge132    obtain ⟨bounded2, g2, hg2, S2, hS2, shape2⟩ :=133      translation.membership.forward with edge2134    have outer := orderedPair.injective with shape135    have outer2 := orderedPair.injective with shape2136    have inputs : (g, S) = (g2, S2) by cc137    have halves := orderedPair.injective with inputs138    cc139  . intros p hp140    obtain ⟨bound, g, hg, S, hS, shape⟩ := product.membership.forward with hp141    have moved := closed with g, hg, S, hS142    have edge := translation.relates with closed, hg, hS143    refine ⟨g • S, moved, ?_⟩144    rw shape145    exact edge146147theorem translation.value (F g S : Set)148  requires closed : TranslationClosed(G, F)149  requires hg : g ∈ G150  requires hS : S ∈ F151  shows translation(G, F)(g, S) = g • S152proof153  have function := translation.function with group, closed154  have edge := translation.relates with closed, hg, hS155  have input := product.pair at g, S, G.carrier, F with *156  have value := FunctionBetween.apply_value with function, input, edge157  unfold call2158  exact value159160theorem translation.action (F : Set)161  requires bounded : F ⊆ 𝒫(G.carrier)162  requires closed : TranslationClosed(G, F)163  shows translation(G, F) : G ↷ F164proof165  have function := translation.function with group, closed166  apply Action.mk with group, function167  . intros S hS168    have subset := powerset.membership_iff.forward with (bounded with S, hS)169    have unitIn : G.one ∈ G := Group.one_mem with *170    have value := translation.value with closed, unitIn, hS171    rw value172    exact leftCoset.one_of_subset with *173  . intros g hg h hh S hS174    have subset := powerset.membership_iff.forward with (bounded with S, hS)175    have moved := closed with h, hh, S, hS176    have product : g * h ∈ G by typecheck177    have first := translation.value with closed, hh, hS178    have second := translation.value with closed, hg, moved179    have third := translation.value with closed, product, hS180    rw [third, first, second]181    symm182    exact leftCoset.mul_of_subset with *183184end Translation185186-- Translation by g carries a subset S of G onto g • S.187defgraph translateMap (G S g : Set) (s ∈ S) : leftCoset(G, g, S) := g * s188requires group : Group(G)189requires bounded : S ⊆ G.carrier190requires hg : g ∈ G.carrier191proof192  exact leftCoset.mul_mem_of_subset with *193194section TranslateSize195variable (G : Set)196hypothesis group : Group(G)197198theorem translateMap.injective (S : Set) (g : G)199  requires bounded : S ⊆ G200  shows InjectiveBetween(translateMap(G, S, g), S, g • S)201proof202  have function := translateMap.function at G, S, g with *203  constructor204  . exact function205  . intros x hx y hy z hz hxz hyz206    have xValue := FunctionBetween.apply_value with function, hx, hxz207    have yValue := FunctionBetween.apply_value with function, hy, hyz208    have xImage := translateMap.value at G, S, g, x with *209    have yImage := translateMap.value at G, S, g, y with *210    have xIn := bounded with x, hx211    have yIn := bounded with y, hy212    have equal : g * x = g * y by cc213    exact mul_left_cancel with *214215theorem translateMap.surjective (S : Set) (g : G)216  requires bounded : S ⊆ G217  shows SurjectiveBetween(translateMap(G, S, g), S, g • S)218proof219  have function := translateMap.function at G, S, g with *220  constructor221  . exact function222  . intros y hy223    obtain ⟨yIn, s, hs, yEq⟩ := leftCoset.membership.forward with hy224    have image := translateMap.value at G, S, g, s with *225    have related := FunctionBetween.relates_apply with function, hs226    witness s227    constructor228    . exact hs229    . rw [image, ← yEq] at related230      exact related231232theorem leftCoset.cardinality_of_subset (S : Set) (g : G)233  requires bounded : S ⊆ G234  requires finite : Finite(S)235  shows cardinality(g • S) = cardinality(S)236proof237  have bijective : BijectiveBetween(translateMap(G, S, g), S, g • S)238    constructor239    . exact translateMap.injective with *240    . exact translateMap.surjective with *241  symm242  exact cardinality.bijective with finite, bijective243244-- The subsets of a given size are closed under translation, so G acts on245-- them.246theorem subsetsOfSize.translation_closed (n : Nat)247  requires finite : Finite(G)248  shows TranslationClosed(G, subsetsOfSize(G.carrier, n))249proof250  intros g hg S hS251  obtain ⟨bound, counted⟩ := subsetsOfSize.membership.forward with hS252  have bounded := powerset.membership_iff.forward with bound253  have finiteS := Finite.subset with finite, bounded254  have same : cardinality(g • S) = cardinality(S) :=255    leftCoset.cardinality_of_subset with *256  have count := cardinality.eq_of_has with counted257  have translateSubset := leftCoset.subset at G, g, S258  have finiteTranslate := Finite.subset with finite, translateSubset259  have correct := cardinality.correct with finiteTranslate260  rw [same, count] at correct261  have translateBound := powerset.membership_iff.backward with translateSubset262  exact subsetsOfSize.membership.backward with ⟨translateBound, correct⟩263264theorem subsetsOfSize.action (n : Nat)265  requires finite : Finite(G)266  shows translation(G, subsetsOfSize(G.carrier, n)) : G ↷ subsetsOfSize(G.carrier, n)267proof268  have bounded := subsetsOfSize.subset_powerset at G.carrier, n269  have closed := subsetsOfSize.translation_closed with *270  exact translation.action with *271272-- The cosets of a subgroup are closed under translation, so G acts on273-- them.274theorem leftCosets.translation_closed (H : Set)275  requires subgroup : Subgroup(H, G)276  shows TranslationClosed(G, leftCosets(G, H))277proof278  intros g hg C hC279  obtain ⟨bound, h, hh, CEq⟩ := leftCosets.membership.forward with hC280  have bounded := Subgroup.subset with subgroup281  have merged : g • (h • H) = (g * h) • H := leftCoset.mul_of_subset with *282  rw [CEq, merged]283  exact leftCosets.coset_member with (Group.mul_mem with *)284285theorem leftCosets.action (H : Set)286  requires subgroup : Subgroup(H, G)287  shows translation(G, leftCosets(G, H)) : G ↷ leftCosets(G, H)288proof289  have bounded := leftCosets.subset_powerset at G, H290  have closed := leftCosets.translation_closed with *291  exact translation.action with *292293end TranslateSize294295-- Right multiplication by s as a function on the carrier.296defgraph rightTranslate (G s : Set) (x ∈ G.carrier) : G.carrier := x * s297requires group : Group(G)298requires hs : s ∈ G.carrier299proof300  exact Group.mul_mem with *301302section StabilizerBound303variable (G : Set)304hypothesis group : Group(G)305306theorem rightTranslate.injective (s : G)307  shows InjectiveBetween(rightTranslate(G, s), G.carrier, G.carrier)308proof309  have function := rightTranslate.function at G, s with *310  constructor311  . exact function312  . intros x hx y hy z hz hxz hyz313    have xValue := FunctionBetween.apply_value with function, hx, hxz314    have yValue := FunctionBetween.apply_value with function, hy, hyz315    have xImage := rightTranslate.value at G, s, x with *316    have yImage := rightTranslate.value at G, s, y with *317    have equal : x * s = y * s by cc318    exact mul_right_cancel with *319320-- The stabilizer of a nonempty subset S under translation is carried321-- injectively into S by right multiplication with a member of S, so it is322-- no larger than S.323theorem translation.stabilizer_card_le (F S : Set)324  requires bounded : F ⊆ 𝒫(G.carrier)325  requires closed : TranslationClosed(G, F)326  requires finite : Finite(G)327  requires hS : S ∈ F328  requires inhabited : Nonempty(S)329  shows cardinality(stabilizer(translation(G, F), G, F, S)) ≤ cardinality(S)330proof331  have action := translation.action with group, bounded, closed332  have subsetS := powerset.membership_iff.forward with (bounded with S, hS)333  have finiteS := Finite.subset with finite, subsetS334  obtain ⟨s, hs⟩ := inhabited335  have sIn := subsetS with s, hs336  have injective := rightTranslate.injective with group, sIn337  have stabilizerSubset := stabilizer.subset at translation(G, F), G, F, S338  have finiteStabilizer := Finite.subset with finite, stabilizerSubset339  have imageCount := cardinality.injective_image with340    injective, stabilizerSubset, finiteStabilizer341  have imageSubset : functionImage(rightTranslate(G, s), stabilizer(translation(G, F), G, F, S), G.carrier) ⊆ S342    intros y hy343    obtain ⟨yIn, h, hh, yEq⟩ := functionImage.membership.forward with hy344    have hIn := stabilizerSubset with h, hh345    have fixed : h ·ₐ S = S := stabilizer.fixes with *346    have value := translation.value with closed, hIn, hS347    have translated : h • S = S by cc348    have image := rightTranslate.value at G, s, h with *349    have member : h * s ∈ h • S := leftCoset.mul_mem_of_subset with *350    rw [yEq, image, ← translated]351    exact member352  have bound := cardinality.monotone with finiteS, imageSubset353  rwa imageCount at bound354355end StabilizerBound356357-- The restriction of an action to a subgroup is an action of the group on358-- the subgroup.359section Restriction360variable (act G X H : Set)361hypothesis action : act : G ↷ X362hypothesis subgroup : Subgroup(H, G)363364theorem Action.restrict_function365  shows restrict(act, H × X) : H × X → X366proof367  have function := Action.function with action368  have subset : H × X ⊆ G.carrier × X369    intros p hp370    obtain ⟨bound, h, hh, x, hx, shape⟩ := product.membership.forward with hp371    have hIn : h ∈ G := Subgroup.mem_carrier with *372    rw shape373    exact product.pair with hIn, hx374  exact restrict.domain_function with function, subset375376theorem Action.restrict_value (h : H) (x : Set)377  requires hx : x ∈ X378  shows restrict(act, H × X)(h, x) = h ·ₐ x379proof380  have function := Action.function with action381  have hIn : h ∈ G := Subgroup.mem_carrier with *382  have subset : H × X ⊆ G.carrier × X383    intros p hp384    obtain ⟨bound, k, hk, y, hy, shape⟩ := product.membership.forward with hp385    have kIn : k ∈ G := Subgroup.mem_carrier with *386    rw shape387    exact product.pair with kIn, hy388  have pair := product.pair at h, x, H, X with *389  have value := restrict.domain_apply with function, subset, pair390  unfold call2391  exact value392393theorem Action.restrict394  shows restrict(act, H × X) : subgroupGroup(G, H) ↷ X395proof396  have group := Action.group with action397  have subgroupGroupIs := subgroupGroup.group with group, subgroup398  have function := Action.restrict_function with action, subgroup399  have carrierFunction : restrict(act, H × X) : Group.carrier(subgroupGroup(G, H)) × X → X400    rw subgroupGroup.carrierOf401    exact function402  apply Action.mk with subgroupGroupIs, carrierFunction403  . intros x hx404    have unitIn : G.one ∈ H := Subgroup.one_mem with *405    have value := Action.restrict_value with action, subgroup, unitIn, hx406    have fixed : G.one ·ₐ x = x := one_act with *407    rw [subgroupGroup.unit, value]408    exact fixed409  . intros g hg h hh x hx410    rw subgroupGroup.carrierOf at hg411    rw subgroupGroup.carrierOf at hh412    have gIn : g ∈ G := Subgroup.mem_carrier with *413    have hIn : h ∈ G := Subgroup.mem_carrier with *414    have product : G.mul(g, h) ∈ H := Subgroup.mul_mem with *415    have moved : h ·ₐ x ∈ X := Action.act_mem with *416    have restricted : Group.mul(subgroupGroup(G, H))(g, h) = G.mul(g, h) :=417      subgroupGroup.mul with *418    have first := Action.restrict_value with action, subgroup, hh, hx419    have second := Action.restrict_value with action, subgroup, hg, moved420    have third := Action.restrict_value with action, subgroup, product, hx421    have merged : G.mul(g, h) ·ₐ x = g ·ₐ h ·ₐ x := mul_act with *422    rw [restricted, third, first, second]423    exact merged424425-- The fixed points of the restricted action are the points fixed by the426-- subgroup.427theorem Action.restrict_fixed_points (x : Set)428  shows x ∈ fixedPoints(restrict(act, H × X), subgroupGroup(G, H), X) ↔429    x ∈ X ∧ ∀ h ∈ H, h ·ₐ x = x430proof431  have criterion := fixedPoints.membership at432    restrict(act, H × X), subgroupGroup(G, H), X, x433  rw under subgroupGroup.carrierOf at criterion434  constructor435  . intro fixed436    obtain ⟨xIn, fixes⟩ := criterion.forward with fixed437    refine ⟨xIn, ?_⟩438    intros h hh439    have value := Action.restrict_value with action, subgroup, hh, xIn440    have restricted := fixes with h, hh441    rwa value at restricted442  . intro fixes443    obtain ⟨xIn, fixesH⟩ := fixes444    apply criterion.backward445    refine ⟨xIn, ?_⟩446    intros h hh447    have value := Action.restrict_value with action, subgroup, hh, xIn448    rw value449    exact fixesH with h, hh450451end Restriction452453-- The restriction of an action to a subset closed under it.454section SubsetRestriction455variable (act G X Y : Set)456hypothesis action : act : G ↷ X457hypothesis bounded : Y ⊆ X458hypothesis closed : ∀ g ∈ G.carrier, ∀ y ∈ Y, act(g, y) ∈ Y459460theorem Action.restrict_subset_value (g : G) (y : Set)461  requires hy : y ∈ Y462  shows restrict(act, G.carrier × Y)(g, y) = g ·ₐ y463proof464  have function := Action.function with action465  have subset : G.carrier × Y ⊆ G.carrier × X466    intros p hp467    obtain ⟨bound, k, hk, z, hz, shape⟩ := product.membership.forward with hp468    rw shape469    exact product.pair with hk, (bounded with z, hz)470  have pair := product.pair at g, y, G.carrier, Y with *471  have value := restrict.domain_apply with function, subset, pair472  unfold call2473  exact value474475theorem Action.restrict_subset476  shows restrict(act, G.carrier × Y) : G ↷ Y477proof478  have group := Action.group with action479  have function := Action.function with action480  have subset : G.carrier × Y ⊆ G.carrier × X481    intros p hp482    obtain ⟨bound, k, hk, z, hz, shape⟩ := product.membership.forward with hp483    rw shape484    exact product.pair with hk, (bounded with z, hz)485  have restricted := restrict.domain_function with function, subset486  have corestricted : restrict(act, G.carrier × Y) : G.carrier × Y → Y487    apply FunctionBetween.codomain_of_values with restricted488    intros p hp489    obtain ⟨bound, k, hk, z, hz, shape⟩ := product.membership.forward with hp490    have value := Action.restrict_subset_value with action, bounded, closed, hk, hz491    rw shape492    unfold call2 at value493    rw value494    have inside := closed with k, hk, z, hz495    unfold call2 at inside496    exact inside497  apply Action.mk with group, corestricted498  . intros y hy499    have yIn := bounded with y, hy500    have unitIn : G.one ∈ G := Group.one_mem with *501    have value := Action.restrict_subset_value with action, bounded, closed, unitIn, hy502    have fixed : G.one ·ₐ y = y := one_act with *503    rw value504    exact fixed505  . intros g hg h hh y hy506    have yIn := bounded with y, hy507    have moved := closed with h, hh, y, hy508    have product : g * h ∈ G by typecheck509    have first := Action.restrict_subset_value with action, bounded, closed, hh, hy510    have second := Action.restrict_subset_value with action, bounded, closed, hg, moved511    have third := Action.restrict_subset_value with action, bounded, closed, product, hy512    have merged : (g * h) ·ₐ y = g ·ₐ h ·ₐ y := mul_act with *513    rw [third, first, second]514    exact merged515516theorem Action.restrict_subset_fixed_points (y : Set)517  shows y ∈ fixedPoints(restrict(act, G.carrier × Y), G, Y) ↔518    y ∈ Y ∧ ∀ g ∈ G.carrier, g ·ₐ y = y519proof520  have criterion := fixedPoints.membership at restrict(act, G.carrier × Y), G, Y, y521  constructor522  . intro fixed523    obtain ⟨yIn, fixes⟩ := criterion.forward with fixed524    refine ⟨yIn, ?_⟩525    intros g hg526    have value := Action.restrict_subset_value with action, bounded, closed, hg, yIn527    have restricted := fixes with g, hg528    rwa value at restricted529  . intro fixes530    obtain ⟨yIn, fixesAll⟩ := fixes531    apply criterion.backward532    refine ⟨yIn, ?_⟩533    intros g hg534    have value := Action.restrict_subset_value with action, bounded, closed, hg, yIn535    rw value536    exact fixesAll with g, hg537538theorem Action.restrict_subset_orbit (y : Set)539  requires hy : y ∈ Y540  shows orbit(restrict(act, G.carrier × Y), G, Y, y) = orbit(y)541proof542  have yIn := bounded with y, hy543  ext z544  constructor545  . intro hz546    obtain ⟨zIn, g, hg, zEq⟩ := orbit.membership.forward with hz547    have value := Action.restrict_subset_value with action, bounded, closed, hg, hy548    have moved : g ·ₐ y ∈ orbit(y) := orbit.act_mem with *549    rw [zEq, value]550    exact moved551  . intro hz552    obtain ⟨zIn, g, hg, zEq⟩ := orbit.membership.forward with hz553    have value := Action.restrict_subset_value with action, bounded, closed, hg, hy554    have moved := closed with g, hg, y, hy555    apply orbit.membership.backward556    refine ⟨?_, g, hg, ?_⟩557    . rw zEq558      exact moved559    . rw [zEq, value]560      rfl561562theorem Action.restrict_subset_stabilizer (y : Set)563  requires hy : y ∈ Y564  shows stabilizer(restrict(act, G.carrier × Y), G, Y, y) = stabilizer(y)565proof566  ext g567  constructor568  . intro hg569    obtain ⟨gIn, fixed⟩ := stabilizer.membership.forward with hg570    have value := Action.restrict_subset_value with action, bounded, closed, gIn, hy571    rw value at fixed572    exact stabilizer.membership.backward with ⟨gIn, fixed⟩573  . intro hg574    obtain ⟨gIn, fixed⟩ := stabilizer.membership.forward with hg575    have value := Action.restrict_subset_value with action, bounded, closed, gIn, hy576    rw ← value at fixed577    exact stabilizer.membership.backward at578      restrict(act, G.carrier × Y), G, Y, y, g with ⟨gIn, fixed⟩579580end SubsetRestriction581