-- Translation: the action of a group on a family of its subsets by left
-- multiplication, a translate of a finite subset having its size, the
-- subsets of a given size and the cosets of a subgroup closed under
-- translation, the stabilizer of a subset no larger than the subset, and
-- the restriction of an action to a subgroup or to an invariant subset
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Group.Translation
import Conjugation
import Combinatorics.Basics

-- Left multiplication on a family F of subsets of G, as a graph on
-- (G.carrier × F) × F, and the families closed under it.
def translation (G F : Set) : Set :=
  { p ∈ (G.carrier × F) × F |
    ∃ g ∈ G.carrier, ∃ S ∈ F, p = ((g, S) ↦ leftCoset(G, g, S)) }

predicate TranslationClosed (G F : Set) :=
  ∀ g ∈ G.carrier, ∀ S ∈ F, leftCoset(G, g, S) ∈ F

theorem subsetsOfSize.subset_powerset (A k : Set)
  shows subsetsOfSize(A, k) ⊆ 𝒫(A)
proof
  intros S hS
  have parts := subsetsOfSize.membership.forward with hS
  exact parts.left

theorem subsetsOfSize.nonempty (A S : Set) (k : Nat)
  requires hS : S ∈ subsetsOfSize(A, k)
  requires nonzero : k ≠ 0
  shows Nonempty(S)
proof
  obtain ⟨bound, counted⟩ := subsetsOfSize.membership.forward with hS
  have shape := natural.zero_or_successor at k
  cases shape with zero | successor
  . exfalso
    exact nonzero with zero
  . obtain ⟨j, jNat, kEq⟩ := successor
    rw kEq at counted
    exact HasCardinality.exists_member with counted

section Translation
variable (G : Set)
hypothesis group : Group(G)

-- Translating a subset of G: the translate of s ∈ S by g is g * s, the
-- unit translates trivially, and translating twice translates by the
-- product.
theorem leftCoset.mul_mem_of_subset (g : G) (S s : Set)
  requires bounded : S ⊆ G
  requires hs : s ∈ S
  shows g * s ∈ g • S
proof
  have sIn := bounded with s, hs
  have product : g * s ∈ G by typecheck
  exact leftCoset.membership.backward with ⟨product, s, hs, rfl⟩

theorem leftCoset.one_of_subset (S : Set)
  requires bounded : S ⊆ G
  shows G.one • S = S
proof
  ext y
  constructor
  . intro hy
    obtain ⟨yIn, s, hs, yEq⟩ := leftCoset.membership.forward with hy
    have sIn := bounded with s, hs
    rw [yEq, one_mul]
    exact hs
  . intro hy
    have yIn := bounded with y, hy
    have identity : G.one * y = y := one_mul with *
    apply leftCoset.membership.backward
    refine ⟨yIn, y, hy, ?_⟩
    symm
    exact identity

theorem leftCoset.mul_of_subset (g h : G) (S : Set)
  requires bounded : S ⊆ G
  shows g • (h • S) = (g * h) • S
proof
  ext y
  constructor
  . intro hy
    obtain ⟨yIn, z, hz, yEq⟩ := leftCoset.membership.forward with hy
    obtain ⟨zIn, s, hs, zEq⟩ := leftCoset.membership.forward with hz
    have sIn := bounded with s, hs
    apply leftCoset.membership.backward
    refine ⟨yIn, s, hs, ?_⟩
    rw [yEq, zEq, mul_assoc]
    rfl
  . intro hy
    obtain ⟨yIn, s, hs, yEq⟩ := leftCoset.membership.forward with hy
    have sIn := bounded with s, hs
    have inner : h * s ∈ h • S := leftCoset.mul_mem_of_subset with *
    apply leftCoset.membership.backward
    refine ⟨yIn, h * s, inner, ?_⟩
    rw [yEq, mul_assoc]
    rfl

-- The translation graph is a function, and an action on a family closed
-- under translation.
theorem translation.relates (F g S : Set)
  requires closed : TranslationClosed(G, F)
  requires hg : g ∈ G
  requires hS : S ∈ F
  shows relates(translation(G, F), (g, S), g • S)
proof
  have moved := closed with g, hg, S, hS
  have input := product.pair at g, S, G.carrier, F with *
  have bounded := product.pair at (g, S), g • S, G.carrier × F, F with *
  unfold relates
  apply translation.membership.backward
  refine ⟨bounded, g, hg, S, hS, rfl⟩

theorem translation.function (F : Set)
  requires closed : TranslationClosed(G, F)
  shows translation(G, F) : G.carrier × F → F
proof
  unfold FunctionBetween
  refine ⟨?_, ?_, ?_⟩
  . intros p hp
    have parts := translation.membership.forward with hp
    exact parts.left
  . intros p y edge z edge2
    unfold relates at edge
    unfold relates at edge2
    obtain ⟨bounded, g, hg, S, hS, shape⟩ :=
      translation.membership.forward with edge
    obtain ⟨bounded2, g2, hg2, S2, hS2, shape2⟩ :=
      translation.membership.forward with edge2
    have outer := orderedPair.injective with shape
    have outer2 := orderedPair.injective with shape2
    have inputs : (g, S) = (g2, S2) by cc
    have halves := orderedPair.injective with inputs
    cc
  . intros p hp
    obtain ⟨bound, g, hg, S, hS, shape⟩ := product.membership.forward with hp
    have moved := closed with g, hg, S, hS
    have edge := translation.relates with closed, hg, hS
    refine ⟨g • S, moved, ?_⟩
    rw shape
    exact edge

theorem translation.value (F g S : Set)
  requires closed : TranslationClosed(G, F)
  requires hg : g ∈ G
  requires hS : S ∈ F
  shows translation(G, F)(g, S) = g • S
proof
  have function := translation.function with group, closed
  have edge := translation.relates with closed, hg, hS
  have input := product.pair at g, S, G.carrier, F with *
  have value := FunctionBetween.apply_value with function, input, edge
  unfold call2
  exact value

theorem translation.action (F : Set)
  requires bounded : F ⊆ 𝒫(G.carrier)
  requires closed : TranslationClosed(G, F)
  shows translation(G, F) : G ↷ F
proof
  have function := translation.function with group, closed
  apply Action.mk with group, function
  . intros S hS
    have subset := powerset.membership_iff.forward with (bounded with S, hS)
    have unitIn : G.one ∈ G := Group.one_mem with *
    have value := translation.value with closed, unitIn, hS
    rw value
    exact leftCoset.one_of_subset with *
  . intros g hg h hh S hS
    have subset := powerset.membership_iff.forward with (bounded with S, hS)
    have moved := closed with h, hh, S, hS
    have product : g * h ∈ G by typecheck
    have first := translation.value with closed, hh, hS
    have second := translation.value with closed, hg, moved
    have third := translation.value with closed, product, hS
    rw [third, first, second]
    symm
    exact leftCoset.mul_of_subset with *

end Translation

-- Translation by g carries a subset S of G onto g • S.
defgraph translateMap (G S g : Set) (s ∈ S) : leftCoset(G, g, S) := g * s
requires group : Group(G)
requires bounded : S ⊆ G.carrier
requires hg : g ∈ G.carrier
proof
  exact leftCoset.mul_mem_of_subset with *

section TranslateSize
variable (G : Set)
hypothesis group : Group(G)

theorem translateMap.injective (S : Set) (g : G)
  requires bounded : S ⊆ G
  shows InjectiveBetween(translateMap(G, S, g), S, g • S)
proof
  have function := translateMap.function at G, S, g with *
  constructor
  . exact function
  . intros x hx y hy z hz hxz hyz
    have xValue := FunctionBetween.apply_value with function, hx, hxz
    have yValue := FunctionBetween.apply_value with function, hy, hyz
    have xImage := translateMap.value at G, S, g, x with *
    have yImage := translateMap.value at G, S, g, y with *
    have xIn := bounded with x, hx
    have yIn := bounded with y, hy
    have equal : g * x = g * y by cc
    exact mul_left_cancel with *

theorem translateMap.surjective (S : Set) (g : G)
  requires bounded : S ⊆ G
  shows SurjectiveBetween(translateMap(G, S, g), S, g • S)
proof
  have function := translateMap.function at G, S, g with *
  constructor
  . exact function
  . intros y hy
    obtain ⟨yIn, s, hs, yEq⟩ := leftCoset.membership.forward with hy
    have image := translateMap.value at G, S, g, s with *
    have related := FunctionBetween.relates_apply with function, hs
    witness s
    constructor
    . exact hs
    . rw [image, ← yEq] at related
      exact related

theorem leftCoset.cardinality_of_subset (S : Set) (g : G)
  requires bounded : S ⊆ G
  requires finite : Finite(S)
  shows cardinality(g • S) = cardinality(S)
proof
  have bijective : BijectiveBetween(translateMap(G, S, g), S, g • S)
    constructor
    . exact translateMap.injective with *
    . exact translateMap.surjective with *
  symm
  exact cardinality.bijective with finite, bijective

-- The subsets of a given size are closed under translation, so G acts on
-- them.
theorem subsetsOfSize.translation_closed (n : Nat)
  requires finite : Finite(G)
  shows TranslationClosed(G, subsetsOfSize(G.carrier, n))
proof
  intros g hg S hS
  obtain ⟨bound, counted⟩ := subsetsOfSize.membership.forward with hS
  have bounded := powerset.membership_iff.forward with bound
  have finiteS := Finite.subset with finite, bounded
  have same : cardinality(g • S) = cardinality(S) :=
    leftCoset.cardinality_of_subset with *
  have count := cardinality.eq_of_has with counted
  have translateSubset := leftCoset.subset at G, g, S
  have finiteTranslate := Finite.subset with finite, translateSubset
  have correct := cardinality.correct with finiteTranslate
  rw [same, count] at correct
  have translateBound := powerset.membership_iff.backward with translateSubset
  exact subsetsOfSize.membership.backward with ⟨translateBound, correct⟩

theorem subsetsOfSize.action (n : Nat)
  requires finite : Finite(G)
  shows translation(G, subsetsOfSize(G.carrier, n)) : G ↷ subsetsOfSize(G.carrier, n)
proof
  have bounded := subsetsOfSize.subset_powerset at G.carrier, n
  have closed := subsetsOfSize.translation_closed with *
  exact translation.action with *

-- The cosets of a subgroup are closed under translation, so G acts on
-- them.
theorem leftCosets.translation_closed (H : Set)
  requires subgroup : Subgroup(H, G)
  shows TranslationClosed(G, leftCosets(G, H))
proof
  intros g hg C hC
  obtain ⟨bound, h, hh, CEq⟩ := leftCosets.membership.forward with hC
  have bounded := Subgroup.subset with subgroup
  have merged : g • (h • H) = (g * h) • H := leftCoset.mul_of_subset with *
  rw [CEq, merged]
  exact leftCosets.coset_member with (Group.mul_mem with *)

theorem leftCosets.action (H : Set)
  requires subgroup : Subgroup(H, G)
  shows translation(G, leftCosets(G, H)) : G ↷ leftCosets(G, H)
proof
  have bounded := leftCosets.subset_powerset at G, H
  have closed := leftCosets.translation_closed with *
  exact translation.action with *

end TranslateSize

-- Right multiplication by s as a function on the carrier.
defgraph rightTranslate (G s : Set) (x ∈ G.carrier) : G.carrier := x * s
requires group : Group(G)
requires hs : s ∈ G.carrier
proof
  exact Group.mul_mem with *

section StabilizerBound
variable (G : Set)
hypothesis group : Group(G)

theorem rightTranslate.injective (s : G)
  shows InjectiveBetween(rightTranslate(G, s), G.carrier, G.carrier)
proof
  have function := rightTranslate.function at G, s with *
  constructor
  . exact function
  . intros x hx y hy z hz hxz hyz
    have xValue := FunctionBetween.apply_value with function, hx, hxz
    have yValue := FunctionBetween.apply_value with function, hy, hyz
    have xImage := rightTranslate.value at G, s, x with *
    have yImage := rightTranslate.value at G, s, y with *
    have equal : x * s = y * s by cc
    exact mul_right_cancel with *

-- The stabilizer of a nonempty subset S under translation is carried
-- injectively into S by right multiplication with a member of S, so it is
-- no larger than S.
theorem translation.stabilizer_card_le (F S : Set)
  requires bounded : F ⊆ 𝒫(G.carrier)
  requires closed : TranslationClosed(G, F)
  requires finite : Finite(G)
  requires hS : S ∈ F
  requires inhabited : Nonempty(S)
  shows cardinality(stabilizer(translation(G, F), G, F, S)) ≤ cardinality(S)
proof
  have action := translation.action with group, bounded, closed
  have subsetS := powerset.membership_iff.forward with (bounded with S, hS)
  have finiteS := Finite.subset with finite, subsetS
  obtain ⟨s, hs⟩ := inhabited
  have sIn := subsetS with s, hs
  have injective := rightTranslate.injective with group, sIn
  have stabilizerSubset := stabilizer.subset at translation(G, F), G, F, S
  have finiteStabilizer := Finite.subset with finite, stabilizerSubset
  have imageCount := cardinality.injective_image with
    injective, stabilizerSubset, finiteStabilizer
  have imageSubset : functionImage(rightTranslate(G, s), stabilizer(translation(G, F), G, F, S), G.carrier) ⊆ S
    intros y hy
    obtain ⟨yIn, h, hh, yEq⟩ := functionImage.membership.forward with hy
    have hIn := stabilizerSubset with h, hh
    have fixed : h ·ₐ S = S := stabilizer.fixes with *
    have value := translation.value with closed, hIn, hS
    have translated : h • S = S by cc
    have image := rightTranslate.value at G, s, h with *
    have member : h * s ∈ h • S := leftCoset.mul_mem_of_subset with *
    rw [yEq, image, ← translated]
    exact member
  have bound := cardinality.monotone with finiteS, imageSubset
  rwa imageCount at bound

end StabilizerBound

-- The restriction of an action to a subgroup is an action of the group on
-- the subgroup.
section Restriction
variable (act G X H : Set)
hypothesis action : act : G ↷ X
hypothesis subgroup : Subgroup(H, G)

theorem Action.restrict_function
  shows restrict(act, H × X) : H × X → X
proof
  have function := Action.function with action
  have subset : H × X ⊆ G.carrier × X
    intros p hp
    obtain ⟨bound, h, hh, x, hx, shape⟩ := product.membership.forward with hp
    have hIn : h ∈ G := Subgroup.mem_carrier with *
    rw shape
    exact product.pair with hIn, hx
  exact restrict.domain_function with function, subset

theorem Action.restrict_value (h : H) (x : Set)
  requires hx : x ∈ X
  shows restrict(act, H × X)(h, x) = h ·ₐ x
proof
  have function := Action.function with action
  have hIn : h ∈ G := Subgroup.mem_carrier with *
  have subset : H × X ⊆ G.carrier × X
    intros p hp
    obtain ⟨bound, k, hk, y, hy, shape⟩ := product.membership.forward with hp
    have kIn : k ∈ G := Subgroup.mem_carrier with *
    rw shape
    exact product.pair with kIn, hy
  have pair := product.pair at h, x, H, X with *
  have value := restrict.domain_apply with function, subset, pair
  unfold call2
  exact value

theorem Action.restrict
  shows restrict(act, H × X) : subgroupGroup(G, H) ↷ X
proof
  have group := Action.group with action
  have subgroupGroupIs := subgroupGroup.group with group, subgroup
  have function := Action.restrict_function with action, subgroup
  have carrierFunction : restrict(act, H × X) : Group.carrier(subgroupGroup(G, H)) × X → X
    rw subgroupGroup.carrierOf
    exact function
  apply Action.mk with subgroupGroupIs, carrierFunction
  . intros x hx
    have unitIn : G.one ∈ H := Subgroup.one_mem with *
    have value := Action.restrict_value with action, subgroup, unitIn, hx
    have fixed : G.one ·ₐ x = x := one_act with *
    rw [subgroupGroup.unit, value]
    exact fixed
  . intros g hg h hh x hx
    rw subgroupGroup.carrierOf at hg
    rw subgroupGroup.carrierOf at hh
    have gIn : g ∈ G := Subgroup.mem_carrier with *
    have hIn : h ∈ G := Subgroup.mem_carrier with *
    have product : G.mul(g, h) ∈ H := Subgroup.mul_mem with *
    have moved : h ·ₐ x ∈ X := Action.act_mem with *
    have restricted : Group.mul(subgroupGroup(G, H))(g, h) = G.mul(g, h) :=
      subgroupGroup.mul with *
    have first := Action.restrict_value with action, subgroup, hh, hx
    have second := Action.restrict_value with action, subgroup, hg, moved
    have third := Action.restrict_value with action, subgroup, product, hx
    have merged : G.mul(g, h) ·ₐ x = g ·ₐ h ·ₐ x := mul_act with *
    rw [restricted, third, first, second]
    exact merged

-- The fixed points of the restricted action are the points fixed by the
-- subgroup.
theorem Action.restrict_fixed_points (x : Set)
  shows x ∈ fixedPoints(restrict(act, H × X), subgroupGroup(G, H), X) ↔
    x ∈ X ∧ ∀ h ∈ H, h ·ₐ x = x
proof
  have criterion := fixedPoints.membership at
    restrict(act, H × X), subgroupGroup(G, H), X, x
  rw under subgroupGroup.carrierOf at criterion
  constructor
  . intro fixed
    obtain ⟨xIn, fixes⟩ := criterion.forward with fixed
    refine ⟨xIn, ?_⟩
    intros h hh
    have value := Action.restrict_value with action, subgroup, hh, xIn
    have restricted := fixes with h, hh
    rwa value at restricted
  . intro fixes
    obtain ⟨xIn, fixesH⟩ := fixes
    apply criterion.backward
    refine ⟨xIn, ?_⟩
    intros h hh
    have value := Action.restrict_value with action, subgroup, hh, xIn
    rw value
    exact fixesH with h, hh

end Restriction

-- The restriction of an action to a subset closed under it.
section SubsetRestriction
variable (act G X Y : Set)
hypothesis action : act : G ↷ X
hypothesis bounded : Y ⊆ X
hypothesis closed : ∀ g ∈ G.carrier, ∀ y ∈ Y, act(g, y) ∈ Y

theorem Action.restrict_subset_value (g : G) (y : Set)
  requires hy : y ∈ Y
  shows restrict(act, G.carrier × Y)(g, y) = g ·ₐ y
proof
  have function := Action.function with action
  have subset : G.carrier × Y ⊆ G.carrier × X
    intros p hp
    obtain ⟨bound, k, hk, z, hz, shape⟩ := product.membership.forward with hp
    rw shape
    exact product.pair with hk, (bounded with z, hz)
  have pair := product.pair at g, y, G.carrier, Y with *
  have value := restrict.domain_apply with function, subset, pair
  unfold call2
  exact value

theorem Action.restrict_subset
  shows restrict(act, G.carrier × Y) : G ↷ Y
proof
  have group := Action.group with action
  have function := Action.function with action
  have subset : G.carrier × Y ⊆ G.carrier × X
    intros p hp
    obtain ⟨bound, k, hk, z, hz, shape⟩ := product.membership.forward with hp
    rw shape
    exact product.pair with hk, (bounded with z, hz)
  have restricted := restrict.domain_function with function, subset
  have corestricted : restrict(act, G.carrier × Y) : G.carrier × Y → Y
    apply FunctionBetween.codomain_of_values with restricted
    intros p hp
    obtain ⟨bound, k, hk, z, hz, shape⟩ := product.membership.forward with hp
    have value := Action.restrict_subset_value with action, bounded, closed, hk, hz
    rw shape
    unfold call2 at value
    rw value
    have inside := closed with k, hk, z, hz
    unfold call2 at inside
    exact inside
  apply Action.mk with group, corestricted
  . intros y hy
    have yIn := bounded with y, hy
    have unitIn : G.one ∈ G := Group.one_mem with *
    have value := Action.restrict_subset_value with action, bounded, closed, unitIn, hy
    have fixed : G.one ·ₐ y = y := one_act with *
    rw value
    exact fixed
  . intros g hg h hh y hy
    have yIn := bounded with y, hy
    have moved := closed with h, hh, y, hy
    have product : g * h ∈ G by typecheck
    have first := Action.restrict_subset_value with action, bounded, closed, hh, hy
    have second := Action.restrict_subset_value with action, bounded, closed, hg, moved
    have third := Action.restrict_subset_value with action, bounded, closed, product, hy
    have merged : (g * h) ·ₐ y = g ·ₐ h ·ₐ y := mul_act with *
    rw [third, first, second]
    exact merged

theorem Action.restrict_subset_fixed_points (y : Set)
  shows y ∈ fixedPoints(restrict(act, G.carrier × Y), G, Y) ↔
    y ∈ Y ∧ ∀ g ∈ G.carrier, g ·ₐ y = y
proof
  have criterion := fixedPoints.membership at restrict(act, G.carrier × Y), G, Y, y
  constructor
  . intro fixed
    obtain ⟨yIn, fixes⟩ := criterion.forward with fixed
    refine ⟨yIn, ?_⟩
    intros g hg
    have value := Action.restrict_subset_value with action, bounded, closed, hg, yIn
    have restricted := fixes with g, hg
    rwa value at restricted
  . intro fixes
    obtain ⟨yIn, fixesAll⟩ := fixes
    apply criterion.backward
    refine ⟨yIn, ?_⟩
    intros g hg
    have value := Action.restrict_subset_value with action, bounded, closed, hg, yIn
    rw value
    exact fixesAll with g, hg

theorem Action.restrict_subset_orbit (y : Set)
  requires hy : y ∈ Y
  shows orbit(restrict(act, G.carrier × Y), G, Y, y) = orbit(y)
proof
  have yIn := bounded with y, hy
  ext z
  constructor
  . intro hz
    obtain ⟨zIn, g, hg, zEq⟩ := orbit.membership.forward with hz
    have value := Action.restrict_subset_value with action, bounded, closed, hg, hy
    have moved : g ·ₐ y ∈ orbit(y) := orbit.act_mem with *
    rw [zEq, value]
    exact moved
  . intro hz
    obtain ⟨zIn, g, hg, zEq⟩ := orbit.membership.forward with hz
    have value := Action.restrict_subset_value with action, bounded, closed, hg, hy
    have moved := closed with g, hg, y, hy
    apply orbit.membership.backward
    refine ⟨?_, g, hg, ?_⟩
    . rw zEq
      exact moved
    . rw [zEq, value]
      rfl

theorem Action.restrict_subset_stabilizer (y : Set)
  requires hy : y ∈ Y
  shows stabilizer(restrict(act, G.carrier × Y), G, Y, y) = stabilizer(y)
proof
  ext g
  constructor
  . intro hg
    obtain ⟨gIn, fixed⟩ := stabilizer.membership.forward with hg
    have value := Action.restrict_subset_value with action, bounded, closed, gIn, hy
    rw value at fixed
    exact stabilizer.membership.backward with ⟨gIn, fixed⟩
  . intro hg
    obtain ⟨gIn, fixed⟩ := stabilizer.membership.forward with hg
    have value := Action.restrict_subset_value with action, bounded, closed, gIn, hy
    rw ← value at fixed
    exact stabilizer.membership.backward at
      restrict(act, G.carrier × Y), G, Y, y, g with ⟨gIn, fixed⟩

end SubsetRestriction