mathlib3 documentation

monlib / linear_algebra.my_ips.strict

Strict tensor product (wip) #

@[instance]

def tensor_product.assoc_has_coe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [comm_semiring R] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module R E] [module R F] [module R G] :

has_coe (tensor_product R (tensor_product R E F) G) (tensor_product R E (tensor_product R F G))

Equations

tensor_product.assoc_has_coe = {coe := λ (x : tensor_product R (tensor_product R E F) G), ⇑(tensor_product.assoc R E F G) x}

@[instance]

def tensor_product.assoc_symm_has_coe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [comm_semiring R] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module R E] [module R F] [module R G] :

has_coe (tensor_product R E (tensor_product R F G)) (tensor_product R (tensor_product R E F) G)

Equations

tensor_product.assoc_symm_has_coe = {coe := λ (x : tensor_product R E (tensor_product R F G)), ⇑((tensor_product.assoc R E F G).symm) x}

@[simp]

theorem tensor_product.assoc_tmul_coe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [comm_semiring R] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module R E] [module R F] [module R G] (a : E) (b : F) (c : G) :

a ⊗ₜ[R] b ⊗ₜ[R] c = ↑(a ⊗ₜ[R] (b ⊗ₜ[R] c))

theorem tensor_product.assoc_coe_coe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [comm_semiring R] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module R E] [module R F] [module R G] (a : tensor_product R (tensor_product R E F) G) :

@[simp]

theorem tensor_product.tmul_assoc_coe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [comm_semiring R] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module R E] [module R F] [module R G] (a : E) (b : F) (c : G) :

a ⊗ₜ[R] (b ⊗ₜ[R] c) = ↑(a ⊗ₜ[R] b ⊗ₜ[R] c)

theorem tensor_product.coe_coe_assoc {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [comm_semiring R] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module R E] [module R F] [module R G] (a : tensor_product R E (tensor_product R F G)) :

@[instance]

def tensor_product.lid_has_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] :

has_coe (tensor_product R R E) E

Equations

tensor_product.lid_has_coe = {coe := λ (x : tensor_product R R E), ⇑(tensor_product.lid R E) x}

@[instance]

def tensor_product.rid_has_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] :

has_coe (tensor_product R E R) E

Equations

tensor_product.rid_has_coe = {coe := λ (x : tensor_product R E R), ⇑(tensor_product.rid R E) x}

@[instance]

def tensor_product.lid_symm_has_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] :

has_coe E (tensor_product R R E)

Equations

tensor_product.lid_symm_has_coe = {coe := λ (x : E), ⇑((tensor_product.lid R E).symm) x}

@[instance]

def tensor_product.rid_symm_has_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] :

has_coe E (tensor_product R E R)

Equations

tensor_product.rid_symm_has_coe = {coe := λ (x : E), ⇑((tensor_product.rid R E).symm) x}

theorem tensor_product.lid_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] (x : E) (r : R) :

↑(r ⊗ₜ[R] x) = r • x

theorem tensor_product.rid_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] (x : E) (r : R) :

↑(x ⊗ₜ[R] r) = r • x

theorem tensor_product.lid_symm_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] (x : E) :

↑x = 1 ⊗ₜ[R] x

theorem tensor_product.rid_symm_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] (x : E) :

↑x = x ⊗ₜ[R] 1

theorem tensor_product.lid_coe' {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] (x : E) (r : R) :

r ⊗ₜ[R] x = r • ↑x

theorem tensor_product.rid_coe' {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] (x : E) (r : R) :

x ⊗ₜ[R] r = r • ↑x

theorem tensor_product.lid_coe_rid_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] (x : E) :

@[instance]

def fun_tensor_product_assoc_has_coe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [comm_semiring R] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module R E] [module R F] [module R G] {A : Type u_5} :

has_coe (tensor_product R (tensor_product R E F) G → A) (tensor_product R E (tensor_product R F G) → A)

Equations

fun_tensor_product_assoc_has_coe = {coe := λ (f : tensor_product R (tensor_product R E F) G → A) (x : tensor_product R E (tensor_product R F G)), f ↑x}

@[instance]

def linear_map.tensor_product_assoc_has_coe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [comm_semiring R] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module R E] [module R F] [module R G] {A : Type u_5} [add_comm_monoid A] [module R A] :

has_coe (tensor_product R (tensor_product R E F) G →ₗ[R] A) (tensor_product R E (tensor_product R F G) →ₗ[R] A)

Equations

linear_map.tensor_product_assoc_has_coe = {coe := λ (f : tensor_product R (tensor_product R E F) G →ₗ[R] A), f.comp ↑((tensor_product.assoc R E F G).symm)}

@[instance]

def fun_tensor_product_assoc_has_coe' {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [comm_semiring R] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module R E] [module R F] [module R G] {A : Type u_5} :

has_coe (tensor_product R E (tensor_product R F G) → A) (tensor_product R (tensor_product R E F) G → A)

Equations

fun_tensor_product_assoc_has_coe' = {coe := λ (f : tensor_product R E (tensor_product R F G) → A) (x : tensor_product R (tensor_product R E F) G), f ↑x}

@[instance]

def linear_map.tensor_product_assoc_has_coe' {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [comm_semiring R] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module R E] [module R F] [module R G] {A : Type u_5} [add_comm_monoid A] [module R A] :

has_coe (tensor_product R E (tensor_product R F G) →ₗ[R] A) (tensor_product R (tensor_product R E F) G →ₗ[R] A)

Equations

linear_map.tensor_product_assoc_has_coe' = {coe := λ (f : tensor_product R E (tensor_product R F G) →ₗ[R] A), f.comp ↑(tensor_product.assoc R E F G)}

@[instance]

def fun_lid_has_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} :

has_coe (tensor_product R R E → A) (E → A)

Equations

fun_lid_has_coe = {coe := λ (f : tensor_product R R E → A) (x : E), f ↑x}

@[instance]

def linear_map.tensor_product_lid_has_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} [add_comm_monoid A] [module R A] :

has_coe (tensor_product R R E →ₗ[R] A) (E →ₗ[R] A)

Equations

linear_map.tensor_product_lid_has_coe = {coe := λ (f : tensor_product R R E →ₗ[R] A), f.comp ↑((tensor_product.lid R E).symm)}

@[instance]

def fun_lid_has_coe' {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} :

has_coe (E → A) (tensor_product R R E → A)

Equations

fun_lid_has_coe' = {coe := λ (f : E → A) (x : tensor_product R R E), f ↑x}

@[instance]

def linear_map.tensor_product_lid_has_coe' {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} [add_comm_monoid A] [module R A] :

has_coe (E →ₗ[R] A) (tensor_product R R E →ₗ[R] A)

Equations

linear_map.tensor_product_lid_has_coe' = {coe := λ (f : E →ₗ[R] A), f.comp ↑(tensor_product.lid R E)}

@[instance]

def fun_rid_has_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} :

has_coe (tensor_product R E R → A) (E → A)

Equations

fun_rid_has_coe = {coe := λ (f : tensor_product R E R → A) (x : E), f ↑x}

@[instance]

def linear_map.tensor_product_rid_has_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} [add_comm_monoid A] [module R A] :

has_coe (tensor_product R E R →ₗ[R] A) (E →ₗ[R] A)

Equations

linear_map.tensor_product_rid_has_coe = {coe := λ (f : tensor_product R E R →ₗ[R] A), f.comp ↑((tensor_product.rid R E).symm)}

@[instance]

def fun_rid_has_coe' {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} :

has_coe (E → A) (tensor_product R E R → A)

Equations

fun_rid_has_coe' = {coe := λ (f : E → A) (x : tensor_product R E R), f ↑x}

@[instance]

def linear_map.tensor_product_rid_has_coe' {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} [add_comm_monoid A] [module R A] :

has_coe (E →ₗ[R] A) (tensor_product R E R →ₗ[R] A)

Equations

linear_map.tensor_product_rid_has_coe' = {coe := λ (f : E →ₗ[R] A), f.comp ↑(tensor_product.rid R E)}

theorem linear_map.lid_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} [add_comm_monoid A] [module R A] (f : E →ₗ[R] A) :

theorem linear_map.lid_symm_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} [add_comm_monoid A] [module R A] (f : tensor_product R R E →ₗ[R] A) :

theorem linear_map.rid_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} [add_comm_monoid A] [module R A] (f : E →ₗ[R] A) :

theorem linear_map.rid_symm_coe {R : Type u_1} {E : Type u_2} [comm_semiring R] [add_comm_group E] [module R E] {A : Type u_3} [add_comm_monoid A] [module R A] (f : tensor_product R E R →ₗ[R] A) :