Rational affine images and their faces

Integral affine maps preserve rational points, hence map rational polytopes to rational polytopes. An injective affine map gives an order isomorphism between the source and image face lattices, with explicit carrier formulas. These constructions place a lineage's varying coordinate spaces inside its initial coordinate space for the common-measure face-counting argument.

theorem EGZ.IntegralAffineMap.real_isRational {m n : ℕ} (A : IntegralAffineMap m n) {q : RealCoord m} (hq : IsRational q) : IsRational (A.real q)

noncomputable def EGZ.RationalPolytope.affineImage {m n : ℕ} (P : RationalPolytope m) (A : RealCoord m →ᵃ[ℝ] RealCoord n) (hAq : ∀ (q : RealCoord m), IsRational q → IsRational (A q)) : RationalPolytope n

Image under an affine map which preserves rational coordinates. The image carrier is definitionally the set-theoretic affine image.

Equations

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

@[simp]

theorem EGZ.RationalPolytope.affineImage_carrier {m n : ℕ} (P : RationalPolytope m) (A : RealCoord m →ᵃ[ℝ] RealCoord n) (hAq : ∀ (q : RealCoord m), IsRational q → IsRational (A q)) : (P.affineImage A hAq).carrier = ⇑A '' P.carrier

@[reducible, inline]

noncomputable abbrev EGZ.RationalPolytope.image {m n : ℕ} (P : RationalPolytope m) (A : IntegralAffineMap m n) : RationalPolytope n

Integral affine image of a rational polytope. Injectivity is not needed.

Equations

• P.image A = P.affineImage A.real ⋯

@[simp]

theorem EGZ.RationalPolytope.image_carrier {m n : ℕ} (P : RationalPolytope m) (A : IntegralAffineMap m n) : (P.image A).carrier = ⇑A.real '' P.carrier

theorem EGZ.RationalPolytope.affineImage_subset {l m n : ℕ} (P : RationalPolytope l) (Q : RationalPolytope m) (A : RealCoord l →ᵃ[ℝ] RealCoord n) (B : RealCoord m →ᵃ[ℝ] RealCoord n) (T : RealCoord l →ᵃ[ℝ] RealCoord m) (hAq : ∀ (q : RealCoord l), IsRational q → IsRational (A q)) (hBq : ∀ (q : RealCoord m), IsRational q → IsRational (B q)) (hT : Set.MapsTo (⇑T) P.carrier Q.carrier) (hcomm : ∀ q ∈ P.carrier, A q = B (T q)) : (P.affineImage A hAq).carrier ⊆ (Q.affineImage B hBq).carrier

Commuting maps and source-polytope containment give nested image polytopes even when the two source coordinate dimensions differ.

noncomputable def EGZ.RationalPolytope.Face.affineImage {m n : ℕ} {P : RationalPolytope m} (Γ : P.Face) (A : RealCoord m →ᵃ[ℝ] RealCoord n) (hAq : ∀ (q : RealCoord m), IsRational q → IsRational (A q)) (hA : Function.Injective ⇑A) : (P.affineImage A hAq).Face

An injective affine map carries every exposed face to an exposed face of the image, using an affine left inverse to transport its functional.

Equations

• Γ.affineImage A hAq hA = { carrier := ⇑A '' Γ.carrier, is_exposed := ⋯, nonempty := ⋯ }

@[simp]

theorem EGZ.RationalPolytope.Face.affineImage_carrier {m n : ℕ} {P : RationalPolytope m} (Γ : P.Face) (A : RealCoord m →ᵃ[ℝ] RealCoord n) (hAq : ∀ (q : RealCoord m), IsRational q → IsRational (A q)) (hA : Function.Injective ⇑A) : (Γ.affineImage A hAq hA).carrier = ⇑A '' Γ.carrier

@[reducible, inline]

noncomputable abbrev EGZ.RationalPolytope.Face.image {m n : ℕ} {P : RationalPolytope m} (Γ : P.Face) (A : IntegralAffineMap m n) (hA : Function.Injective ⇑A.real) : (P.image A).Face

Image of a face under an injective integral affine map.

Equations

• Γ.image A hA = Γ.affineImage A.real ⋯ hA

@[simp]

theorem EGZ.RationalPolytope.Face.image_carrier {m n : ℕ} {P : RationalPolytope m} (Γ : P.Face) (A : IntegralAffineMap m n) (hA : Function.Injective ⇑A.real) : (Γ.image A hA).carrier = ⇑A.real '' Γ.carrier

noncomputable def EGZ.RationalPolytope.Face.affineImagePullback {m n : ℕ} {P : RationalPolytope m} (A : RealCoord m →ᵃ[ℝ] RealCoord n) (hAq : ∀ (q : RealCoord m), IsRational q → IsRational (A q)) (Δ : (P.affineImage A hAq).Face) : P.Face

Pull back any face of an image polytope. The image description supplies the required nonemptiness automatically.

Equations

• EGZ.RationalPolytope.Face.affineImagePullback A hAq Δ = Δ.preimage A ⋯ ⋯

@[simp]

theorem EGZ.RationalPolytope.Face.affineImagePullback_carrier {m n : ℕ} {P : RationalPolytope m} (A : RealCoord m →ᵃ[ℝ] RealCoord n) (hAq : ∀ (q : RealCoord m), IsRational q → IsRational (A q)) (Δ : (P.affineImage A hAq).Face) : (affineImagePullback A hAq Δ).carrier = P.carrier ∩ ⇑A ⁻¹' Δ.carrier

@[simp]

theorem EGZ.RationalPolytope.Face.affineImagePullback_affineImage {m n : ℕ} {P : RationalPolytope m} (Γ : P.Face) (A : RealCoord m →ᵃ[ℝ] RealCoord n) (hAq : ∀ (q : RealCoord m), IsRational q → IsRational (A q)) (hA : Function.Injective ⇑A) : affineImagePullback A hAq (Γ.affineImage A hAq hA) = Γ

@[simp]

theorem EGZ.RationalPolytope.Face.affineImage_affineImagePullback {m n : ℕ} {P : RationalPolytope m} (A : RealCoord m →ᵃ[ℝ] RealCoord n) (hAq : ∀ (q : RealCoord m), IsRational q → IsRational (A q)) (hA : Function.Injective ⇑A) (Δ : (P.affineImage A hAq).Face) : (affineImagePullback A hAq Δ).affineImage A hAq hA = Δ

theorem EGZ.RationalPolytope.Face.affineImage_ssubset_iff {m n : ℕ} {P : RationalPolytope m} (Γ Δ : P.Face) (A : RealCoord m →ᵃ[ℝ] RealCoord n) (hAq : ∀ (q : RealCoord m), IsRational q → IsRational (A q)) (hA : Function.Injective ⇑A) : (Γ.affineImage A hAq hA).carrier ⊂ (Δ.affineImage A hAq hA).carrier ↔ Γ.carrier ⊂ Δ.carrier

theorem EGZ.RationalPolytope.Face.image_inter_carrier_eq_iff {m n : ℕ} {P Q : RationalPolytope m} (Γ : P.Face) (Δ : Q.Face) (A : IntegralAffineMap m n) (hA : Function.Injective ⇑A.real) : (Γ.image A hA).carrier ∩ (Q.image A).carrier = (Δ.image A hA).carrier ↔ Γ.carrier ∩ Q.carrier = Δ.carrier

Image coordinates preserve the no-repeated-restricted-face condition when all polytopes are already expressed in one source coordinate space.

noncomputable def EGZ.RationalPolytope.faceAffineImageEquiv {m n : ℕ} (P : RationalPolytope m) (A : RealCoord m →ᵃ[ℝ] RealCoord n) (hAq : ∀ (q : RealCoord m), IsRational q → IsRational (A q)) (hA : Function.Injective ⇑A) : P.Face ≃o (P.affineImage A hAq).Face

The full face lattice is unchanged by injective affine coordinates.

Equations

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

@[reducible, inline]

noncomputable abbrev EGZ.RationalPolytope.faceImageEquiv {m n : ℕ} (P : RationalPolytope m) (A : IntegralAffineMap m n) (hA : Function.Injective ⇑A.real) : P.Face ≃o (P.image A).Face

Order isomorphism between faces of a polytope and its injective affine image.

Equations

• P.faceImageEquiv A hA = P.faceAffineImageEquiv A.real ⋯ hA

theorem EGZ.affineImage_inter_comp_eq_iff {l m n : ℕ} (A : RealCoord m →ᵃ[ℝ] RealCoord n) (T : RealCoord l →ᵃ[ℝ] RealCoord m) (hA : Function.Injective ⇑A) (hT : Function.Injective ⇑T) (S : Set (RealCoord m)) (P Γ : Set (RealCoord l)) : ⇑A '' S ∩ ⇑(A.comp T) '' P = ⇑(A.comp T) '' Γ ↔ P ∩ ⇑T ⁻¹' S = Γ

For two injective coordinate maps, equality of a later image face with the restricted old image face is exactly equality with the pulled-back face. This formula allows the two source coordinate dimensions to differ.