Multiplicative maps into rings

The element -1 squares to 1. A multiplicative map into a ring without zero divisors therefore sends it to 1 or -1. This applies to ordinary ring-valued maps as well as to unit-valued characters after composing with the coercion homomorphism.

A ring homomorphism fixes natural number casts, so it preserves membership statements of the form n ^ k * x ∈ A: if it maps A into B, then n ^ k * x ∈ A implies n ^ k * f x ∈ B. This controls denominators under ring endomorphisms that preserve a subring, as in integrality arguments for Hazewinkel's functional equation.

Main results

• TauCeti.map_neg_one_eq_one_or_eq_neg_one: the image of -1 is 1 or -1.
• Set.MapsTo.natCast_pow_mul_apply_mem: if a ring homomorphism f maps A into B, then n ^ k * x ∈ A implies n ^ k * f x ∈ B.
• Set.MapsTo.ringHom_pow: if a ring endomorphism f maps A into itself, so does f ^ n.

theorem TauCeti.map_neg_one_eq_one_or_eq_neg_one {F : Type u_1} {M : Type u_2} {R : Type u_3} [MulOneClass M] [HasDistribNeg M] [NonAssocRing R] [NoZeroDivisors R] [FunLike F M R] [MonoidHomClass F M R] (f : F) : f (-1) = 1 ∨ f (-1) = -1

A multiplicative map into a ring without zero divisors sends -1 to 1 or -1. Only distributive negation and a multiplicative identity are required in the source; the target ring need not be associative.

theorem Set.MapsTo.ringHom_pow {R : Type u_1} [NonAssocSemiring R] {f : R →+* R} {A : Set R} (hf : MapsTo (⇑f) A A) (n : ℕ) : MapsTo (⇑(f ^ n)) A A

If a ring endomorphism f maps A into itself, then so does its power f ^ n, which is the n-th iterate of f.

theorem Set.MapsTo.natCast_pow_mul_apply_mem {R : Type u_1} {S : Type u_2} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S] {f : F} {A : Set R} {B : Set S} (hf : MapsTo (⇑f) A B) {n k : ℕ} {x : R} (hx : ↑n ^ k * x ∈ A) : ↑n ^ k * f x ∈ B

If a ring homomorphism f maps A into B, then n ^ k * x ∈ A implies n ^ k * f x ∈ B for all natural numbers n and k, since f fixes n ^ k. No closure properties of A or B are needed.