mathlib3 documentation

lean-ga / for_mathlib.linear_algebra.quadratic_form.prod

Extra results using `isometric_map` about `quadratic_form`s on product types #

def quadratic_form.isometric_map.inl {ι : Type u_1} {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module R M₂] [fintype ι] (QM₁ : quadratic_form R M₁) (QM₂ : quadratic_form R M₂) [decidable_eq ι] (i : ι) :

QM₁.isometric_map (QM₁.prod QM₂)

linear_map.inl as an isometric_map.

Equations

quadratic_form.isometric_map.inl QM₁ QM₂ i = {to_fun := (linear_map.inl R M₁ M₂).to_fun, map_add' := _, map_smul' := _, map_app' := _}

@[simp]

theorem quadratic_form.isometric_map.inl_apply {ι : Type u_1} {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module R M₂] [fintype ι] (QM₁ : quadratic_form R M₁) (QM₂ : quadratic_form R M₂) [decidable_eq ι] (i : ι) (ᾰ : M₁) :

⇑(quadratic_form.isometric_map.inl QM₁ QM₂ i) ᾰ = (linear_map.inl R M₁ M₂).to_fun ᾰ

def quadratic_form.isometric_map.inr {ι : Type u_1} {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module R M₂] [fintype ι] (QM₁ : quadratic_form R M₁) (QM₂ : quadratic_form R M₂) [decidable_eq ι] (i : ι) :

QM₂.isometric_map (QM₁.prod QM₂)

linear_map.inl as an isometric_map.

Equations

quadratic_form.isometric_map.inr QM₁ QM₂ i = {to_fun := (linear_map.inr R M₁ M₂).to_fun, map_add' := _, map_smul' := _, map_app' := _}

@[simp]

theorem quadratic_form.isometric_map.inr_apply {ι : Type u_1} {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module R M₂] [fintype ι] (QM₁ : quadratic_form R M₁) (QM₂ : quadratic_form R M₂) [decidable_eq ι] (i : ι) (ᾰ : M₂) :

⇑(quadratic_form.isometric_map.inr QM₁ QM₂ i) ᾰ = (linear_map.inr R M₁ M₂).to_fun ᾰ

@[simp]

theorem quadratic_form.isometric_map.prod_apply {R : Type u_2} {M₁ : Type u_3} {N₁ : Type u_5} {N₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid N₁] [add_comm_monoid N₂] [module R M₁] [module R N₁] [module R N₂] {QN₁ : quadratic_form R N₁} {QN₂ : quadratic_form R N₂} {fQM₁ gQM₁ : quadratic_form R M₁} (f : fQM₁.isometric_map QN₁) (g : gQM₁.isometric_map QN₂) (i : M₁) :

⇑(f.prod g) i = pi.prod ⇑f ⇑g i

def quadratic_form.isometric_map.prod {R : Type u_2} {M₁ : Type u_3} {N₁ : Type u_5} {N₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid N₁] [add_comm_monoid N₂] [module R M₁] [module R N₁] [module R N₂] {QN₁ : quadratic_form R N₁} {QN₂ : quadratic_form R N₂} {fQM₁ gQM₁ : quadratic_form R M₁} (f : fQM₁.isometric_map QN₁) (g : gQM₁.isometric_map QN₂) :

(fQM₁ + gQM₁).isometric_map (QN₁.prod QN₂)

pi.prod of two isometric maps.

Equations

f.prod g = {to_fun := pi.prod ⇑f ⇑g, map_add' := _, map_smul' := _, map_app' := _}

def quadratic_form.isometric_map.prod_map {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid N₁] [add_comm_monoid N₂] [module R M₁] [module R M₂] [module R N₁] [module R N₂] {QM₁ : quadratic_form R M₁} {QM₂ : quadratic_form R M₂} {QN₁ : quadratic_form R N₁} {QN₂ : quadratic_form R N₂} (f : QM₁.isometric_map QN₁) (g : QM₂.isometric_map QN₂) :

(QM₁.prod QM₂).isometric_map (QN₁.prod QN₂)

prod.map of two isometric maps.

Equations

f.prod_map g = {to_fun := (f.to_linear_map.prod_map g.to_linear_map).to_fun, map_add' := _, map_smul' := _, map_app' := _}

@[simp]

theorem quadratic_form.isometric_map.prod_map_apply {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid N₁] [add_comm_monoid N₂] [module R M₁] [module R M₂] [module R N₁] [module R N₂] {QM₁ : quadratic_form R M₁} {QM₂ : quadratic_form R M₂} {QN₁ : quadratic_form R N₁} {QN₂ : quadratic_form R N₂} (f : QM₁.isometric_map QN₁) (g : QM₂.isometric_map QN₂) (ᾰ : M₁ × M₂) :

⇑(f.prod_map g) ᾰ = (f.to_linear_map.prod_map g.to_linear_map).to_fun ᾰ

def quadratic_form.isometric_map.single {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [semiring R] [Π (i : ι), add_comm_monoid (Mᵢ i)] [Π (i : ι), module R (Mᵢ i)] [fintype ι] (QMᵢ : Π (i : ι), quadratic_form R (Mᵢ i)) [decidable_eq ι] (i : ι) :

(QMᵢ i).isometric_map (quadratic_form.pi QMᵢ)

linear_map.single as an isometric_map.

Equations

quadratic_form.isometric_map.single QMᵢ i = {to_fun := pi.single i, map_add' := _, map_smul' := _, map_app' := _}

@[simp]

theorem quadratic_form.isometric_map.single_apply {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_7} [semiring R] [Π (i : ι), add_comm_monoid (Mᵢ i)] [Π (i : ι), module R (Mᵢ i)] [fintype ι] (QMᵢ : Π (i : ι), quadratic_form R (Mᵢ i)) [decidable_eq ι] (i : ι) (x : Mᵢ i) (i_1 : ι) :

⇑(quadratic_form.isometric_map.single QMᵢ i) x i_1 = pi.single i x i_1

def quadratic_form.isometric_map.pi {ι : Type u_1} {R : Type u_2} {M₁ : Type u_3} {Mᵢ : ι → Type u_7} [semiring R] [add_comm_monoid M₁] [module R M₁] [Π (i : ι), add_comm_monoid (Mᵢ i)] [Π (i : ι), module R (Mᵢ i)] [fintype ι] (QM₁ : ι → quadratic_form R M₁) (QMᵢ : Π (i : ι), quadratic_form R (Mᵢ i)) (f : Π (i : ι), (QM₁ i).isometric_map (QMᵢ i)) :

(finset.univ.sum (λ (i : ι), QM₁ i)).isometric_map (quadratic_form.pi QMᵢ)

linear_map.pi for isometric_map.

Equations

quadratic_form.isometric_map.pi QM₁ QMᵢ f = {to_fun := λ (c : M₁) (i : ι), ⇑(f i) c, map_add' := _, map_smul' := _, map_app' := _}