-- Images of sets and powers under a group action commute with
-- conjugation, in general and for SO3 acting on the sphere
-- 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.Geometry.Sphere.Conjugate
import Geometry.Absorption.Pieces

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

theorem actImage.mul (g h : G) (D : Set)
  requires subset : D ⊆ X
  shows actImage(act, g * h, D) = actImage(act, g, actImage(act, h, D))
proof
  have group := Action.group with action
  have inner := actImage.subset at act, G, X, h, D with action, subset
  have merged := translate.mul at act, G, X, g, h, D with action, subset
  have outer := actImage.eq_translate at act, G, X, g * h, D with action, subset
  have first := actImage.eq_translate at act, G, X, h, D with action, subset
  have second := actImage.eq_translate at act, G, X, g, actImage(act, h, D)
    with action, inner
  rw [← outer, ← second, ← first]
  exact merged

theorem actImage.inv_image (g : G) (D : Set)
  requires subset : D ⊆ X
  shows actImage(act, g⁻¹, actImage(act, g, D)) = D
proof
  have group := Action.group with action
  have inner := actImage.subset at act, G, X, g, D with action, subset
  have cancel := translate.inv_translate at act, G, X, g, D with action, subset
  have first := actImage.eq_translate at act, G, X, g, D with action, subset
  have second := actImage.eq_translate at act, G, X, g⁻¹, actImage(act, g, D)
    with action, inner
  rw [← second, ← first]
  exact cancel

theorem actImage.disjoint (g : G) (A B : Set)
  requires subsetA : A ⊆ X
  requires subsetB : B ⊆ X
  requires disjoint : Disjoint(A, B)
  shows Disjoint(actImage(act, g, A), actImage(act, g, B))
proof
  have moved := translate.disjoint at act, G, X, g, A, B
    with action, subsetA, subsetB, disjoint
  have first := actImage.eq_translate at act, G, X, g, A with action, subsetA
  have second := actImage.eq_translate at act, G, X, g, B with action, subsetB
  rw [← first, ← second]
  exact moved

theorem actImage.conjugation (g x : G) (D : Set)
  requires subset : D ⊆ X
  shows actImage(act, g⁻¹ * x * g, D) =
    actImage(act, g⁻¹, actImage(act, x, actImage(act, g, D)))
proof
  have group := Action.group with action
  have inverse : g⁻¹ ∈ G.carrier := Group.inv_mem with group
  have product : g⁻¹ * x ∈ G.carrier := Group.mul_mem with group
  have inner := actImage.subset at act, G, X, g, D with action, subset
  have first := actImage.mul at act, G, X, g⁻¹ * x, g, D with action, subset
  have second := actImage.mul at act, G, X, g⁻¹, x, actImage(act, g, D)
    with action, inner
  rw [first, second]
  rfl

end Images

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

theorem pow.conjugation (g x : G) (n : Nat)
  shows (g⁻¹ * x * g) ^ n = g⁻¹ * x ^ n * g
proof
  induction n
  | zero =>
    have inverse : g⁻¹ ∈ G.carrier := Group.inv_mem with group
    have product : g⁻¹ * x ∈ G.carrier := Group.mul_mem with group
    have conjugate : g⁻¹ * x * g ∈ G.carrier := Group.mul_mem with group
    have left := pow_zero at G, g⁻¹ * x * g with group
    have right := pow_zero at G, x with group
    have unit := mul_one at G, g⁻¹ with group
    have cancel := Group.inv_mul at G, g with group
    rw [left, right, unit, cancel]
    rfl
  | k + 1 using ih =>
    have inverse : g⁻¹ ∈ G.carrier := Group.inv_mem with group
    have product : g⁻¹ * x ∈ G.carrier := Group.mul_mem with group
    have conjugate : g⁻¹ * x * g ∈ G.carrier := Group.mul_mem with group
    have power : x ^ k ∈ G.carrier := Group.pow_mem with group
    have powerG : x ^ k * g ∈ G.carrier := Group.mul_mem with group
    have left := pow_succ_left at G, g⁻¹ * x * g, k with group
    have right := pow_succ_left at G, x, k with group
    rw [left, right, ih]
    have assoc1 := mul_assoc at G, g⁻¹ * x, g, g⁻¹ * x ^ k * g with group
    have assoc2 := mul_assoc at G, g⁻¹, x ^ k, g with group
    have cancel := mul_inv_cancel_left at G, g, x ^ k * g with group
    have assoc3 := mul_assoc at G, g⁻¹, x, x ^ k * g with group
    have assoc4 := mul_assoc at G, x, x ^ k, g with group
    have assoc5 := mul_assoc at G, g⁻¹, x * x ^ k, g with group
    rw [assoc1, assoc2, cancel, assoc3, ← assoc4, ← assoc5]
    rfl

end Powers

-- Conjugation in SO3 acting on the sphere: the image of D ⊆ S² under
-- σ⁻¹ ρ σ, and the powers of a conjugate.
theorem actImage.conjugate (σ ρ D : Set)
  requires hσ : σ ∈ so3Matrices
  requires hρ : ρ ∈ so3Matrices
  requires subset : D ⊆ S²
  shows actImage(sphereAction, SO3.mul(SO3.mul(SO3.inv(σ), ρ), σ), D) =
    actImage(sphereAction, SO3.inv(σ),
      actImage(sphereAction, ρ, actImage(sphereAction, σ, D)))
proof
  have action := sphereAction.action
  have σIn : σ ∈ Group.carrier(SO3)
    rw SO3.carrierOf
    exact hσ
  have ρIn : ρ ∈ Group.carrier(SO3)
    rw SO3.carrierOf
    exact hρ
  exact actImage.conjugation at sphereAction, SO3, S², σ, ρ, D
    with action, subset

theorem so3.pow_conjugate (σ ρ : Set) (n : Nat)
  requires hσ : σ ∈ so3Matrices
  requires hρ : ρ ∈ so3Matrices
  shows groupPow(SO3, SO3.mul(SO3.mul(SO3.inv(σ), ρ), σ), n) =
    SO3.mul(SO3.mul(SO3.inv(σ), groupPow(SO3, ρ, n)), σ)
proof
  have group := SO3.group
  have σIn : σ ∈ Group.carrier(SO3)
    rw SO3.carrierOf
    exact hσ
  have ρIn : ρ ∈ Group.carrier(SO3)
    rw SO3.carrierOf
    exact hρ
  exact pow.conjugation at SO3, σ, ρ, n with group