Grace/Cumulus/Geometry/Sphere/Conjugate.g17

Open in Workbench Download source

Imports

Geometry.Absorption.Pieces

Declarations

Source

1-- Images of sets and powers under a group action commute with2-- conjugation, in general and for SO3 acting on the sphere3-- 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.Geometry.Sphere.Conjugate9import Geometry.Absorption.Pieces1011section Images12variable (act G X : Set)13hypothesis action : act : G ↷ X1415theorem actImage.mul (g h : G) (D : Set)16  requires subset : D ⊆ X17  shows actImage(act, g * h, D) = actImage(act, g, actImage(act, h, D))18proof19  have group := Action.group with action20  have inner := actImage.subset at act, G, X, h, D with action, subset21  have merged := translate.mul at act, G, X, g, h, D with action, subset22  have outer := actImage.eq_translate at act, G, X, g * h, D with action, subset23  have first := actImage.eq_translate at act, G, X, h, D with action, subset24  have second := actImage.eq_translate at act, G, X, g, actImage(act, h, D)25    with action, inner26  rw [← outer, ← second, ← first]27  exact merged2829theorem actImage.inv_image (g : G) (D : Set)30  requires subset : D ⊆ X31  shows actImage(act, g⁻¹, actImage(act, g, D)) = D32proof33  have group := Action.group with action34  have inner := actImage.subset at act, G, X, g, D with action, subset35  have cancel := translate.inv_translate at act, G, X, g, D with action, subset36  have first := actImage.eq_translate at act, G, X, g, D with action, subset37  have second := actImage.eq_translate at act, G, X, g⁻¹, actImage(act, g, D)38    with action, inner39  rw [← second, ← first]40  exact cancel4142theorem actImage.disjoint (g : G) (A B : Set)43  requires subsetA : A ⊆ X44  requires subsetB : B ⊆ X45  requires disjoint : Disjoint(A, B)46  shows Disjoint(actImage(act, g, A), actImage(act, g, B))47proof48  have moved := translate.disjoint at act, G, X, g, A, B49    with action, subsetA, subsetB, disjoint50  have first := actImage.eq_translate at act, G, X, g, A with action, subsetA51  have second := actImage.eq_translate at act, G, X, g, B with action, subsetB52  rw [← first, ← second]53  exact moved5455theorem actImage.conjugation (g x : G) (D : Set)56  requires subset : D ⊆ X57  shows actImage(act, g⁻¹ * x * g, D) =58    actImage(act, g⁻¹, actImage(act, x, actImage(act, g, D)))59proof60  have group := Action.group with action61  have inverse : g⁻¹ ∈ G.carrier := Group.inv_mem with group62  have product : g⁻¹ * x ∈ G.carrier := Group.mul_mem with group63  have inner := actImage.subset at act, G, X, g, D with action, subset64  have first := actImage.mul at act, G, X, g⁻¹ * x, g, D with action, subset65  have second := actImage.mul at act, G, X, g⁻¹, x, actImage(act, g, D)66    with action, inner67  rw [first, second]68  rfl6970end Images7172section Powers73variable (G : Set)74hypothesis group : Group(G)7576theorem pow.conjugation (g x : G) (n : Nat)77  shows (g⁻¹ * x * g) ^ n = g⁻¹ * x ^ n * g78proof79  induction n80  | zero =>81    have inverse : g⁻¹ ∈ G.carrier := Group.inv_mem with group82    have product : g⁻¹ * x ∈ G.carrier := Group.mul_mem with group83    have conjugate : g⁻¹ * x * g ∈ G.carrier := Group.mul_mem with group84    have left := pow_zero at G, g⁻¹ * x * g with group85    have right := pow_zero at G, x with group86    have unit := mul_one at G, g⁻¹ with group87    have cancel := Group.inv_mul at G, g with group88    rw [left, right, unit, cancel]89    rfl90  | k + 1 using ih =>91    have inverse : g⁻¹ ∈ G.carrier := Group.inv_mem with group92    have product : g⁻¹ * x ∈ G.carrier := Group.mul_mem with group93    have conjugate : g⁻¹ * x * g ∈ G.carrier := Group.mul_mem with group94    have power : x ^ k ∈ G.carrier := Group.pow_mem with group95    have powerG : x ^ k * g ∈ G.carrier := Group.mul_mem with group96    have left := pow_succ_left at G, g⁻¹ * x * g, k with group97    have right := pow_succ_left at G, x, k with group98    rw [left, right, ih]99    have assoc1 := mul_assoc at G, g⁻¹ * x, g, g⁻¹ * x ^ k * g with group100    have assoc2 := mul_assoc at G, g⁻¹, x ^ k, g with group101    have cancel := mul_inv_cancel_left at G, g, x ^ k * g with group102    have assoc3 := mul_assoc at G, g⁻¹, x, x ^ k * g with group103    have assoc4 := mul_assoc at G, x, x ^ k, g with group104    have assoc5 := mul_assoc at G, g⁻¹, x * x ^ k, g with group105    rw [assoc1, assoc2, cancel, assoc3, ← assoc4, ← assoc5]106    rfl107108end Powers109110-- Conjugation in SO3 acting on the sphere: the image of D ⊆ S² under111-- σ⁻¹ ρ σ, and the powers of a conjugate.112theorem actImage.conjugate (σ ρ D : Set)113  requires hσ : σ ∈ so3Matrices114  requires hρ : ρ ∈ so3Matrices115  requires subset : D ⊆ S²116  shows actImage(sphereAction, SO3.mul(SO3.mul(SO3.inv(σ), ρ), σ), D) =117    actImage(sphereAction, SO3.inv(σ),118      actImage(sphereAction, ρ, actImage(sphereAction, σ, D)))119proof120  have action := sphereAction.action121  have σIn : σ ∈ Group.carrier(SO3)122    rw SO3.carrierOf123    exact hσ124  have ρIn : ρ ∈ Group.carrier(SO3)125    rw SO3.carrierOf126    exact hρ127  exact actImage.conjugation at sphereAction, SO3, S², σ, ρ, D128    with action, subset129130theorem so3.pow_conjugate (σ ρ : Set) (n : Nat)131  requires hσ : σ ∈ so3Matrices132  requires hρ : ρ ∈ so3Matrices133  shows groupPow(SO3, SO3.mul(SO3.mul(SO3.inv(σ), ρ), σ), n) =134    SO3.mul(SO3.mul(SO3.inv(σ), groupPow(SO3, ρ, n)), σ)135proof136  have group := SO3.group137  have σIn : σ ∈ Group.carrier(SO3)138    rw SO3.carrierOf139    exact hσ140  have ρIn : ρ ∈ Group.carrier(SO3)141    rw SO3.carrierOf142    exact hρ143  exact pow.conjugation at SO3, σ, ρ, n with group144