Units and coprimality over ZMod d

Results connecting unit and coprimality data over ZMod d, independent of one another:

• Int.isUnit_intCast_iff_gcd_eq_one — an integer is a unit mod d exactly when it is coprime to d. Its consumers are the Atkin-Lehner and bad-prime double-coset arguments in TauCeti/NumberTheory/HeckeRing/GL2/Gamma0/, which need the Int.gcd form of the unit condition carried by membership of Δ₀(N), and Int.exists_nonneg_lt_and_dvd_mul_sub in TauCeti/Data/Int/LinearCongruence.lean, which needs the other direction.
• IsCoprime.exists_int_lifts — a pair of coprime residues mod d lifts to a coprime pair of integers. Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/SL2Surjection.lean, Chris Birkbeck); its consumer is the strong approximation theorem Matrix.SpecialLinearGroup.map_intCast_zmod_surjective in TauCeti/LinearAlgebra/Matrix/SpecialLinearGroup/Basic.lean.
• TauCeti.comp_unitsMap_eq_comp_unitsMap_of_comp_mul_left — a lowered unit homomorphism stays lowered after restricting to a multiple of its modulus.
• ZMod.exists_unitOfCoprime_eq — every unit of ZMod d is ZMod.unitOfCoprime of a natural number coprime to d, so a statement about all units may be checked on those.
• ZMod.unitOfCoprime_mul — ZMod.unitOfCoprime is multiplicative in its numerator.
• TauCeti.eq_comp_unitsMap_of_comp_unitsMap_eq — a unit homomorphism that agrees with a lowered one after restriction along ZMod.unitsMap is itself that lowered one, read at the smaller modulus. Its consumers are the descent arguments of TauCeti/NumberTheory/ModularForms/Newforms/Descent/, which carry a nebentypus lowered modulo M / p along a chain of divisibilities.
• ZMod.zmultiples_coe_unit_eq_top — a unit of ZMod d generates ZMod d additively, so that translation by it is a single cycle; its consumer is the genus-one Heegaard diagram of a lens space in TauCeti/LowDimTopology/Heegaard/LensSpace.lean.

theorem Int.isUnit_intCast_iff_gcd_eq_one {d : ℕ} {a : ℤ} : IsUnit ↑a ↔ a.gcd ↑d = 1

An integer is a unit mod d exactly when it is coprime to d. The Int.gcd form is what consumers of Nat.Coprime want; ZMod.coe_int_isUnit_iff_isCoprime states the same equivalence with IsCoprime over ℤ on the right, in the opposite argument order.

theorem TauCeti.eq_comp_unitsMap_of_comp_unitsMap_eq {G : Type u_1} [MulOne G] {p M M' N' : ℕ} [NeZero M'] (hpM : p ∣ M) (hMN' : M ∣ N') (hN'M' : N' ∣ M') {χM : (ZMod M)ˣ →* G} {χ₀ : (ZMod (M / p))ˣ →* G} (hcomp : χM = χ₀.comp (ZMod.unitsMap ⋯)) {χ' : (ZMod N')ˣ →* G} (h : χ'.comp (ZMod.unitsMap hN'M') = χM.comp (ZMod.unitsMap ⋯)) : χ' = (χ₀.comp (ZMod.unitsMap ⋯)).comp (ZMod.unitsMap ⋯)

A lowered unit homomorphism is determined at the smaller modulus. If χM is pulled back from χ₀ modulo M / p, and χ' modulo N' agrees with χM after restriction to the units modulo a common multiple M', then χ' is itself pulled back from χ₀, along N' / p. ZMod.unitsMap is surjective onto the units of a divisor, so the restriction can be cancelled.

theorem TauCeti.comp_unitsMap_eq_comp_unitsMap_of_comp_mul_left {G : Type u_1} [MulOne G] {p N L : ℕ} (hpN : p ∣ N) {χ : (ZMod N)ˣ →* G} {χ₀ : (ZMod (N / p))ˣ →* G} (hcomp : χ = χ₀.comp (ZMod.unitsMap ⋯)) : χ.comp (ZMod.unitsMap ⋯) = (χ₀.comp (ZMod.unitsMap ⋯)).comp (ZMod.unitsMap ⋯)

A lowered unit homomorphism stays lowered after restricting to a multiple. If χ modulo N is pulled back from χ₀ modulo N / p, then restricting χ to the units modulo N * L is again a pull-back of χ₀, now along N * L / p. Both sides collapse to one ZMod.unitsMap by ZMod.unitsMap_comp.

theorem IsCoprime.exists_int_lifts {d : ℕ} {a c : ZMod d} (hac : IsCoprime a c) : ∃ (a₀ : ℤ) (c₀ : ℤ), ↑a₀ = a ∧ ↑c₀ = c ∧ IsCoprime a₀ c₀

Coprime residues modulo d lift to coprime integers: if a and c are coprime in ZMod d, there are integers a₀, c₀ reducing to a, c with IsCoprime a₀ c₀.

theorem ZMod.exists_unitOfCoprime_eq {d : ℕ} [NeZero d] (u : (ZMod d)ˣ) : ∃ (m : ℕ) (hm : m.Coprime d), unitOfCoprime m hm = u

Every unit of ZMod d is ZMod.unitOfCoprime of a natural number coprime to d. A property of all units may therefore be checked on the units of this shape.

theorem ZMod.unitOfCoprime_mul {d m n : ℕ} (hm : m.Coprime d) (hn : n.Coprime d) : unitOfCoprime (m * n) ⋯ = unitOfCoprime m hm * unitOfCoprime n hn

ZMod.unitOfCoprime is multiplicative in its numerator.

theorem ZMod.zmultiples_coe_unit_eq_top {d : ℕ} (u : (ZMod d)ˣ) : AddSubgroup.zmultiples ↑u = ⊤

A unit of ZMod d generates ZMod d as an additive group.