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.

def LinearMap.transvection {R : Type u_1} {V : Type u_2} [CommSemiring 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. It is only a transvection when f v = 0. See also Module.preReflection.

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} [CommSemiring 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} [CommSemiring 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} [CommSemiring 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} [CommSemiring 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} [CommSemiring 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} [CommSemiring 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} [CommSemiring R] [AddCommMonoid V] [Module R V] (f : Module.Dual R V) : transvection f 0 = id

theorem LinearMap.transvection.congr {R : Type u_1} {V : Type u_2} [CommSemiring 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} [CommRing 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} [CommRing 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} [CommRing 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} [CommRing 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} [CommRing 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} [CommRing 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} [CommRing 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} [CommRing 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} [CommRing 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} [CommRing 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'