Adding slab coordinates to a flag fibre

The completeness refinement augments a fibre by finitely many affine functionals. These coordinate maps project to the old fibre, retain the additional coordinates along lower transitions, and commute with scalar extension and reduction modulo every modulus.

def EGZ.Coord.first {R : Type u_1} [CommRing R] (m k : ℕ) : (Fin (m + k) → R) →ₗ[R] Fin m → R

Linear projection onto the first block of coordinates.

Equations

• EGZ.Coord.first m k = LinearMap.pi fun (i : Fin m) => LinearMap.proj (Fin.castAdd k i)

def EGZ.Coord.last {R : Type u_1} [CommRing R] (m k : ℕ) : (Fin (m + k) → R) →ₗ[R] Fin k → R

Linear projection onto the last block of coordinates.

Equations

• EGZ.Coord.last m k = LinearMap.pi fun (i : Fin k) => LinearMap.proj (Fin.natAdd m i)

@[simp]

theorem EGZ.Coord.first_apply {R : Type u_1} [CommRing R] {m k : ℕ} (q : Fin (m + k) → R) (i : Fin m) : (first m k) q i = q (Fin.castAdd k i)

@[simp]

theorem EGZ.Coord.last_apply {R : Type u_1} [CommRing R] {m k : ℕ} (q : Fin (m + k) → R) (i : Fin k) : (last m k) q i = q (Fin.natAdd m i)

def EGZ.Coord.append {R : Type u_1} [CommRing R] {V : Type u_2} [AddCommGroup V] [Module R V] {m k : ℕ} (A : V →ᵃ[R] Fin m → R) (B : V →ᵃ[R] Fin k → R) : V →ᵃ[R] Fin (m + k) → R

Append the outputs of two affine maps in the standard finite coordinates.

Equations

• EGZ.Coord.append A B = AffineMap.pi fun (i : Fin (m + k)) => Fin.addCases (fun (i : Fin m) => (AffineMap.proj i).comp A) (fun (i : Fin k) => (AffineMap.proj i).comp B) i

@[simp]

theorem EGZ.Coord.append_castAdd {R : Type u_1} [CommRing R] {V : Type u_2} [AddCommGroup V] [Module R V] {m k : ℕ} (A : V →ᵃ[R] Fin m → R) (B : V →ᵃ[R] Fin k → R) (v : V) (i : Fin m) : (append A B) v (Fin.castAdd k i) = A v i

@[simp]

theorem EGZ.Coord.append_natAdd {R : Type u_1} [CommRing R] {V : Type u_2} [AddCommGroup V] [Module R V] {m k : ℕ} (A : V →ᵃ[R] Fin m → R) (B : V →ᵃ[R] Fin k → R) (v : V) (i : Fin k) : (append A B) v (Fin.natAdd m i) = B v i

@[simp]

theorem EGZ.Coord.first_append {R : Type u_1} [CommRing R] {V : Type u_2} [AddCommGroup V] [Module R V] {m k : ℕ} (A : V →ᵃ[R] Fin m → R) (B : V →ᵃ[R] Fin k → R) (v : V) : (first m k) ((append A B) v) = A v

@[simp]

theorem EGZ.Coord.last_append {R : Type u_1} [CommRing R] {V : Type u_2} [AddCommGroup V] [Module R V] {m k : ℕ} (A : V →ᵃ[R] Fin m → R) (B : V →ᵃ[R] Fin k → R) (v : V) : (last m k) ((append A B) v) = B v

def EGZ.Coord.extend {R : Type u_1} [CommRing R] {m n : ℕ} (A : (Fin m → R) →ᵃ[R] Fin n → R) (k : ℕ) : (Fin (m + k) → R) →ᵃ[R] Fin (n + k) → R

Extend an affine map while leaving additional coordinates fixed.

Equations

• EGZ.Coord.extend A k = EGZ.Coord.append (A.comp (EGZ.Coord.first m k).toAffineMap) (EGZ.Coord.last m k).toAffineMap

@[simp]

theorem EGZ.Coord.first_extend {R : Type u_1} [CommRing R] {m n k : ℕ} (A : (Fin m → R) →ᵃ[R] Fin n → R) (q : Fin (m + k) → R) : (first n k) ((extend A k) q) = A ((first m k) q)

@[simp]

theorem EGZ.Coord.last_extend {R : Type u_1} [CommRing R] {m n k : ℕ} (A : (Fin m → R) →ᵃ[R] Fin n → R) (q : Fin (m + k) → R) : (last n k) ((extend A k) q) = (last m k) q

theorem EGZ.Coord.ext_first_last {R : Type u_1} [CommRing R] {m k : ℕ} {q r : Fin (m + k) → R} (hfirst : (first m k) q = (first m k) r) (hlast : (last m k) q = (last m k) r) : q = r

theorem EGZ.Coord.extend_id {R : Type u_1} [CommRing R] (m k : ℕ) : extend (AffineMap.id R (Fin m → R)) k = AffineMap.id R (Fin (m + k) → R)

theorem EGZ.Coord.extend_comp {R : Type u_1} [CommRing R] {l m n : ℕ} (A : (Fin m → R) →ᵃ[R] Fin n → R) (B : (Fin l → R) →ᵃ[R] Fin m → R) (k : ℕ) : extend (A.comp B) k = (extend A k).comp (extend B k)

def EGZ.IntegralAffineMap.first (m k : ℕ) : IntegralAffineMap (m + k) m

Forget the extra coordinates of an augmented lattice fibre.

Equations

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

noncomputable def EGZ.IntegralAffineMap.extend {m n : ℕ} (A : IntegralAffineMap m n) (k : ℕ) : IntegralAffineMap (m + k) (n + k)

Apply an old transition and keep the newly added slab coordinates.

Equations

• A.extend k = { real := EGZ.Coord.extend A.real k, integer := ⇑(EGZ.Coord.extend A.toIntAffineMap k), modp := fun (p : ℕ) => EGZ.Coord.extend (A.modp p) k, real_integer := ⋯, mod_integer := ⋯ }

theorem EGZ.IntegralAffineMap.first_comp_extend {m n : ℕ} (A : IntegralAffineMap m n) (k : ℕ) : (first n k).comp (A.extend k) = A.comp (first m k)

theorem EGZ.IntegralAffineMap.extend_id (m k : ℕ) : (id m).extend k = id (m + k)

theorem EGZ.IntegralAffineMap.extend_comp {l m n : ℕ} (A : IntegralAffineMap m n) (B : IntegralAffineMap l m) (k : ℕ) : (A.comp B).extend k = (A.extend k).comp (B.extend k)

theorem EGZ.latticeSupNorm_le_of_first_last {m k B : ℕ} (q : IntCoord (m + k)) (hfirst : latticeSupNorm ((Coord.first m k) q) ≤ B) (hlast : latticeSupNorm ((Coord.last m k) q) ≤ B) : latticeSupNorm q ≤ B

def EGZ.Coord.prefixMap {R : Type u_1} [CommRing R] (es et : ℕ) (h : et ≤ es) : (Fin es → R) →ₗ[R] Fin et → R

Keep the initial coordinates of a finite coordinate vector.

Equations

• EGZ.Coord.prefixMap es et h = LinearMap.pi fun (i : Fin et) => LinearMap.proj (Fin.castLE h i)

@[simp]

theorem EGZ.Coord.prefixMap_apply {R : Type u_1} [CommRing R] {es et : ℕ} (h : et ≤ es) (q : Fin es → R) (i : Fin et) : (prefixMap es et h) q i = q (Fin.castLE h i)

@[simp]

theorem EGZ.Coord.prefixMap_refl {R : Type u_1} [CommRing R] (e : ℕ) (q : Fin e → R) : (prefixMap e e ⋯) q = q

@[simp]

theorem EGZ.Coord.prefixMap_comp {R : Type u_1} [CommRing R] {es em et : ℕ} (hm : em ≤ es) (ht : et ≤ em) (q : Fin es → R) : (prefixMap em et ht) ((prefixMap es em hm) q) = (prefixMap es et ⋯) q

def EGZ.Coord.extendPrefix {R : Type u_1} [CommRing R] {m n : ℕ} (A : (Fin m → R) →ᵃ[R] Fin n → R) (es et : ℕ) (h : et ≤ es) : (Fin (m + es) → R) →ᵃ[R] Fin (n + et) → R

Apply an affine map to the old coordinates and keep an initial segment of the additional coordinates.

Equations

• EGZ.Coord.extendPrefix A es et h = EGZ.Coord.append (A.comp (EGZ.Coord.first m es).toAffineMap) ((EGZ.Coord.prefixMap es et h).toAffineMap.comp (EGZ.Coord.last m es).toAffineMap)

@[simp]

theorem EGZ.Coord.first_extendPrefix {R : Type u_1} [CommRing R] {m n es et : ℕ} (A : (Fin m → R) →ᵃ[R] Fin n → R) (h : et ≤ es) (q : Fin (m + es) → R) : (first n et) ((extendPrefix A es et h) q) = A ((first m es) q)

@[simp]

theorem EGZ.Coord.last_extendPrefix {R : Type u_1} [CommRing R] {m n es et : ℕ} (A : (Fin m → R) →ᵃ[R] Fin n → R) (h : et ≤ es) (q : Fin (m + es) → R) : (last n et) ((extendPrefix A es et h) q) = (prefixMap es et h) ((last m es) q)

theorem EGZ.Coord.extendPrefix_id {R : Type u_1} [CommRing R] (m e : ℕ) : extendPrefix (AffineMap.id R (Fin m → R)) e e ⋯ = AffineMap.id R (Fin (m + e) → R)

theorem EGZ.Coord.extendPrefix_comp {R : Type u_1} [CommRing R] {l m n es em et : ℕ} (A : (Fin m → R) →ᵃ[R] Fin n → R) (B : (Fin l → R) →ᵃ[R] Fin m → R) (hm : em ≤ es) (ht : et ≤ em) : extendPrefix (A.comp B) es et ⋯ = (extendPrefix A em et ht).comp (extendPrefix B es em hm)

noncomputable def EGZ.IntegralAffineMap.extendPrefix {m n : ℕ} (A : IntegralAffineMap m n) (es et : ℕ) (h : et ≤ es) : IntegralAffineMap (m + es) (n + et)

Extend an integral-affine map while retaining an initial segment of its additional coordinates.

Equations

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

theorem EGZ.IntegralAffineMap.first_comp_extendPrefix {m n : ℕ} (A : IntegralAffineMap m n) (es et : ℕ) (h : et ≤ es) : (first n et).comp (A.extendPrefix es et h) = A.comp (first m es)

theorem EGZ.IntegralAffineMap.extendPrefix_id (m e : ℕ) : (id m).extendPrefix e e ⋯ = id (m + e)

theorem EGZ.IntegralAffineMap.extendPrefix_comp {l m n es em et : ℕ} (A : IntegralAffineMap m n) (B : IntegralAffineMap l m) (hm : em ≤ es) (ht : et ≤ em) : (A.comp B).extendPrefix es et ⋯ = (A.extendPrefix em et ht).comp (B.extendPrefix es em hm)