Automorphisms acting on square roots

An automorphism σ of a commutative F-algebra L without zero divisors sends a square root x of an element of F to another square root of it, so σ x = x or σ x = -x. An algebra tower also allows the radicands to come from a smaller semiring. Consequently an automorphism is known on such roots once its signs on them are, and a group of automorphisms in which only the identity fixes each of n square roots has at most 2ⁿ elements.

Main results

• AlgEquiv.apply_eq_or_eq_neg_of_sq_eq: σ x = ± x when x ^ 2 comes from the base.
• Subgroup.card_le_two_pow_of_forall_apply_eq_self: a subgroup in which only the identity fixes each of n square roots has at most 2ⁿ elements.
• Subgroup.card_eq_four_of_exists_apply_eq_neg: a finite subgroup of order at most four that negates two elements and their nonzero product has order four when multiplication by 2 is injective.

theorem AlgEquiv.apply_eq_or_eq_neg_of_sq_eq {R : Type u_1} {F : Type u_2} {L : Type u_3} [CommSemiring R] [CommSemiring F] [CommRing L] [NoZeroDivisors L] [Algebra R F] [Algebra R L] [Algebra F L] [IsScalarTower R F L] (σ : L ≃ₐ[F] L) {x : L} {c : R} (hx : x ^ 2 = (algebraMap R L) c) : σ x = x ∨ σ x = -x

An automorphism sends a square root of an element of the base semiring R to plus or minus itself.

theorem Subgroup.card_le_two_pow_of_forall_apply_eq_self {R : Type u_1} {F : Type u_2} {L : Type u_3} [CommSemiring R] [CommSemiring F] [CommRing L] [NoZeroDivisors L] [Algebra R F] [Algebra R L] [Algebra F L] [IsScalarTower R F L] (H : Subgroup (L ≃ₐ[F] L)) {n : ℕ} {y : Fin n → L} {c : Fin n → R} (hy : ∀ (k : Fin n), y k ^ 2 = (algebraMap R L) (c k)) (h : ∀ τ ∈ H, (∀ (k : Fin n), τ (y k) = y k) → τ = 1) : Nat.card ↥H ≤ 2 ^ n

A subgroup of L ≃ₐ[F] L in which only the identity fixes each of n square roots of elements of R has at most 2ⁿ elements: an element is determined by the signs by which it acts on them.

theorem Subgroup.card_eq_four_of_exists_apply_eq_neg {F : Type u_4} {L : Type u_5} [CommSemiring F] [Ring L] [Algebra F L] (H : Subgroup (L ≃ₐ[F] L)) [Finite ↥H] (h2 : IsLeftRegular 2) (hle : Nat.card ↥H ≤ 4) {y z : L} (hyz : y * z ≠ 0) (h₁ : ∃ τ ∈ H, τ y = -y) (h₂ : ∃ τ ∈ H, τ z = -z) (h₃ : ∃ τ ∈ H, τ (y * z) = -(y * z)) : Nat.card ↥H = 4

A finite subgroup of L ≃ₐ[F] L with at most four elements, containing elements that negate y, z, and their nonzero product, has exactly four elements when multiplication by 2 is injective.