Scalar extension of integer affine maps

An affine map of integer coordinate lattices is determined by its value at zero and the images of the standard basis under its linear part. Casting these integer coefficients constructs compatible affine maps over the real numbers and modulo every natural number.

theorem EGZ.IntCoord.real_injective {n : ℕ} : Function.Injective real

@[simp]

theorem EGZ.IntCoord.real_zero {n : ℕ} : real 0 = 0

@[simp]

theorem EGZ.IntCoord.real_add {n : ℕ} (x y : IntCoord n) : (x + y).real = x.real + y.real

@[simp]

theorem EGZ.IntCoord.real_sub {n : ℕ} (x y : IntCoord n) : (x - y).real = x.real - y.real

theorem EGZ.IntCoord.real_zsmul {n : ℕ} (c : ℤ) (x : IntCoord n) : (c • x).real = c • x.real

noncomputable def EGZ.IntegralAffineMap.linearScalarExtension {m n : ℕ} (R : Type u_1) [CommRing R] (A : IntCoord m →ₗ[ℤ] IntCoord n) : (Fin m → R) →ₗ[R] Fin n → R

Extend the integer matrix of a linear map to a commutative ring.

Equations

• EGZ.IntegralAffineMap.linearScalarExtension R A = { toFun := fun (x : Fin m → R) (i : Fin n) => ∑ j : Fin m, x j * ↑(A (Pi.single j 1) i), map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EGZ.IntegralAffineMap.scalarExtension {m n : ℕ} (R : Type u_1) [CommRing R] (A : IntCoord m →ᵃ[ℤ] IntCoord n) : (Fin m → R) →ᵃ[R] Fin n → R

Extend the integer coefficients and offset of an affine lattice map.

Equations

• EGZ.IntegralAffineMap.scalarExtension R A = (EGZ.IntegralAffineMap.linearScalarExtension R A.linear).toAffineMap + AffineMap.const R (Fin m → R) fun (i : Fin n) => ↑(A 0 i)

@[simp]

theorem EGZ.IntegralAffineMap.scalarExtension_apply {m n : ℕ} (R : Type u_1) [CommRing R] (A : IntCoord m →ᵃ[ℤ] IntCoord n) (x : Fin m → R) (i : Fin n) : (scalarExtension R A) x i = ∑ j : Fin m, x j * ↑(A.linear (Pi.single j 1) i) + ↑(A 0 i)

theorem EGZ.IntegralAffineMap.integer_expansion {m n : ℕ} (A : IntCoord m →ᵃ[ℤ] IntCoord n) (z : IntCoord m) (i : Fin n) : A z i = ∑ j : Fin m, z j * A.linear (Pi.single j 1) i + A 0 i

Standard-basis expansion of an integer affine map, coordinate by coordinate.

theorem EGZ.IntegralAffineMap.scalarExtension_intCast {m n : ℕ} (R : Type u_1) [CommRing R] (A : IntCoord m →ᵃ[ℤ] IntCoord n) (z : IntCoord m) : ((scalarExtension R A) fun (i : Fin m) => ↑(z i)) = fun (i : Fin n) => ↑(A z i)

Scalar extension agrees with the integer map on every integer vector.

theorem EGZ.IntegralAffineMap.affine_ext_intCast {m n : ℕ} (R : Type u_1) [CommRing R] {A B : (Fin m → R) →ᵃ[R] Fin n → R} (h : ∀ (z : IntCoord m), (A fun (i : Fin m) => ↑(z i)) = B fun (i : Fin m) => ↑(z i)) : A = B

Affine maps on a coordinate module are determined by their values on integer coordinate vectors, over any commutative ring.

@[simp]

theorem EGZ.IntegralAffineMap.scalarExtension_id {n : ℕ} (R : Type u_1) [CommRing R] : scalarExtension R (AffineMap.id ℤ (IntCoord n)) = AffineMap.id R (Fin n → R)

@[simp]

theorem EGZ.IntegralAffineMap.scalarExtension_comp {l m n : ℕ} (R : Type u_1) [CommRing R] (A : IntCoord m →ᵃ[ℤ] IntCoord n) (B : IntCoord l →ᵃ[ℤ] IntCoord m) : scalarExtension R (A.comp B) = (scalarExtension R A).comp (scalarExtension R B)

noncomputable def EGZ.IntegralAffineMap.ofIntAffineMap {m n : ℕ} (A : IntCoord m →ᵃ[ℤ] IntCoord n) : IntegralAffineMap m n

Package any integer affine map with its real and modular scalar extensions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EGZ.IntegralAffineMap.ofIntAffineMap_integer {m n : ℕ} (A : IntCoord m →ᵃ[ℤ] IntCoord n) : (ofIntAffineMap A).integer = ⇑A

@[simp]

theorem EGZ.IntegralAffineMap.ofIntAffineMap_real {m n : ℕ} (A : IntCoord m →ᵃ[ℤ] IntCoord n) : (ofIntAffineMap A).real = scalarExtension ℝ A

@[simp]

theorem EGZ.IntegralAffineMap.ofIntAffineMap_modp {m n : ℕ} (A : IntCoord m →ᵃ[ℤ] IntCoord n) (p : ℕ) : (ofIntAffineMap A).modp p = scalarExtension (ZMod p) A

theorem EGZ.IntegralAffineMap.ext_integer {m n : ℕ} {A B : IntegralAffineMap m n} (h : A.integer = B.integer) : A = B

An integral-affine map is determined by its integer realization.

theorem EGZ.IntegralAffineMap.ext_integer_iff {m n : ℕ} {A B : IntegralAffineMap m n} : A = B ↔ A.integer = B.integer

@[simp]

theorem EGZ.IntegralAffineMap.ofIntAffineMap_id {n : ℕ} : ofIntAffineMap (AffineMap.id ℤ (IntCoord n)) = id n

@[simp]

theorem EGZ.IntegralAffineMap.ofIntAffineMap_comp {l m n : ℕ} (A : IntCoord m →ᵃ[ℤ] IntCoord n) (B : IntCoord l →ᵃ[ℤ] IntCoord m) : ofIntAffineMap (A.comp B) = (ofIntAffineMap A).comp (ofIntAffineMap B)

theorem EGZ.IntegralAffineMap.linearScalarExtension_real_injective {m n : ℕ} (A : IntCoord m →ₗ[ℤ] IntCoord n) (hA : Function.Injective ⇑A) : Function.Injective ⇑(linearScalarExtension ℝ A)

Injectivity of an integer linear map survives extension to real scalars.

theorem EGZ.IntegralAffineMap.ofIntAffineMap_real_injective {m n : ℕ} (A : IntCoord m →ᵃ[ℤ] IntCoord n) (hA : Function.Injective ⇑A) : Function.Injective ⇑(ofIntAffineMap A).real

An injective affine lattice chart has an injective real realization.

theorem EGZ.IntegralAffineMap.integer_sub_zero_real {m n : ℕ} (A : IntegralAffineMap m n) (z : IntCoord m) : (A.integer z - A.integer 0).real = A.real.linear z.real

The difference from the integer offset realizes the real linear part.

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

Recover the integer linear part of an integral-affine map. Its additivity and integer homogeneity follow from compatibility with its real realization.

Equations

• A.integerLinear = { toFun := fun (z : EGZ.IntCoord m) => A.integer z - A.integer 0, map_add' := ⋯, map_smul' := ⋯ }

def EGZ.IntegralAffineMap.toIntAffineMap {m n : ℕ} (A : IntegralAffineMap m n) : IntCoord m →ᵃ[ℤ] IntCoord n

The stored integer realization is itself an affine map over the integers.

Equations

• A.toIntAffineMap = { toFun := A.integer, linear := A.integerLinear, map_vadd' := ⋯ }

@[simp]

theorem EGZ.IntegralAffineMap.toIntAffineMap_apply {m n : ℕ} (A : IntegralAffineMap m n) (z : IntCoord m) : A.toIntAffineMap z = A.integer z

@[simp]

theorem EGZ.IntegralAffineMap.ofIntAffineMap_toIntAffineMap {m n : ℕ} (A : IntegralAffineMap m n) : ofIntAffineMap A.toIntAffineMap = A

@[simp]

theorem EGZ.IntegralAffineMap.toIntAffineMap_ofIntAffineMap {m n : ℕ} (A : IntCoord m →ᵃ[ℤ] IntCoord n) : (ofIntAffineMap A).toIntAffineMap = A

@[simp]

theorem EGZ.IntegralAffineMap.toIntAffineMap_id {n : ℕ} : (id n).toIntAffineMap = AffineMap.id ℤ (IntCoord n)

@[simp]

theorem EGZ.IntegralAffineMap.toIntAffineMap_comp {l m n : ℕ} (A : IntegralAffineMap m n) (B : IntegralAffineMap l m) : (A.comp B).toIntAffineMap = A.toIntAffineMap.comp B.toIntAffineMap