Theme/Equivariant.lean — FrcCore

1import FrcCore.Nat2import FrcCore.Shell34/-!5# The logic theme — equivariant choice: a section exists iff every stabiliser has a fixed point675-reductio's Theorem equivariant-choice (5:E3), the Fraenkel–Mostowski mechanism in positive form, on the kernel alone8(21 October 2026): a group as a structure with its four laws, actions on an index type and on a fibre type, an9equivariant family `π : A → I`. On one orbit (a transitivity datum `tr i • i₀ = i`) an equivariant section exists10exactly when the stabiliser of the base point fixes a point of its fibre; over finitely many orbits, exactly when11every orbit's representative does. The hard direction defines the section by transport, `s i = tr i • a`, and shows12it well defined through the stabiliser. The paper's obstruction (5:E4): on the line over `𝔽₅` the map `v ↦ −v`13fixes no basis vector, over `𝔽₂` it fixes `1`. No Mathlib, no axioms.14-/1516namespace FRC.Equivariant1718/-- A group: carrier `G`, the operation, the unit, the inverse, the laws. -/19structure Group (G : Type) where20  mul : G → G → G21  one : G22  inv : G → G23  mul_assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)24  one_mul : ∀ a, mul one a = a25  mul_one : ∀ a, mul a one = a26  inv_mul : ∀ a, mul (inv a) a = one27  mul_inv : ∀ a, mul a (inv a) = one2829/-- An action of the group on `X`. -/30structure Action {G : Type} (Γ : Group G) (X : Type) where31  act : G → X → X32  one_act : ∀ x, act Γ.one x = x33  mul_act : ∀ g h x, act (Γ.mul g h) x = act g (act h x)3435variable {G I A : Type} {Γ : Group G}3637/-- The family `π : A → I` is equivariant: `π (g • a) = g • π a`. -/38def Equivariant (ρI : Action Γ I) (ρA : Action Γ A) (π : A → I) : Prop :=39  ∀ g a, π (ρA.act g a) = ρI.act g (π a)4041/-- `s` is a section of `π`. -/42def IsSection (π : A → I) (s : I → A) : Prop := ∀ i, π (s i) = i4344/-- `s : I → A` is an equivariant map: `s (g • i) = g • s i`. -/45def EquivariantMap (ρI : Action Γ I) (ρA : Action Γ A) (s : I → A) : Prop :=46  ∀ g i, s (ρI.act g i) = ρA.act g (s i)4748/-- `g` lies in the stabiliser of `i₀`. -/49def Stab (ρI : Action Γ I) (i₀ : I) (g : G) : Prop := ρI.act g i₀ = i₀5051/-- 5:E3 (Theorem equivariant-choice, ⇒) — an equivariant section picks, at every point `i₀`, a point of the fibre52fixed by the stabiliser of `i₀`: `g • i₀ = i₀` gives `g • s i₀ = s (g • i₀) = s i₀`. -/53theorem fixed_point_of_section (ρI : Action Γ I) (ρA : Action Γ A) (π : A → I) (s : I → A)54    (hs : IsSection π s) (he : EquivariantMap ρI ρA s) (i₀ : I) :55    π (s i₀) = i₀ ∧ ∀ g, Stab ρI i₀ g → ρA.act g (s i₀) = s i₀ :=56  ⟨hs i₀, fun g hg => by rw [← he g i₀]; exact congrArg s hg⟩5758theorem Group.inv_mul_cancel_left (Γ : Group G) (a b : G) : Γ.mul a (Γ.mul (Γ.inv a) b) = b := by59  rw [← Γ.mul_assoc, Γ.mul_inv, Γ.one_mul]6061/-- The transport datum undone: `tr j⁻¹ • j = i₀`. -/62theorem act_inv_tr (ρI : Action Γ I) (i₀ : I) (tr : I → G) (htr : ∀ i, ρI.act (tr i) i₀ = i) (j : I) :63    ρI.act (Γ.inv (tr j)) j = i₀ :=64  calc ρI.act (Γ.inv (tr j)) j = ρI.act (Γ.inv (tr j)) (ρI.act (tr j) i₀) := by rw [htr j]65    _ = i₀ := by rw [← ρI.mul_act, Γ.inv_mul, ρI.one_act]6667/-- 5:E3 (Theorem equivariant-choice, ⇐, one orbit) — on a transitive index set, given the transport datum68`tr i • i₀ = i`, a point `a` of the fibre over `i₀` fixed by the stabiliser of `i₀` yields the equivariant section69`s i = tr i • a`: it is a section since `π (tr i • a) = tr i • i₀ = i`, and equivariant since70`tr (g • i)⁻¹ · g · tr i` stabilises `i₀` and so fixes `a`. -/71theorem section_of_fixed_point (ρI : Action Γ I) (ρA : Action Γ A) (π : A → I)72    (hπ : Equivariant ρI ρA π) (i₀ : I) (tr : I → G) (htr : ∀ i, ρI.act (tr i) i₀ = i)73    (a : A) (ha : π a = i₀) (hfix : ∀ g, Stab ρI i₀ g → ρA.act g a = a) :74    ∃ s, IsSection π s ∧ EquivariantMap ρI ρA s :=75  ⟨fun i => ρA.act (tr i) a,76   fun i => by rw [hπ, ha, htr],77   fun g i => by78     -- h = tr (g • i)⁻¹ · (g · tr i) stabilises i₀79     have hstab : Stab ρI i₀ (Γ.mul (Γ.inv (tr (ρI.act g i))) (Γ.mul g (tr i))) := by80       show ρI.act (Γ.mul (Γ.inv (tr (ρI.act g i))) (Γ.mul g (tr i))) i₀ = i₀81       rw [ρI.mul_act, ρI.mul_act, htr i]; exact act_inv_tr ρI i₀ tr htr (ρI.act g i)82     have e := hfix _ hstab83     show ρA.act (tr (ρI.act g i)) a = ρA.act g (ρA.act (tr i) a)84     rw [← ρA.mul_act]85     -- g · tr i = tr (g • i) · h86     have e2 : Γ.mul g (tr i) = Γ.mul (tr (ρI.act g i)) (Γ.mul (Γ.inv (tr (ρI.act g i))) (Γ.mul g (tr i))) :=87       (Γ.inv_mul_cancel_left _ _).symm88     rw [e2, ρA.mul_act, e]⟩8990/-- 5:E3 (Theorem equivariant-choice, one orbit) — on a transitive index set an equivariant section exists exactly91when the stabiliser of the base point fixes a point of its fibre. -/92theorem equivariant_section_iff (ρI : Action Γ I) (ρA : Action Γ A) (π : A → I)93    (hπ : Equivariant ρI ρA π) (i₀ : I) (tr : I → G) (htr : ∀ i, ρI.act (tr i) i₀ = i) :94    (∃ s, IsSection π s ∧ EquivariantMap ρI ρA s) ↔ ∃ a, π a = i₀ ∧ ∀ g, Stab ρI i₀ g → ρA.act g a = a :=95  ⟨fun ⟨s, hs, he⟩ => ⟨s i₀, fixed_point_of_section ρI ρA π s hs he i₀⟩,96   fun ⟨a, ha, hfix⟩ => section_of_fixed_point ρI ρA π hπ i₀ tr htr a ha hfix⟩9798/-- 5:E3 (Theorem equivariant-choice, finitely many orbits) — with a representative `rep i` of every orbit, constant99on orbits, and the transport `tr i • rep i = i`, an equivariant section exists exactly when every representative's100stabiliser fixes a point of its fibre, the choice `a` of fixed points being itself constant on orbits. -/101theorem equivariant_section_orbits (ρI : Action Γ I) (ρA : Action Γ A) (π : A → I)102    (hπ : Equivariant ρI ρA π) (rep : I → I) (hrep : ∀ g i, rep (ρI.act g i) = rep i)103    (tr : I → G) (htr : ∀ i, ρI.act (tr i) (rep i) = i) :104    (∃ s, IsSection π s ∧ EquivariantMap ρI ρA s) ↔105      ∃ a : I → A, (∀ g i, a (ρI.act g i) = a i) ∧ ∀ i, π (a i) = rep i ∧ ∀ g, Stab ρI (rep i) g → ρA.act g (a i) = a i :=106  ⟨fun ⟨s, hs, he⟩ => ⟨fun i => s (rep i), fun g i => by show s (rep (ρI.act g i)) = s (rep i); rw [hrep],107     fun i => fixed_point_of_section ρI ρA π s hs he (rep i)⟩,108   fun ⟨a, hconst, hfix⟩ =>109    ⟨fun i => ρA.act (tr i) (a i),110     fun i => by rw [hπ, (hfix i).1, htr],111     fun g i => by112       have hstab : Stab ρI (rep i) (Γ.mul (Γ.inv (tr (ρI.act g i))) (Γ.mul g (tr i))) := by113         show ρI.act (Γ.mul (Γ.inv (tr (ρI.act g i))) (Γ.mul g (tr i))) (rep i) = rep i114         have h1 : ρI.act (tr (ρI.act g i)) (rep i) = ρI.act g i := by115           have := htr (ρI.act g i); rwa [hrep] at this116         rw [ρI.mul_act, ρI.mul_act, htr i]117         calc ρI.act (Γ.inv (tr (ρI.act g i))) (ρI.act g i)118             = ρI.act (Γ.inv (tr (ρI.act g i))) (ρI.act (tr (ρI.act g i)) (rep i)) := by rw [h1]119           _ = rep i := by rw [← ρI.mul_act, Γ.inv_mul, ρI.one_act]120       have e := (hfix i).2 _ hstab121       show ρA.act (tr (ρI.act g i)) (a (ρI.act g i)) = ρA.act g (ρA.act (tr i) (a i))122       rw [hconst, ← ρA.mul_act]123       have e2 : Γ.mul g (tr i) = Γ.mul (tr (ρI.act g i)) (Γ.mul (Γ.inv (tr (ρI.act g i))) (Γ.mul g (tr i))) :=124         (Γ.inv_mul_cancel_left _ _).symm125       rw [e2, ρA.mul_act, e]⟩⟩126127/-! ### 5:E4 — the equivariant obstruction on `𝔽₅` (moved from the paper module, 21 October 2026) -/128129/-- 5:E4 (Example basis-obstruction) — on the line over `𝔽₅` the map `v ↦ −v` fixes no basis: `−v ≠ v` for every130`v ≠ 0`; over `𝔽₂` it fixes `1`, so the obstruction is arithmetic. -/131theorem obstruction_five :132    (-(1 : FRC.Shell 5) ≠ 1) ∧ (-(2 : FRC.Shell 5) ≠ 2) ∧ (-(3 : FRC.Shell 5) ≠ 3) ∧ (-(4 : FRC.Shell 5) ≠ 4) ∧133      (-(1 : FRC.Shell 2) = 1) := by134  decide135136end FRC.Equivariant137138139