Linear maps

Some definitions and properties of linear, bilinear, and trilinear maps, along with homogeneous quadratic and cubic equations.

def HomogeneousQuadratic (V : Type) [AddCommMonoid V] [Module ℚ V] : Type

The structure defining a homogeneous quadratic equation.

Equations

• HomogeneousQuadratic V = (V →ₑ[fun (a : ℚ) => a ^ 2] ℚ)

instance HomogeneousQuadratic.instFun {V : Type} [AddCommMonoid V] [Module ℚ V] : FunLike (HomogeneousQuadratic V) V ℚ

A homogenous quadratic equation can be treated as a function from V to ℚ.

Equations

• HomogeneousQuadratic.instFun = { coe := fun (f : HomogeneousQuadratic V) => f.toFun, coe_injective' := ⋯ }

theorem HomogeneousQuadratic.map_smul {V : Type} [AddCommMonoid V] [Module ℚ V] (f : HomogeneousQuadratic V) (a : ℚ) (S : V) : f (a • S) = a ^ 2 * f S

structure BiLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends V →ₗ[ℚ] V →ₗ[ℚ] ℚ : Type

The structure of a symmetric bilinear function.

• toFun : V → V →ₗ[ℚ] ℚ
• map_add' (x y : V) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : ℚ) (x : V) : self.toFun (m • x) = (RingHom.id ℚ) m • self.toFun x
• swap' (S T : V) : (self.toFun S) T = (self.toFun T) S

class IsSymmetric {V : Type} [AddCommMonoid V] [Module ℚ V] (f : V →ₗ[ℚ] V →ₗ[ℚ] ℚ) : Prop

A symmetric bilinear function.

• swap (S T : V) : (f S) T = (f T) S

instance BiLinearSymm.instFun (V : Type) [AddCommMonoid V] [Module ℚ V] : FunLike (BiLinearSymm V) V (V →ₗ[ℚ] ℚ)

A symmetric bilinear form can be treated as a function from V to V →ₗ[ℚ] ℚ.

Equations

• BiLinearSymm.instFun V = { coe := fun (f : BiLinearSymm V) => f.toFun, coe_injective' := ⋯ }

def BiLinearSymm.mk₂ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : V × V → ℚ) (map_smul : ∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)) (map_add : ∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)) (swap : ∀ (S T : V), f (S, T) = f (T, S)) : BiLinearSymm V

The construction of a symmetric bilinear map from smul and map_add in the first factor, and swap.

Equations

• BiLinearSymm.mk₂ f map_smul map_add swap = { toFun := fun (S : V) => { toFun := fun (T : V) => f (S, T), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯, swap' := swap }

@[simp]

theorem BiLinearSymm.mk₂_toFun_apply {V : Type} [AddCommMonoid V] [Module ℚ V] (f : V × V → ℚ) (map_smul : ∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)) (map_add : ∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)) (swap : ∀ (S T : V), f (S, T) = f (T, S)) (S T : V) : ((mk₂ f map_smul map_add swap) S) T = f (S, T)

theorem BiLinearSymm.map_smul₁ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : BiLinearSymm V) (a : ℚ) (S T : V) : (f (a • S)) T = a * (f S) T

theorem BiLinearSymm.swap {V : Type} [AddCommMonoid V] [Module ℚ V] (f : BiLinearSymm V) (S T : V) : (f S) T = (f T) S

theorem BiLinearSymm.map_smul₂ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : BiLinearSymm V) (a : ℚ) (S T : V) : (f S) (a • T) = a * (f S) T

theorem BiLinearSymm.map_add₁ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : BiLinearSymm V) (S1 S2 T : V) : (f (S1 + S2)) T = (f S1) T + (f S2) T

theorem BiLinearSymm.map_add₂ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : BiLinearSymm V) (S T1 T2 : V) : (f S) (T1 + T2) = (f S) T1 + (f S) T2

def BiLinearSymm.toLinear₁ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : BiLinearSymm V) (T : V) : V →ₗ[ℚ] ℚ

Fixing the second input vectors, the resulting linear map.

Equations

• f.toLinear₁ T = { toFun := fun (S : V) => (f S) T, map_add' := ⋯, map_smul' := ⋯ }

theorem BiLinearSymm.toLinear₁_apply {V : Type} [AddCommMonoid V] [Module ℚ V] (f : BiLinearSymm V) (S T : V) : (f S) T = (f.toLinear₁ T) S

theorem BiLinearSymm.map_sum₁ {V : Type} [AddCommMonoid V] [Module ℚ V] {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V) : (f (∑ i : Fin n, S i)) T = ∑ i : Fin n, (f (S i)) T

theorem BiLinearSymm.map_sum₂ {V : Type} [AddCommMonoid V] [Module ℚ V] {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V) : (f T) (∑ i : Fin n, S i) = ∑ i : Fin n, (f T) (S i)

def BiLinearSymm.toHomogeneousQuad {V : Type} [AddCommMonoid V] [Module ℚ V] (τ : BiLinearSymm V) : HomogeneousQuadratic V

The homogenous quadratic equation obtainable from a bilinear function.

Equations

• τ.toHomogeneousQuad = { toFun := fun (S : V) => (τ S) S, map_smul' := ⋯ }

@[simp]

theorem BiLinearSymm.toHomogeneousQuad_apply {V : Type} [AddCommMonoid V] [Module ℚ V] (τ : BiLinearSymm V) (S : V) : τ.toHomogeneousQuad S = (τ S) S

theorem BiLinearSymm.toHomogeneousQuad_add {V : Type} [AddCommMonoid V] [Module ℚ V] (τ : BiLinearSymm V) (S T : V) : τ.toHomogeneousQuad (S + T) = τ.toHomogeneousQuad S + τ.toHomogeneousQuad T + 2 * (τ S) T

def HomogeneousCubic (V : Type) [AddCommMonoid V] [Module ℚ V] : Type

The structure of a homogeneous cubic equation.

Equations

• HomogeneousCubic V = (V →ₑ[fun (a : ℚ) => a ^ 3] ℚ)

instance HomogeneousCubic.instFun {V : Type} [AddCommMonoid V] [Module ℚ V] : FunLike (HomogeneousCubic V) V ℚ

A homogenous cubic equation can be treated as a function from V to ℚ.

Equations

• HomogeneousCubic.instFun = { coe := fun (f : HomogeneousCubic V) => f.toFun, coe_injective' := ⋯ }

theorem HomogeneousCubic.map_smul {V : Type} [AddCommMonoid V] [Module ℚ V] (f : HomogeneousCubic V) (a : ℚ) (S : V) : f (a • S) = a ^ 3 * f S

structure TriLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends V →ₗ[ℚ] V →ₗ[ℚ] V →ₗ[ℚ] ℚ : Type

The structure of a symmetric trilinear function.

• toFun : V → V →ₗ[ℚ] V →ₗ[ℚ] ℚ
• map_add' (x y : V) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : ℚ) (x : V) : self.toFun (m • x) = (RingHom.id ℚ) m • self.toFun x
• swap₁' (S T L : V) : ((self.toFun S) T) L = ((self.toFun T) S) L
• swap₂' (S T L : V) : ((self.toFun S) T) L = ((self.toFun S) L) T

instance TriLinearSymm.instFun {V : Type} [AddCommMonoid V] [Module ℚ V] : FunLike (TriLinearSymm V) V (V →ₗ[ℚ] V →ₗ[ℚ] ℚ)

A symmetric trilinear form can be treated as a function from V to V →ₗ[ℚ] V →ₗ[ℚ] ℚ.

Equations

• TriLinearSymm.instFun = { coe := fun (f : TriLinearSymm V) => f.toFun, coe_injective' := ⋯ }

def TriLinearSymm.mk₃ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : V × V × V → ℚ) (map_smul : ∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)) (map_add : ∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)) (swap₁ : ∀ (S T L : V), f (S, T, L) = f (T, S, L)) (swap₂ : ∀ (S T L : V), f (S, T, L) = f (S, L, T)) : TriLinearSymm V

The construction of a symmetric trilinear map from smul and map_add in the first factor, and two swap.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TriLinearSymm.mk₃_toFun_apply_apply {V : Type} [AddCommMonoid V] [Module ℚ V] (f : V × V × V → ℚ) (map_smul : ∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)) (map_add : ∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)) (swap₁ : ∀ (S T L : V), f (S, T, L) = f (T, S, L)) (swap₂ : ∀ (S T L : V), f (S, T, L) = f (S, L, T)) (S S✝ T : V) : (((mk₃ f map_smul map_add swap₁ swap₂) S) S✝) T = f (S, S✝, T)

theorem TriLinearSymm.swap₁ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (S T L : V) : ((f S) T) L = ((f T) S) L

theorem TriLinearSymm.swap₂ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (S T L : V) : ((f S) T) L = ((f S) L) T

theorem TriLinearSymm.swap₃ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (S T L : V) : ((f S) T) L = ((f L) T) S

theorem TriLinearSymm.map_smul₁ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (a : ℚ) (S T L : V) : ((f (a • S)) T) L = a * ((f S) T) L

theorem TriLinearSymm.map_smul₂ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (S : V) (a : ℚ) (T L : V) : ((f S) (a • T)) L = a * ((f S) T) L

theorem TriLinearSymm.map_smul₃ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (S T : V) (a : ℚ) (L : V) : ((f S) T) (a • L) = a * ((f S) T) L

theorem TriLinearSymm.map_add₁ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (S1 S2 T L : V) : ((f (S1 + S2)) T) L = ((f S1) T) L + ((f S2) T) L

theorem TriLinearSymm.map_add₂ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (S T1 T2 L : V) : ((f S) (T1 + T2)) L = ((f S) T1) L + ((f S) T2) L

theorem TriLinearSymm.map_add₃ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (S T L1 L2 : V) : ((f S) T) (L1 + L2) = ((f S) T) L1 + ((f S) T) L2

def TriLinearSymm.toLinear₁ {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (T L : V) : V →ₗ[ℚ] ℚ

Fixing the second and third input vectors, the resulting linear map.

Equations

• f.toLinear₁ T L = { toFun := fun (S : V) => ((f S) T) L, map_add' := ⋯, map_smul' := ⋯ }

theorem TriLinearSymm.toLinear₁_apply {V : Type} [AddCommMonoid V] [Module ℚ V] (f : TriLinearSymm V) (S T L : V) : ((f S) T) L = (f.toLinear₁ T L) S

theorem TriLinearSymm.map_sum₁ {V : Type} [AddCommMonoid V] [Module ℚ V] {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T L : V) : ((f (∑ i : Fin n, S i)) T) L = ∑ i : Fin n, ((f (S i)) T) L

theorem TriLinearSymm.map_sum₂ {V : Type} [AddCommMonoid V] [Module ℚ V] {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T L : V) : ((f T) (∑ i : Fin n, S i)) L = ∑ i : Fin n, ((f T) (S i)) L

theorem TriLinearSymm.map_sum₃ {V : Type} [AddCommMonoid V] [Module ℚ V] {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T L : V) : ((f T) L) (∑ i : Fin n, S i) = ∑ i : Fin n, ((f T) L) (S i)

theorem TriLinearSymm.map_sum₁₂₃ {V : Type} [AddCommMonoid V] [Module ℚ V] {n1 n2 n3 : ℕ} (f : TriLinearSymm V) (S : Fin n1 → V) (T : Fin n2 → V) (L : Fin n3 → V) : ((f (∑ i : Fin n1, S i)) (∑ i : Fin n2, T i)) (∑ i : Fin n3, L i) = ∑ i : Fin n1, ∑ k : Fin n2, ∑ l : Fin n3, ((f (S i)) (T k)) (L l)

def TriLinearSymm.toCubic {charges : Type} [AddCommMonoid charges] [Module ℚ charges] (τ : TriLinearSymm charges) : HomogeneousCubic charges

The homogenous cubic equation obtainable from a symmetric trilinear function.

Equations

• τ.toCubic = { toFun := fun (S : charges) => ((τ S) S) S, map_smul' := ⋯ }

@[simp]

theorem TriLinearSymm.toCubic_apply {charges : Type} [AddCommMonoid charges] [Module ℚ charges] (τ : TriLinearSymm charges) (S : charges) : τ.toCubic S = ((τ S) S) S

theorem TriLinearSymm.toCubic_add {charges : Type} [AddCommMonoid charges] [Module ℚ charges] (τ : TriLinearSymm charges) (S T : charges) : τ.toCubic (S + T) = τ.toCubic S + τ.toCubic T + 3 * ((τ S) S) T + 3 * ((τ T) T) S