Surjective Lang maps and fixed lifts

The Lang map is written in Mathlib's convention as MonoidHom.commutatorMap F, namely t ↦ t / F t. On a commutative group, surjectivity for an iterate of F implies surjectivity for F, by the telescoping product of the iterates. In particular, if an iterate is a power map and the corresponding roots exist, the Lang map is surjective.

A surjective Lang map on an invariant subgroup corrects an element whose Frobenius defect lies in that subgroup to a fixed element in the same coset. This is useful for lifting fixed elements of a normalizer quotient; it does not require a finite kernel or claim uniqueness of a fixed lift.

The telescoping calculation follows the argument of MonoidHom.FixedPointFree.prod_pow_eq_one in Mathlib. The correction argument is the usual torus correction in Steinberg, Lectures on Chevalley Groups, Chapter 11.

theorem MonoidHom.commutatorMap_prod_range {T : Type u_1} [CommGroup T] (F : T →* T) (m : ℕ) (t : T) : commutatorMap (⇑F) (∏ i ∈ Finset.range m, (⇑F)^[i] t) = t / (⇑F)^[m] t

The Lang map of the product of the first m iterates telescopes to the Lang map of the m-th iterate.

theorem MonoidHom.surjective_commutatorMap_of_iterate {T : Type u_1} [CommGroup T] (F : T →* T) (m : ℕ) (h : Function.Surjective (commutatorMap (⇑F)^[m])) : Function.Surjective (commutatorMap ⇑F)

On a commutative group, surjectivity of the Lang map of any iterate implies surjectivity of the Lang map of the original endomorphism.

theorem MonoidHom.surjective_commutatorMap_of_iterate_eq_pow {T : Type u_1} [CommGroup T] (F : T →* T) {m Q : ℕ} (hQ : 0 < Q) (hF : ∀ (t : T), (⇑F)^[m] t = t ^ Q) (hroot : Function.Surjective fun (t : T) => t ^ (Q - 1)) : Function.Surjective (commutatorMap ⇑F)

If an iterate of F is the Q-th power map, and every element has a (Q - 1)-st root, then the Lang map of F is surjective.

theorem MonoidHom.exists_fixed_inv_mul_of_surjective_commutatorMap {T : Type u_1} {G : Type u_2} [Group T] [Group G] (ι : T →* G) (f : T →* T) (F : G →* G) (hι : ∀ (t : T), F (ι t) = ι (f t)) (hf : Function.Surjective (commutatorMap ⇑f)) {n : G} (hn : n / F n ∈ ι.range) : ∃ (t : T), F ((ι t)⁻¹ * n) = (ι t)⁻¹ * n

Correct an element to a fixed element by left multiplication from an invariant subgroup with surjective Lang map. The defect must lie in the subgroup's image.

theorem MonoidHom.exists_fixed_lift_of_surjective_commutatorMap {T : Type u_1} {G : Type u_2} [Group T] [Group G] {H : Type u_3} [Group H] (ψ : G →* H) (j : T →* G) (hker : j.range = ψ.ker) (f : T →* T) (F : G →* G) (F' : H →* H) (hψ : ∀ (x : G), ψ (F x) = F' (ψ x)) (hj : ∀ (t : T), F (j t) = j (f t)) (hsurj : Function.Surjective ⇑ψ) (hf : Function.Surjective (commutatorMap ⇑f)) {y : H} (hy : F' y = y) : ∃ (x : G), F x = x ∧ ψ x = y

An equivariant surjection admits fixed lifts if its kernel is parametrized by an invariant group with surjective Lang map. The parametrization need not be injective.