Injectivity over the reals from injectivity modulo a prime

For a square integer matrix, injectivity modulo a prime implies that the integer determinant is nonzero. Its real scalar extension is therefore injective. This applies to integral affine maps between equal-rank fibres.

def EGZ.IntegralAffineMap.coefficientMatrix {m n : ℕ} (A : IntCoord m →ₗ[ℤ] IntCoord n) : Matrix (Fin n) (Fin m) ℤ

The integer coefficient matrix in standard coordinate bases.

Equations

• EGZ.IntegralAffineMap.coefficientMatrix A i j = A (Pi.single j 1) i

theorem EGZ.IntegralAffineMap.linearScalarExtension_eq_mulVec {m n : ℕ} (R : Type u_1) [CommRing R] (A : IntCoord m →ₗ[ℤ] IntCoord n) : ⇑(linearScalarExtension R A) = ((coefficientMatrix A).map ⇑(Int.castRingHom R)).mulVec

theorem EGZ.IntegralAffineMap.linearScalarExtension_real_injective_of_modp {p n : ℕ} [Fact (Nat.Prime p)] (A : IntCoord n →ₗ[ℤ] IntCoord n) (hA : Function.Injective ⇑(linearScalarExtension (ZMod p) A)) : Function.Injective ⇑(linearScalarExtension ℝ A)

A square integer linear map injective modulo p stays injective after extending scalars to the real numbers.

theorem EGZ.IntegralAffineMap.ofIntAffineMap_real_injective_of_modp {p n : ℕ} [Fact (Nat.Prime p)] (A : IntCoord n →ᵃ[ℤ] IntCoord n) (hA : Function.Injective ⇑((ofIntAffineMap A).modp p)) : Function.Injective ⇑(ofIntAffineMap A).real

theorem EGZ.IntegralAffineMap.real_injective_of_modp_of_rank_eq {p m n : ℕ} [Fact (Nat.Prime p)] (A : IntegralAffineMap m n) (hrank : m = n) (hA : Function.Injective ⇑(A.modp p)) : Function.Injective ⇑A.real

An equal-rank integral affine map which is injective modulo a prime is injective on its real coordinate spaces.

theorem EGZ.IntegralAffineMap.integer_injective_of_modp_of_rank_eq {p m n : ℕ} [Fact (Nat.Prime p)] (A : IntegralAffineMap m n) (hrank : m = n) (hA : Function.Injective ⇑(A.modp p)) : Function.Injective A.integer

The same map is injective on its integer lattices.