Cup-product naturality and powers

Reusable algebra for powers under multiplicative pullbacks, together with its cochain-level realization. The cohomology-level cup product and power naturality are implemented in CohomologyCupProduct.lean; InducedOnRPCohomology.lean specializes them to maps of RP n.

1. Reusable algebra: powers under multiplicative maps

theorem SphereOddDegree.mulMap_pow {M : Type u_1} [Monoid M] {φ : M → M} (hmul : ∀ (a b : M), φ (a * b) = φ a * φ b) (hone : φ 1 = 1) (a : M) (n : ℕ) : φ (a ^ n) = φ a ^ n

A multiplicative, unital self-map of a monoid preserves powers: φ(aⁿ) = (φ a)ⁿ. (Unbundled form, for use before a MonoidHom is available.)

theorem SphereOddDegree.mulMap_pow_fixed {M : Type u_1} [Monoid M] {φ : M → M} (hmul : ∀ (a b : M), φ (a * b) = φ a * φ b) (hone : φ 1 = 1) {a : M} (ha : φ a = a) (n : ℕ) : φ (a ^ n) = a ^ n

A multiplicative, unital self-map of a monoid fixes the powers of any fixed point: if φ a = a then φ(aⁿ) = aⁿ.

theorem SphereOddDegree.MonoidHom.map_pow_fixed {M : Type u_1} [Monoid M] (φ : M →* M) {a : M} (ha : φ a = a) (n : ℕ) : φ (a ^ n) = a ^ n

A monoid homomorphism fixes the powers of any fixed point: φ a = a ⟹ φ(aⁿ) = aⁿ. This is the algebraic shape of the final target fbar^*(α)=α ⟹ fbar^*(αⁿ)=αⁿ once the pullback is a (multiplicative) ring map.

theorem SphereOddDegree.RingHom.map_pow_fixed {R : Type u_1} [Semiring R] (φ : R →+* R) {a : R} (ha : φ a = a) (n : ℕ) : φ (a ^ n) = a ^ n

A ring homomorphism fixes the powers of any fixed point: φ a = a ⟹ φ(aⁿ) = aⁿ. The cohomology pullback fbar^* will be such a ring map once the cohomology-level cup product exists; this is then the verbatim final step.

2. Abstract graded multiplicative-pullback API

This packages exactly the structure a cohomology-level cup product with a multiplicative pullback provides — a degreewise product, a unit, and a degreewise pullback satisfying multiplicativity and unitality — and derives that the pullback preserves cup powers of a degree-one class, plus the fixed-point corollary. It is independent of singular cohomology and reusable.

structure SphereOddDegree.GradedCupPullback (A : ℕ → Type u_1) : Type u_1

An abstract graded multiplicative pullback on a graded family A : ℕ → Type*: a degreewise product cup, a degree-0 unit one, and a degreewise self-map pull that is multiplicative (pull (cup a b) = cup (pull a) (pull b)) and unital (pull one = one).

• cup {p q : ℕ} : A p → A q → A (p + q)

  The degreewise product A p → A q → A (p+q).

• one : A 0

  The degree-0 unit.

• pull {p : ℕ} : A p → A p

  The degreewise pullback self-map.

• pull_one : self.pull self.one = self.one

  The pullback fixes the unit.

• pull_cup {p q : ℕ} (a : A p) (b : A q) : self.pull (self.cup a b) = self.cup (self.pull a) (self.pull b)

  The pullback is multiplicative for the graded product.

def SphereOddDegree.GradedCupPullback.pow {A : ℕ → Type u_1} (G : GradedCupPullback A) (x : A 1) (n : ℕ) : A n

The n-th cup power xⁿ ∈ A n of a degree-one element x ∈ A 1, by x⁰ = one and xⁿ⁺¹ = xⁿ ⌣ x.

Equations

• G.pow x 0 = G.one
• G.pow x n.succ = G.cup (G.pow x n) x

@[simp]

theorem SphereOddDegree.GradedCupPullback.pow_zero {A : ℕ → Type u_1} (G : GradedCupPullback A) (x : A 1) : G.pow x 0 = G.one

@[simp]

theorem SphereOddDegree.GradedCupPullback.pow_succ {A : ℕ → Type u_1} (G : GradedCupPullback A) (x : A 1) (n : ℕ) : G.pow x (n + 1) = G.cup (G.pow x n) x

theorem SphereOddDegree.GradedCupPullback.pull_pow {A : ℕ → Type u_1} (G : GradedCupPullback A) (x : A 1) (n : ℕ) : G.pull (G.pow x n) = G.pow (G.pull x) n

Pullback preserves powers. pull(xⁿ) = (pull x)ⁿ.

theorem SphereOddDegree.GradedCupPullback.pull_pow_fixed {A : ℕ → Type u_1} (G : GradedCupPullback A) {x : A 1} (hx : G.pull x = x) (n : ℕ) : G.pull (G.pow x n) = G.pow x n

Fixed-point powers. If pull x = x then pull(xⁿ) = xⁿ for all n.

3. Cochain-level realization

The pullback of a self-map f : X ⟶ X together with the cochain cup product and unit form a GradedCupPullback, from which the fixed-point power theorem follows.

@[simp]

theorem SphereOddDegree.cochainPullback_one {R : Type} [CommRing R] {X Y : TopCat} (f : X ⟶ Y) : cochainPullback f 0 cochainOne = cochainOne

Pullback fixes the unit cochain. f^*(1) = 1.

noncomputable def SphereOddDegree.cochainCupPullback {R : Type} [CommRing R] {X : TopCat} (f : X ⟶ X) : GradedCupPullback fun (p : ℕ) => singularCochainGroup R X p

The cochain cup product, unit, and pullback of a self-map f : X ⟶ X assemble into a GradedCupPullback on the graded family of singular cochain groups. Its pow is cochainPow and its pull_pow/pull_pow_fixed specialize to the cochain-level power naturality / fixed-point theorems.

Equations

• One or more equations did not get rendered due to their size.

theorem SphereOddDegree.cochainCupPullback_pow {R : Type} [CommRing R] {X : TopCat} (f : X ⟶ X) (φ : singularCochainGroup R X 1) (n : ℕ) : (cochainCupPullback f).pow φ n = cochainPow φ n

The abstract pow of cochainCupPullback is the cochain power cochainPow.

theorem SphereOddDegree.cochainPow_fixed {R : Type} [CommRing R] {X : TopCat} (f : X ⟶ X) (φ : singularCochainGroup R X 1) (hφ : cochainPullback f 1 φ = φ) (n : ℕ) : cochainPullback f n (cochainPow φ n) = cochainPow φ n

Fixed-point powers at cochain level. If a degree-one cochain φ is fixed by the pullback f^* of a self-map f : X ⟶ X (i.e. f^*φ = φ), then so are all its cup powers: f^*(φⁿ) = φⁿ. This is the cochain-level form of the final target fbar^*(α)=α ⟹ fbar^*(αⁿ)=αⁿ.

theorem SphereOddDegree.cochainPow_fixedZMod2 {X : TopCat} (f : X ⟶ X) (φ : singularCochainGroup (ZMod 2) X 1) (hφ : cochainPullback f 1 φ = φ) (n : ℕ) : cochainPullback f n (cochainPowZMod2 φ n) = cochainPowZMod2 φ n

ZMod 2 specialization of the cochain-level fixed-point power theorem: f^*φ = φ ⟹ f^*(φⁿ) = φⁿ over ZMod 2.