Grace/Cumulus/Algebra/Group/Action/Restrict.g17

Open in Workbench Download source

Imports

Algebra.Group.Action

Declarations

• restrictAction def
• restrictAction.function theorem derivation
• restrictAction.value theorem derivation
• restrictAction.apply theorem derivation
• restrictAction.action theorem derivation

Source

1-- Restricting a group action to an invariant subset Y ⊆ X: the restricted2-- graph is an action of G on Y with the same values3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.Group.Action.Restrict9import Algebra.Group.Action1011-- The action graph restricted to the pairs (g, y) with y ∈ Y.12def restrictAction (act G Y : Set) : Set := restrict(act, G.carrier × Y)1314section Restriction15variable (act G X : Set)16hypothesis action : act : G ↷ X1718theorem restrictAction.function (Y : Set)19  requires subset : Y ⊆ X20  requires invariant : ∀ g ∈ G.carrier, ∀ y ∈ Y, g ·ₐ y ∈ Y21  shows restrictAction(act, G, Y) : G.carrier × Y → Y22proof23  have function := Action.function with action24  have same := Subset.reflexive at G.carrier25  have pairs : G.carrier × Y ⊆ G.carrier × X :=26    product.monotone with same, subset27  have closed : ∀ p ∈ G.carrier × Y, act(p) ∈ Y28    intros p hp29    obtain ⟨bound, g, hg, y, hy, shape⟩ :=30      product.membership.forward with hp31    have moved := invariant with g, hg, y, hy32    rw shape33    unfold call2 at moved34    exact moved35  unfold restrictAction36  exact restrict.function with function, pairs, closed3738-- The values of the restriction need no invariance of Y.39theorem restrictAction.value (Y g y : Set)40  requires subset : Y ⊆ X41  requires hg : g ∈ G.carrier42  requires hy : y ∈ Y43  shows call2(restrictAction(act, G, Y), g, y) = g ·ₐ y44proof45  have function := Action.function with action46  have same := Subset.reflexive at G.carrier47  have pairs : G.carrier × Y ⊆ G.carrier × X :=48    product.monotone with same, subset49  have pair := product.pair at g, y, G.carrier, Y with *50  have value := restrict.domain_apply at act, G.carrier × X, X,51    G.carrier × Y, (g, y) with function, pairs, pair52  simp [restrictAction, call2]5354theorem restrictAction.apply (Y g y : Set)55  requires subset : Y ⊆ X56  requires invariant : ∀ g ∈ G.carrier, ∀ y ∈ Y, g ·ₐ y ∈ Y57  requires hg : g ∈ G.carrier58  requires hy : y ∈ Y59  shows call2(restrictAction(act, G, Y), g, y) = g ·ₐ y60proof61  exact restrictAction.value with action, subset, hg, hy6263theorem restrictAction.action (Y : Set)64  requires subset : Y ⊆ X65  requires invariant : ∀ g ∈ G.carrier, ∀ y ∈ Y, g ·ₐ y ∈ Y66  shows restrictAction(act, G, Y) : G ↷ Y67proof68  have group := Action.group with action69  have function := restrictAction.function with action, subset, invariant70  apply Action.mk with group, function71  . intros y hy72    have unitIn : G.one ∈ G.carrier := Group.one_mem with group73    have yIn := subset with y, hy74    have value := restrictAction.apply with75      action, subset, invariant, unitIn, hy76    rw value77    exact one_act with action, yIn78  . intros g hg h hh y hy79    have yIn := subset with y, hy80    have productIn : g * h ∈ G.carrier := Group.mul_mem with group, hg, hh81    have moved := invariant with h, hh, y, hy82    have outer := restrictAction.apply with83      action, subset, invariant, productIn, hy84    have inner := restrictAction.apply with action, subset, invariant, hh, hy85    have composed := restrictAction.apply with86      action, subset, invariant, hg, moved87    rw [outer, inner, composed]88    exact mul_act with action, yIn8990end Restriction91