Fixed points of a generated subgroup

A point is fixed by the subgroup generated by a set exactly when every element of the set fixes it. This reduces the fixed-point conditions in the Frobenius power criteria to their generators. Likewise, a function invariant under every element of a set S of a group acting on its domain is invariant under the subgroup generated by S (TauCeti.apply_eq_of_mem_closure), hence constant when that subgroup acts transitively (TauCeti.apply_eq_apply_of_isPretransitive_closure).

theorem TauCeti.forall_mem_closure_smul_eq_self_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {s : Set G} {x : X} : (∀ g ∈ Subgroup.closure s, g • x = x) ↔ ∀ g ∈ s, g • x = x

A generated subgroup fixes a point exactly when all its generators fix that point.

theorem TauCeti.apply_eq_of_mem_closure {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G α] {S : Set G} {f : α → β} (hS : ∀ g ∈ S, ∀ (a : α), f (g • a) = f a) {g : G} (hg : g ∈ Subgroup.closure S) (a : α) : f (g • a) = f a

A function invariant under every element of a set S of a group acting on α is invariant under the whole subgroup generated by S.

theorem TauCeti.apply_eq_apply_of_isPretransitive_closure {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G α] {S : Set G} {f : α → β} (hS : ∀ g ∈ S, ∀ (a : α), f (g • a) = f a) (hconn : MulAction.IsPretransitive (↥(Subgroup.closure S)) α) (a b : α) : f a = f b

A function invariant under every element of a set S of a group acting on α takes a single value when the subgroup generated by S acts transitively.