Units and powers in groups with zero

Two elementary facts about a group with zero G₀, and one about local ring homomorphisms.

A product a ^ i * a⁻¹ ^ (n - i), in which the two exponents are natural numbers adding up to n, is the integer power a ^ (2 * i - n). Such a product is what a diagonal matrix diag(a, a⁻¹) contributes to a monomial of degree n, so the identity is the exponent bookkeeping behind a weight computation.

Mathlib splits an integer power as a quotient (zpow_sub₀, zpow_natCast_sub_natCast₀) and subtracts natural-number exponents (pow_sub₀, inv_pow_sub₀); this is the corresponding statement for the exponents i and n - i of a and a⁻¹.

A monoid-with-zero homomorphism out of G₀ carries units to units, and that is the only way one of its values can be a unit: such a homomorphism is local, so a preimage of a unit is itself a unit of G₀. Membership of a unit in the range is therefore the same as being Units.map of a unit, which is what turns a hypothesis about Set.range (algebraMap F E) into one about Fˣ.

A local ring homomorphism reflects units, and it carries the natural number n to n; so n is invertible in the source as soon as it is invertible in the target. For an algebra map of fields K → L this is how invertibility of n travels from L down to K.

Main results

• TauCeti.pow_mul_inv_pow_eq_zpow₀: a ^ i * a⁻¹ ^ (n - i) = a ^ (2 * i - n) for i ≤ n.
• TauCeti.mem_range_iff_exists_units_map_eq: a unit lies in the range of a monoid-with-zero homomorphism out of a group with zero exactly when it is Units.map of a unit.
• TauCeti.isUnit_natCast_of_isUnit_natCast: a natural number invertible in the target of a local ring homomorphism is invertible in its source.

theorem TauCeti.pow_mul_inv_pow_eq_zpow₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) {i n : ℕ} (hi : i ≤ n) : a ^ i * a⁻¹ ^ (n - i) = a ^ (2 * ↑i - ↑n)

A power of a times a power of a⁻¹ is an integer power of a: for i ≤ n, the exponents i and n - i combine to i - (n - i) = 2 * i - n.

theorem TauCeti.mem_range_iff_exists_units_map_eq {G₀ : Type u_1} {M₀ : Type u_2} {F : Type u_3} [GroupWithZero G₀] [MonoidWithZero M₀] [Nontrivial M₀] [FunLike F G₀ M₀] [MonoidWithZeroHomClass F G₀ M₀] (f : F) (u : M₀ˣ) : ↑u ∈ Set.range ⇑f ↔ ∃ (a : G₀ˣ), (Units.map ↑f) a = u

A unit in the range of a monoid-with-zero homomorphism out of a group with zero comes from a unit. Such a homomorphism is local, so a preimage of a unit is a unit of G₀; conversely every value of Units.map f lies in the range of f.

theorem TauCeti.isUnit_natCast_of_isUnit_natCast {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) [IsLocalHom f] {n : ℕ} (hn : IsUnit ↑n) : IsUnit ↑n

A natural number invertible after a local ring homomorphism was already invertible: f carries n to n, and a local homomorphism reflects units.