Transvections in a module

• When f : Module.Dual R V and v : V, LinearMap.transvection f v is the linear map given by x ↦ x + f x • v,

• LinearMap.transvection.det shows that the determinant of LinearMap.transvection f v is equal to 1 + f v.

• If, moreover, f v = 0, then LinearEquiv.transvection shows that it is a linear equivalence.

• LinearMap.transvections R V: the set of transvections.

• LinearEquiv.dilatransvections R V: the set of linear equivalences whose associated linear map is of the form LinearMap.transvection f v.

• LinearEquiv.transvection.det shows that it has determinant 1.

Note on terminology

In the mathematical litterature, linear maps of the form LinearMap.transvection f v are only called “transvections” when f v = 0. Otherwise, they are sometimes called “dilations” (especially if f v ≠ -1).

The definition is almost the same as that of Module.preReflection f v, up to a sign change, which are interesting when f v = 2, because they give “reflections”.

def LinearMap.transvection {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] (f : Module.Dual R V) (v : V) : V →ₗ[R] V

The transvection associated with a linear form f and a vector v.

NB. In mathematics, these linear maps are only called “transvections” when f v = 0. See also Module.preReflection for a similar definition, up to a sign.

theorem LinearMap.transvection.apply {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] (f : Module.Dual R V) (v x : V) : (transvection f v) x = x + f x • v

theorem LinearMap.transvection.comp_of_left_eq_apply {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] {f : Module.Dual R V} {v w x : V} (hw : f w = 0) : (transvection f v) ((transvection f w) x) = (transvection f (v + w)) x

theorem LinearMap.transvection.comp_of_left_eq {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] {f : Module.Dual R V} {v w : V} (hw : f w = 0) : transvection f v ∘ₗ transvection f w = transvection f (v + w)

theorem LinearMap.transvection.comp_of_right_eq_apply {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] {f g : Module.Dual R V} {v x : V} (hf : f v = 0) : (transvection f v) ((transvection g v) x) = (transvection (f + g) v) x

theorem LinearMap.transvection.comp_of_right_eq {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] {f g : Module.Dual R V} {v : V} (hf : f v = 0) : transvection f v ∘ₗ transvection g v = transvection (f + g) v

@[simp]

theorem LinearMap.transvection.of_left_eq_zero {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] (v : V) : transvection 0 v = id

@[simp]

theorem LinearMap.transvection.of_right_eq_zero {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] (f : Module.Dual R V) : transvection f 0 = id

theorem LinearMap.transvection.eq_id_of_finrank_le_one {R : Type u_3} {V : Type u_4} [CommSemiring R] [AddCommMonoid V] [Module R V] [Module.Free R V] [Module.Finite R V] [StrongRankCondition R] {f : Module.Dual R V} {v : V} (hfv : f v = 0) (h1 : Module.finrank R V ≤ 1) : transvection f v = id

theorem LinearMap.transvection.congr {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] {W : Type u_3} [AddCommMonoid W] [Module R W] (f : Module.Dual R V) (v : V) (e : V ≃ₗ[R] W) : ↑e ∘ₗ transvection f v ∘ₗ ↑e.symm = (f ∘ₗ ↑e.symm).transvection (e v)

def LinearEquiv.transvection {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v : V} (h : f v = 0) : V ≃ₗ[R] V

The transvection associated with a linear form f and a vector v such that f v = 0.

theorem LinearEquiv.transvection.apply {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v : V} (h : f v = 0) (x : V) : (transvection h) x = x + f x • v

@[simp]

theorem LinearEquiv.transvection.coe_toLinearMap {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v : V} (h : f v = 0) : ↑(transvection h) = LinearMap.transvection f v

@[simp]

theorem LinearEquiv.transvection.coe_apply {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v x : V} {h : f v = 0} : (transvection h) x = (LinearMap.transvection f v) x

theorem LinearEquiv.transvection.trans_of_left_eq {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v w : V} (hv : f v = 0) (hw : f w = 0) (hvw : f (v + w) = 0 := by simp [hv, hw]) : transvection hw ≪≫ₗ transvection hv = transvection hvw

theorem LinearEquiv.transvection.trans_of_right_eq {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f g : Module.Dual R V} {v : V} (hf : f v = 0) (hg : g v = 0) (hfg : (f + g) v = 0 := by simp [hf, hg]) : transvection hg ≪≫ₗ transvection hf = transvection hfg

@[simp]

theorem LinearEquiv.transvection.of_left_eq_zero {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] (v : V) (hv : 0 v = 0 := ⋯) : transvection hv = refl R V

@[simp]

theorem LinearEquiv.transvection.of_right_eq_zero {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] (f : Module.Dual R V) (hf : f 0 = 0 := ⋯) : transvection hf = refl R V

theorem LinearEquiv.transvection.symm_eq {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v : V} (hv : f v = 0) (hv' : f (-v) = 0 := by simp [hv]) : (transvection hv).symm = transvection hv'

theorem LinearEquiv.transvection.inv_eq {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v : V} (hv : f v = 0) (hv' : f (-v) = 0 := by simp [hv]) : (transvection hv)⁻¹ = transvection hv'

theorem LinearEquiv.transvection.symm_eq' {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v : V} (hf : f v = 0) (hf' : (-f) v = 0 := by simp [hf]) : (transvection hf).symm = transvection hf'

theorem LinearEquiv.transvection.inv_eq' {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v : V} (hf : f v = 0) (hf' : (-f) v = 0 := by simp [hf]) : (transvection hf)⁻¹ = transvection hf'

def LinearEquiv.transvections (R : Type u_1) (V : Type u_2) [Ring R] [AddCommGroup V] [Module R V] : Set (V ≃ₗ[R] V)

The set of transvections in the group of linear equivalences

theorem LinearEquiv.mem_transvections_iff {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {e : V ≃ₗ[R] V} : e ∈ transvections R V ↔ ∃ (f : Module.Dual R V) (v : V) (hfv : f v = 0), e = transvection hfv

@[simp]

theorem LinearEquiv.mem_transvections {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v : V} (hfv : f v = 0) : transvection hfv ∈ transvections R V

@[simp]

theorem LinearEquiv.refl_mem_transvections {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] : refl R V ∈ transvections R V

@[simp]

theorem LinearEquiv.one_mem_transvections {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] : 1 ∈ transvections R V

@[simp]

theorem LinearEquiv.symm_mem_transvections_iff {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {e : V ≃ₗ[R] V} : e.symm ∈ transvections R V ↔ e ∈ transvections R V

@[simp]

theorem LinearEquiv.inv_mem_transvections_iff {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {e : V ≃ₗ[R] V} : e⁻¹ ∈ transvections R V ↔ e ∈ transvections R V

theorem LinearEquiv.transvections_pow_mono {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] : Monotone fun (n : ℕ) => transvections R V ^ n

def LinearEquiv.dilatransvections (R : Type u_1) (V : Type u_2) [Ring R] [AddCommGroup V] [Module R V] : Set (V ≃ₗ[R] V)

Dilatransvections are linear equivalences V ≃ₗ[R] V whose associated linear map are given by LinearMap.transvection, i.e., are of the form x ↦ x + f x • v for f : Dual R V and v : V.

Over a division ring, LinearEquiv.mem_dilatransvections_iff_rank shows that they correspond to the linear equivalences which differ from the identity map by a linear map of rank at most 1.

theorem LinearEquiv.transvections_subset_dilatransvections {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] : transvections R V ⊆ dilatransvections R V

@[simp]

theorem LinearEquiv.refl_mem_dilatransvections {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] : refl R V ∈ dilatransvections R V

@[simp]

theorem LinearEquiv.one_mem_dilatransvections {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] : 1 ∈ dilatransvections R V

@[simp]

theorem LinearEquiv.symm_mem_dilatransvections_iff {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {e : V ≃ₗ[R] V} : e.symm ∈ dilatransvections R V ↔ e ∈ dilatransvections R V

@[simp]

theorem LinearEquiv.inv_mem_dilatransvections_iff {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {e : V ≃ₗ[R] V} : e⁻¹ ∈ dilatransvections R V ↔ e ∈ dilatransvections R V

theorem LinearEquiv.dilatransvections_pow_mono {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] : Monotone fun (n : ℕ) => dilatransvections R V ^ n

theorem LinearEquiv.mem_dilatransvections_iff_rank {V : Type u_2} [AddCommGroup V] {K : Type u_3} [DivisionRing K] [Module K V] {e : V ≃ₗ[K] V} : e ∈ dilatransvections K V ↔ Module.rank K ↥(↑e - LinearMap.id).range ≤ 1

Over a division ring, dilatransvections correspond to linear equivalences e such that the linear map e - id has rank at most 1.

See also LinearEquiv.mem_dilatransvections_iff_finrank.

theorem LinearEquiv.mem_dilatransvections_iff_finrank {V : Type u_2} [AddCommGroup V] {K : Type u_3} [DivisionRing K] [Module K V] [Module.Finite K V] {e : V ≃ₗ[K] V} : e ∈ dilatransvections K V ↔ Module.finrank K ↥(↑e - LinearMap.id).range ≤ 1

Over a division ring, dilatransvections correspond to linear equivalences e such that the linear map e - id has rank at most 1.

See also LinearEquiv.mem_dilatransvections_iff_rank.

theorem LinearMap.transvection.baseChange {R : Type u_3} {V : Type u_4} [CommSemiring R] [AddCommMonoid V] [Module R V] (A : Type u_5) [CommSemiring A] [Algebra R A] (f : Module.Dual R V) (v : V) : LinearMap.baseChange A (transvection f v) = transvection ((Module.Dual.baseChange A) f) (1 ⊗ₜ[R] v)

theorem IsBaseChange.transvection {R : Type u_3} {V : Type u_4} [CommSemiring R] [AddCommMonoid V] [Module R V] (A : Type u_5) [CommSemiring A] [Algebra R A] {W : Type u_6} [AddCommMonoid W] [Module R W] [Module A W] [IsScalarTower R A W] {ε : V →ₗ[R] W} (ibc : IsBaseChange A ε) (f : Module.Dual R V) (v : V) : ibc.endHom (LinearMap.transvection f v) = LinearMap.transvection (ibc.toDual f) (ε v)

theorem LinearEquiv.transvection.baseChange {R : Type u_3} {V : Type u_4} {A : Type u_5} [CommRing R] [AddCommGroup V] [Module R V] [CommRing A] [Algebra R A] {f : Module.Dual R V} {v : V} (h : f v = 0) (hA : ((Module.Dual.baseChange A) f) (1 ⊗ₜ[R] v) = 0 := by simp [Algebra.algebraMap_eq_smul_one]) : LinearEquiv.baseChange R A V V (transvection h) = transvection hA

theorem LinearEquiv.dilatransvection.baseChange {R : Type u_3} {V : Type u_4} {A : Type u_5} [CommRing R] [AddCommGroup V] [Module R V] [CommRing A] [Algebra R A] (e : V ≃ₗ[R] V) (he : e ∈ dilatransvections R V) : LinearEquiv.baseChange R A V V e ∈ dilatransvections A (TensorProduct R A V)

@[simp]

theorem LinearMap.transvection.det {R : Type u_3} {V : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (f : Module.Dual R V) (v : V) : LinearMap.det (transvection f v) = 1 + f v

@[simp]

theorem LinearEquiv.transvection.det_eq_one {R : Type u_3} {V : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] {f : Module.Dual R V} {v : V} (hfv : f v = 0) : LinearEquiv.det (transvection hfv) = 1

Determinant of a transvection.

It is not necessary to assume that the module is finite and free because LinearMap.det is identically 1 otherwise.