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,

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

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.

Equations

• LinearMap.transvection f v = { toFun := fun (x : V) => x + f x • v, map_add' := ⋯, map_smul' := ⋯ }

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.

Equations

• LinearEquiv.transvection h = { toFun := ⇑(LinearMap.transvection f v), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(LinearMap.transvection f (-v)), left_inv := ⋯, right_inv := ⋯ }

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.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 LinearMap.transvection.baseChange {R : Type u_3} {V : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] {A : Type u_5} [CommRing 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 LinearEquiv.transvection.baseChange {R : Type u_3} {V : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] {A : Type u_5} [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

@[simp]

theorem IsBaseChange.transvection {R : Type u_3} {V : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] {A : Type u_5} [CommRing 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)