-- Restricting a group action to an invariant subset Y ⊆ X: the restricted
-- graph is an action of G on Y with the same values
-- 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.Action.Restrict
import Algebra.Group.Action

-- The action graph restricted to the pairs (g, y) with y ∈ Y.
def restrictAction (act G Y : Set) : Set := restrict(act, G.carrier × Y)

section Restriction
variable (act G X : Set)
hypothesis action : act : G ↷ X

theorem restrictAction.function (Y : Set)
  requires subset : Y ⊆ X
  requires invariant : ∀ g ∈ G.carrier, ∀ y ∈ Y, g ·ₐ y ∈ Y
  shows restrictAction(act, G, Y) : G.carrier × Y → Y
proof
  have function := Action.function with action
  have same := Subset.reflexive at G.carrier
  have pairs : G.carrier × Y ⊆ G.carrier × X :=
    product.monotone with same, subset
  have closed : ∀ p ∈ G.carrier × Y, act(p) ∈ Y
    intros p hp
    obtain ⟨bound, g, hg, y, hy, shape⟩ :=
      product.membership.forward with hp
    have moved := invariant with g, hg, y, hy
    rw shape
    unfold call2 at moved
    exact moved
  unfold restrictAction
  exact restrict.function with function, pairs, closed

-- The values of the restriction need no invariance of Y.
theorem restrictAction.value (Y g y : Set)
  requires subset : Y ⊆ X
  requires hg : g ∈ G.carrier
  requires hy : y ∈ Y
  shows call2(restrictAction(act, G, Y), g, y) = g ·ₐ y
proof
  have function := Action.function with action
  have same := Subset.reflexive at G.carrier
  have pairs : G.carrier × Y ⊆ G.carrier × X :=
    product.monotone with same, subset
  have pair := product.pair at g, y, G.carrier, Y with *
  have value := restrict.domain_apply at act, G.carrier × X, X,
    G.carrier × Y, (g, y) with function, pairs, pair
  simp [restrictAction, call2]

theorem restrictAction.apply (Y g y : Set)
  requires subset : Y ⊆ X
  requires invariant : ∀ g ∈ G.carrier, ∀ y ∈ Y, g ·ₐ y ∈ Y
  requires hg : g ∈ G.carrier
  requires hy : y ∈ Y
  shows call2(restrictAction(act, G, Y), g, y) = g ·ₐ y
proof
  exact restrictAction.value with action, subset, hg, hy

theorem restrictAction.action (Y : Set)
  requires subset : Y ⊆ X
  requires invariant : ∀ g ∈ G.carrier, ∀ y ∈ Y, g ·ₐ y ∈ Y
  shows restrictAction(act, G, Y) : G ↷ Y
proof
  have group := Action.group with action
  have function := restrictAction.function with action, subset, invariant
  apply Action.mk with group, function
  . intros y hy
    have unitIn : G.one ∈ G.carrier := Group.one_mem with group
    have yIn := subset with y, hy
    have value := restrictAction.apply with
      action, subset, invariant, unitIn, hy
    rw value
    exact one_act with action, yIn
  . intros g hg h hh y hy
    have yIn := subset with y, hy
    have productIn : g * h ∈ G.carrier := Group.mul_mem with group, hg, hh
    have moved := invariant with h, hh, y, hy
    have outer := restrictAction.apply with
      action, subset, invariant, productIn, hy
    have inner := restrictAction.apply with action, subset, invariant, hh, hy
    have composed := restrictAction.apply with
      action, subset, invariant, hg, moved
    rw [outer, inner, composed]
    exact mul_act with action, yIn

end Restriction