def
Garrett.IsFormedSpaceIso
{k : Type u_1}
[Field k]
{V₁ : Type u_2}
{V₂ : Type u_3}
[AddCommGroup V₁]
[Module k V₁]
[AddCommGroup V₂]
[Module k V₂]
(B₁ : LinearMap.BilinForm k V₁)
(B₂ : LinearMap.BilinForm k V₂)
(φ : V₁ ≃ₗ[k] V₂)
:
φ : V₁ ≃ₗ V₂ is an isometry of formed spaces with respect to B₁ and B₂
if it preserves the bilinear forms.
Instances For
def
Garrett.orthogonalSumForm
{k : Type u_1}
[Field k]
{U : Type u_2}
{W : Type u_3}
[AddCommGroup U]
[Module k U]
[AddCommGroup W]
[Module k W]
(B_U : LinearMap.BilinForm k U)
(B_W : LinearMap.BilinForm k W)
:
LinearMap.BilinForm k (U × W)
Orthogonal direct sum of two bilinear forms B_U on U and B_W on W.
Instances For
@[simp]
theorem
Garrett.orthogonalSumForm_apply
{k : Type u_1}
[Field k]
[NeZero 2]
{U : Type u_2}
{W : Type u_3}
[AddCommGroup U]
[Module k U]
[AddCommGroup W]
[Module k W]
(B_U : LinearMap.BilinForm k U)
(B_W : LinearMap.BilinForm k W)
(x y : U × W)
:
Evaluation formula for the orthogonal direct sum bilinear form.
def
Garrett.IsNondegenerate'
{k : Type u_1}
[Field k]
{V : Type u_2}
[AddCommGroup V]
[Module k V]
(B : LinearMap.BilinForm k V)
:
A bilinear form is nondegenerate (in the orthogonal-complement sense) if the orthogonal complement of the whole space is trivial.
Instances For
def
Garrett.IsSymmetric'
{k : Type u_1}
[Field k]
{V : Type u_2}
[AddCommGroup V]
[Module k V]
(B : LinearMap.BilinForm k V)
:
A bilinear form is symmetric: B x y = B y x for all x, y.
Instances For
theorem
Garrett.witt_extension_identity_on_U
{k : Type u_1}
[Field k]
[NeZero 2]
{U : Type u_2}
[AddCommGroup U]
[Module k U]
[FiniteDimensional k U]
{V : Type u_3}
[AddCommGroup V]
[Module k V]
[FiniteDimensional k V]
{W : Type u_4}
[AddCommGroup W]
[Module k W]
[FiniteDimensional k W]
(B_U : LinearMap.BilinForm k U)
(B_V : LinearMap.BilinForm k V)
(B_W : LinearMap.BilinForm k W)
(hU_symm : IsSymmetric' B_U)
(hV_symm : IsSymmetric' B_V)
(hW_symm : IsSymmetric' B_W)
(hU_nd : IsNondegenerate' B_U)
(hV_nd : IsNondegenerate' B_V)
(hW_nd : IsNondegenerate' B_W)
(φ : (U × V) ≃ₗ[k] U × W)
(hφ : IsFormedSpaceIso (orthogonalSumForm B_U B_V) (orthogonalSumForm B_U B_W) φ)
:
∃ (Ψ : (U × V) ≃ₗ[k] U × W),
IsFormedSpaceIso (orthogonalSumForm B_U B_V) (orthogonalSumForm B_U B_W) Ψ ∧ ∀ (u : U), Ψ (u, 0) = (u, 0)
Witt extension lemma: any isometry φ : U ⊕ V ≃ U ⊕ W can be modified to
an isometry Ψ of the same formed spaces that fixes the U-summand pointwise.
theorem
Garrett.first_component_zero
{k : Type u_1}
[Field k]
[NeZero 2]
{U : Type u_2}
[AddCommGroup U]
[Module k U]
[FiniteDimensional k U]
{V : Type u_3}
[AddCommGroup V]
[Module k V]
[FiniteDimensional k V]
{W : Type u_4}
[AddCommGroup W]
[Module k W]
[FiniteDimensional k W]
(B_U : LinearMap.BilinForm k U)
(B_V : LinearMap.BilinForm k V)
(B_W : LinearMap.BilinForm k W)
(hU_nd : IsNondegenerate' B_U)
(Ψ : (U × V) ≃ₗ[k] U × W)
(hΨ : IsFormedSpaceIso (orthogonalSumForm B_U B_V) (orthogonalSumForm B_U B_W) Ψ)
(hΨ_U : ∀ (u : U), Ψ (u, 0) = (u, 0))
(v : V)
:
If Ψ is an isometry of U ⊕ V and U ⊕ W fixing the U-summand, then the
first component of Ψ (0, v) vanishes for every v ∈ V.
noncomputable def
Garrett.extractEquiv
{k : Type u_1}
[Field k]
[NeZero 2]
{U : Type u_2}
[AddCommGroup U]
[Module k U]
[FiniteDimensional k U]
{V : Type u_3}
[AddCommGroup V]
[Module k V]
[FiniteDimensional k V]
{W : Type u_4}
[AddCommGroup W]
[Module k W]
[FiniteDimensional k W]
(B_U : LinearMap.BilinForm k U)
(B_V : LinearMap.BilinForm k V)
(B_W : LinearMap.BilinForm k W)
(hU_nd : IsNondegenerate' B_U)
(Ψ : (U × V) ≃ₗ[k] U × W)
(hΨ : IsFormedSpaceIso (orthogonalSumForm B_U B_V) (orthogonalSumForm B_U B_W) Ψ)
(hΨ_U : ∀ (u : U), Ψ (u, 0) = (u, 0))
:
Extract a linear equivalence V ≃ₗ W from a U-fixing isometry Ψ of
U ⊕ V and U ⊕ W, by sending v to the second component of Ψ (0, v).
Instances For
theorem
Garrett.extractEquiv_isometry
{k : Type u_1}
[Field k]
[NeZero 2]
{U : Type u_2}
[AddCommGroup U]
[Module k U]
[FiniteDimensional k U]
{V : Type u_3}
[AddCommGroup V]
[Module k V]
[FiniteDimensional k V]
{W : Type u_4}
[AddCommGroup W]
[Module k W]
[FiniteDimensional k W]
(B_U : LinearMap.BilinForm k U)
(B_V : LinearMap.BilinForm k V)
(B_W : LinearMap.BilinForm k W)
(hU_nd : IsNondegenerate' B_U)
(Ψ : (U × V) ≃ₗ[k] U × W)
(hΨ : IsFormedSpaceIso (orthogonalSumForm B_U B_V) (orthogonalSumForm B_U B_W) Ψ)
(hΨ_U : ∀ (u : U), Ψ (u, 0) = (u, 0))
:
IsFormedSpaceIso B_V B_W (extractEquiv B_U B_V B_W hU_nd Ψ hΨ hΨ_U)
The extracted linear equivalence V ≃ₗ W is an isometry of the formed
spaces (V, B_V) and (W, B_W).
theorem
Garrett.witt_cancellation_direct_sum
{k : Type u_1}
[Field k]
[NeZero 2]
{U : Type u_2}
[AddCommGroup U]
[Module k U]
[FiniteDimensional k U]
{V : Type u_3}
[AddCommGroup V]
[Module k V]
[FiniteDimensional k V]
{W : Type u_4}
[AddCommGroup W]
[Module k W]
[FiniteDimensional k W]
(B_U : LinearMap.BilinForm k U)
(B_V : LinearMap.BilinForm k V)
(B_W : LinearMap.BilinForm k W)
(hU_symm : IsSymmetric' B_U)
(hV_symm : IsSymmetric' B_V)
(hW_symm : IsSymmetric' B_W)
(hU_nd : IsNondegenerate' B_U)
(hV_nd : IsNondegenerate' B_V)
(hW_nd : IsNondegenerate' B_W)
(φ : (U × V) ≃ₗ[k] U × W)
(hφ : IsFormedSpaceIso (orthogonalSumForm B_U B_V) (orthogonalSumForm B_U B_W) φ)
:
∃ (ψ : V ≃ₗ[k] W), IsFormedSpaceIso B_V B_W ψ
Witt cancellation for orthogonal direct sums: if U ⊕ V is isometric to
U ⊕ W (with the same nondegenerate U-summand), then V is isometric to W.