Isometric linear maps #
Note that quadratic_form.isometry is already taken for isometric equivalences.
def
quadratic_form.isometric_map.to_linear_map
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(self : Q₁.isometric_map Q₂) :
@[nolint]
structure
quadratic_form.isometric_map
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(Q₁ : quadratic_form R M₁)
(Q₂ : quadratic_form R M₂) :
Type (max u_4 u_5)
- to_fun : M₁ → M₂
- map_add' : ∀ (x y : M₁), self.to_fun (x + y) = self.to_fun x + self.to_fun y
- map_smul' : ∀ (r : R) (x : M₁), self.to_fun (r • x) = ⇑(ring_hom.id R) r • self.to_fun x
- map_app' : ∀ (m : M₁), ⇑Q₂ (self.to_fun m) = ⇑Q₁ m
An isometry between two quadratic spaces M₁, Q₁ and M₂, Q₂ over a ring R,
is a linear equivalence between M₁ and M₂ that commutes with the quadratic forms.
Instances for quadratic_form.isometric_map
- quadratic_form.isometric_map.has_sizeof_inst
- quadratic_form.isometric_map.semilinear_map_class
- quadratic_form.isometric_map.isometric_map.has_zero
- quadratic_form.isometric_map.has_zero
- quadratic_form.isometric_map.subsingleton
@[protected, instance]
def
quadratic_form.isometric_map.semilinear_map_class
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂} :
semilinear_map_class (Q₁.isometric_map Q₂) (ring_hom.id R) M₁ M₂
Equations
- quadratic_form.isometric_map.semilinear_map_class = {coe := λ (f : Q₁.isometric_map Q₂), ⇑(f.to_linear_map), coe_injective' := _, map_add := _, map_smulₛₗ := _}
theorem
quadratic_form.isometric_map.to_linear_map_injective
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂} :
@[ext]
theorem
quadratic_form.isometric_map.ext
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
⦃f g : Q₁.isometric_map Q₂⦄
(h : ∀ (x : M₁), ⇑f x = ⇑g x) :
f = g
@[protected]
def
quadratic_form.isometric_map.simps.apply
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(f : Q₁.isometric_map Q₂) :
M₁ → M₂
See Note [custom simps projection].
Equations
@[simp]
theorem
quadratic_form.isometric_map.map_app
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(f : Q₁.isometric_map Q₂)
(m : M₁) :
@[simp]
theorem
quadratic_form.isometric_map.coe_to_linear_map
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(f : Q₁.isometric_map Q₂) :
⇑(f.to_linear_map) = ⇑f
@[simp]
theorem
quadratic_form.isometric_map.id_apply
{R : Type u_2}
{M : Type u_3}
[semiring R]
[add_comm_monoid M]
[module R M]
(Q : quadratic_form R M)
(ᾰ : M) :
def
quadratic_form.isometric_map.id
{R : Type u_2}
{M : Type u_3}
[semiring R]
[add_comm_monoid M]
[module R M]
(Q : quadratic_form R M) :
Q.isometric_map Q
The identity isometry from a quadratic form to itself.
Equations
- quadratic_form.isometric_map.id Q = {to_fun := linear_map.id.to_fun, map_add' := _, map_smul' := _, map_app' := _}
def
quadratic_form.isometric_map.comp
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
{M₃ : Type u_6}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₁]
[module R M₂]
[module R M₃]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
{Q₃ : quadratic_form R M₃}
(g : Q₂.isometric_map Q₃)
(f : Q₁.isometric_map Q₂) :
Q₁.isometric_map Q₃
The composition of two isometries between quadratic forms.
@[simp]
theorem
quadratic_form.isometric_map.comp_apply
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
{M₃ : Type u_6}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₁]
[module R M₂]
[module R M₃]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
{Q₃ : quadratic_form R M₃}
(g : Q₂.isometric_map Q₃)
(f : Q₁.isometric_map Q₂)
(x : M₁) :
@[simp]
theorem
quadratic_form.isometric_map.to_linear_map_comp
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
{M₃ : Type u_6}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₁]
[module R M₂]
[module R M₃]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
{Q₃ : quadratic_form R M₃}
(g : Q₂.isometric_map Q₃)
(f : Q₁.isometric_map Q₂) :
(g.comp f).to_linear_map = g.to_linear_map.comp f.to_linear_map
@[simp]
theorem
quadratic_form.isometric_map.id_comp
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(f : Q₁.isometric_map Q₂) :
(quadratic_form.isometric_map.id Q₂).comp f = f
@[simp]
theorem
quadratic_form.isometric_map.comp_id
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(f : Q₁.isometric_map Q₂) :
f.comp (quadratic_form.isometric_map.id Q₁) = f
theorem
quadratic_form.isometric_map.comp_assoc
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
{M₃ : Type u_6}
{M₄ : Type u_7}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[add_comm_monoid M₄]
[module R M₁]
[module R M₂]
[module R M₃]
[module R M₄]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
{Q₃ : quadratic_form R M₃}
{Q₄ : quadratic_form R M₄}
(h : Q₃.isometric_map Q₄)
(g : Q₂.isometric_map Q₃)
(f : Q₁.isometric_map Q₂) :
def
quadratic_form.isometry.to_isometric_map
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(g : Q₁.isometry Q₂) :
Q₁.isometric_map Q₂
Isometries are isometric maps
Equations
- g.to_isometric_map = {to_fun := g.to_linear_equiv.to_fun, map_add' := _, map_smul' := _, map_app' := _}
@[simp]
theorem
quadratic_form.isometry.to_isometric_map_apply
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(g : Q₁.isometry Q₂)
(ᾰ : M₁) :
⇑(g.to_isometric_map) ᾰ = g.to_linear_equiv.to_fun ᾰ
@[protected, instance]
def
quadratic_form.isometric_map.isometric_map.has_zero
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₂ : quadratic_form R M₂} :
has_zero (0.isometric_map Q₂)
There is a zero map from any module with the zero form.
@[protected, instance]
def
quadratic_form.isometric_map.has_zero
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
[subsingleton M₁] :
has_zero (Q₁.isometric_map Q₂)
There is a zero map from the trivial module.
@[protected, instance]
def
quadratic_form.isometric_map.subsingleton
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
[subsingleton M₂] :
subsingleton (Q₁.isometric_map Q₂)
Maps into the zero module are trivial