Transvection automorphisms and their action on lattices

If b = (b₀, b₁) is a basis of a two-dimensional K-vector space V and x : K a scalar, we have a transvection automorphism of V given by b₀ ↦ b₀ and b₁ ↦ x • b₀ + b₁. In the coordinate system induced by b, this is a transvection by x.

We call the basis representing this automorphism the unipotent matrix associated to b and x.

Main definitions

• Basis.transvect: The basis of K^2 given by the image of b under the transvection automorphism.
• Basis.transvectEquiv: The transvection automorphism induced by b and x.
• Basis.unipotent: The unipotent matrix realising the transvection automorphism.

Main results

• unipotent_pow_irred_smul_eq_submodule: If b = (b₀, b₁) is a basis of K^2, then the submodule spanned by (ϖ ^ k • b₀, b₁) is invariant under the action of b.unipotent (ϖ ^ n * x) if n ≥ k.

noncomputable def Module.Basis.transvect {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (b : Basis (Fin 2) K V) (x : K) : Basis (Fin 2) K V

Given a basis b = (b₀, b₁) of a K-vector space V and an element x : K, this is the basis (b₀, x • b₀ + b₁) of V. Hence, this is a transvection in the coordinate system induced by b.

Equations

• b.transvect x = Module.Basis.mk ⋯ ⋯

@[simp]

theorem Module.Basis.transvect_apply₀ {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (b : Basis (Fin 2) K V) (x : K) : (b.transvect x) 0 = b 0

@[simp]

theorem Module.Basis.transvect_apply₁ {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (b : Basis (Fin 2) K V) (x : K) : (b.transvect x) 1 = x • b 0 + b 1

noncomputable def Module.Basis.transvect' {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : Basis (Fin 2) K (Fin 2 → K)

Special case of Basis.transvect for V = Fin 2 → K for ease of application.

Equations

• b.transvect' x = b.transvect ↑x

@[simp]

theorem Module.Basis.transvect'_apply₀ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : (b.transvect' x) 0 = b 0

@[simp]

theorem Module.Basis.transvect'_apply₁ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : (b.transvect' x) 1 = x • b 0 + b 1

noncomputable def Module.Basis.transvectEquiv {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : (Fin 2 → K) ≃ₗ[K] Fin 2 → K

The K-automorphism of Fin 2 → K induced by sending b to the transvection of b by x.

Equations

• b.transvectEquiv x = b.equiv (b.transvect' x) (Equiv.refl (Fin 2))

@[simp]

theorem Module.Basis.transvectEquiv_apply₀ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : (b.transvectEquiv x) (b 0) = b 0

@[simp]

theorem Module.Basis.transvectEquiv_apply₁ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : (b.transvectEquiv x) (b 1) = x • b 0 + b 1

theorem Module.Basis.transvectEquiv_pow_irred_mul_eq {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (n : ℕ) {ϖ : ↥R} (hϖ : Irreducible ϖ) : b.transvectEquiv (ϖ ^ n * x) = (b.ntwist₂ hϖ n 0).transvectEquiv x

noncomputable def Module.Basis.unipotent {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : GL (Fin 2) K

The basis associated to the transvection automorphism Basis.transvectEquiv induced by x. In the coordinate system of b, this is the upper triangular matrix with 1 on the diagonal and x in the top-right.

Equations

• b.unipotent x = Matrix.GeneralLinearGroup.toLin.symm (LinearMap.GeneralLinearGroup.ofLinearEquiv (b.transvectEquiv x))

theorem Module.Basis.unipotent_mulVec {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (y : Fin 2 → K) : (↑(b.unipotent x)).mulVec y = (b.transvectEquiv x) y

theorem Module.Basis.unipotent_pow_irred_mul_eq {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (n : ℕ) {ϖ : ↥R} (hϖ : Irreducible ϖ) : b.unipotent (ϖ ^ n * x) = (b.ntwist₂ hϖ n 0).unipotent x

theorem unipotent_pow_irred_smul_eq_submodule {K : Type u_1} [Field K] {R : Subring K} {ϖ : ↥R} (hϖ : Irreducible ϖ) (b : Module.Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (k n : ℕ) (hkn : k ≤ n) : b.unipotent (ϖ ^ n * x) • (b.ntwist₂ hϖ k 0).toSubmodule = (b.ntwist₂ hϖ k 0).toSubmodule

If b = (b₀, b₁) is a basis of K^2, then the submodule spanned by (ϖ ^ k • b₀, b₁) is invariant under the action of b.unipotent (ϖ ^ n * x) if n ≥ k.

This is used in Lattice.exists_GL_forall_smul_eq_ntwist₂_of_isSimpleChain_cons: We use such unipotent matrices to inductively bring a simple chain of lattices in standard form. This makes sure that in the n + 1th step, multiplying with a unipotent matrix does not change the first n terms of the chain.

See unipotent_pow_irred_smul_eq for a version for Basis.toLattice.

theorem unipotent_pow_irred_smul_eq {K : Type u_1} [Field K] {R : Subring K} {ϖ : ↥R} (hϖ : Irreducible ϖ) (b : Module.Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (k n : ℕ) (hkn : k ≤ n) : b.unipotent (ϖ ^ n * x) • (b.ntwist₂ hϖ k 0).toLattice = (b.ntwist₂ hϖ k 0).toLattice

Version of unipotent_pow_irred_smul_eq_submodule for Basis.toLattice.

theorem Module.Basis.transvectEquiv_mem_of_mem {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (y : Fin 2 → K) (hy : y ∈ b.toSubmodule) : (b.transvectEquiv x) y ∈ b.toSubmodule

theorem Module.Basis.transvectEquiv_symm_mem_of_mem {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (y : Fin 2 → K) (hy : y ∈ b.toSubmodule) : (b.transvectEquiv x).symm y ∈ b.toSubmodule