Injective coordinate transport at equal levels

If a new represented space is contained in an old one and an integral coordinate map factors the old representation through the new one, equal levels force equal spaces and equal ranks. The factor is then bijective modulo the prime, injective on integer lattices, and bijective over the reals.

theorem EGZ.FpRepresentation.factor_modp_injective_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (A : FpCoord p (G.rank y) →ᵃ[ZMod p] FpCoord p (F.rank x)) (hspace : T.space y ≤ R.space x) (hfactor : ∀ v ∈ T.space y, (R.map x) v = A ((T.map y) v)) (hlevel : R.level x = T.level y) : Function.Injective ⇑A

At equal levels, any affine factor between the coordinate spaces is injective over the represented field.

theorem EGZ.FpRepresentation.factor_real_injective_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (A : IntegralAffineMap (G.rank y) (F.rank x)) (hspace : T.space y ≤ R.space x) (hfactor : ∀ v ∈ T.space y, (R.map x) v = (A.modp p) ((T.map y) v)) (hlevel : R.level x = T.level y) : Function.Injective ⇑A.real

theorem EGZ.FpRepresentation.factor_integer_injective_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (A : IntegralAffineMap (G.rank y) (F.rank x)) (hspace : T.space y ≤ R.space x) (hfactor : ∀ v ∈ T.space y, (R.map x) v = (A.modp p) ((T.map y) v)) (hlevel : R.level x = T.level y) : Function.Injective A.integer

theorem EGZ.FpRepresentation.factor_real_bijective_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (A : IntegralAffineMap (G.rank y) (F.rank x)) (hspace : T.space y ≤ R.space x) (hfactor : ∀ v ∈ T.space y, (R.map x) v = (A.modp p) ((T.map y) v)) (hlevel : R.level x = T.level y) : Function.Bijective ⇑A.real

Real coordinate transport at an unchanged level is an affine isomorphism; lattice indices need not be one.

theorem EGZ.FpRepresentation.transition_real_injective_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) {y x : F.Node} (h : y ≤ x) (heq : R.level y = R.level x) : Function.Injective ⇑(F.transition h).real

theorem EGZ.FpRepresentation.transition_integer_injective_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) {y x : F.Node} (h : y ≤ x) (heq : R.level y = R.level x) : Function.Injective (F.transition h).integer