Documentation

TauCeti.LinearAlgebra.QuadraticForm.TotallyIsotropic

Totally isotropic submodules #

A submodule W of M is totally isotropic for a quadratic map Q when Q vanishes on every vector of W, that is, when the restriction of Q to W is zero.

Main definitions #

Main results #

The Witt-index comparison for maximal totally isotropic subspaces (Lam I.4.4) is in TauCeti.LinearAlgebra.QuadraticForm.Witt.TotallyIsotropic.

source
def QuadraticMap.IsTotallyIsotropic {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (W : Submodule R M) :
Prop

A submodule W is totally isotropic for a quadratic map Q when Q vanishes on every vector of W.

Instances For
    source
    theorem QuadraticMap.isTotallyIsotropic_iff {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {W : Submodule R M} :
    Q.IsTotallyIsotropic W ↔ ∀ v ∈ W, Q v = 0

    Unfolds QuadraticMap.IsTotallyIsotropic.

    source
    theorem QuadraticMap.IsTotallyIsotropic.apply_eq_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {W : Submodule R M} (hW : Q.IsTotallyIsotropic W) {v : M} (hv : v ∈ W) :
    Q v = 0

    A quadratic map vanishes on each vector of a totally isotropic submodule.

    source
    theorem QuadraticMap.isTotallyIsotropic_iff_restrict_eq_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {W : Submodule R M} :
    Q.IsTotallyIsotropic W ↔ Q.restrict W = 0

    A submodule is totally isotropic exactly when the restriction of the form to it is zero.

    source
    theorem QuadraticMap.isTotallyIsotropic_comp_iff {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {f : M' →ₗ[R] M} {T : Submodule R M'} :
    (Q.comp f).IsTotallyIsotropic T ↔ Q.IsTotallyIsotropic (Submodule.map f T)

    A submodule is totally isotropic for Q.comp f exactly when its image under f is totally isotropic for Q.

    source
    theorem QuadraticMap.IsTotallyIsotropic.comap {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {W : Submodule R M} (hW : Q.IsTotallyIsotropic W) (f : M' →ₗ[R] M) :
    (Q.comp f).IsTotallyIsotropic (Submodule.comap f W)

    The preimage of a totally isotropic submodule under a linear map f is totally isotropic for Q.comp f.

    source
    theorem QuadraticMap.isTotallyIsotropic_restrict_iff {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {U : Submodule R M} {T : Submodule R ↥U} :
    (Q.restrict U).IsTotallyIsotropic T ↔ Q.IsTotallyIsotropic (Submodule.map U.subtype T)

    A submodule of U is totally isotropic for the restriction of Q to U exactly when it is totally isotropic for Q as a submodule of M.

    source
    theorem QuadraticMap.IsTotallyIsotropic.restrict {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {W : Submodule R M} (hW : Q.IsTotallyIsotropic W) (U : Submodule R M) :
    (Q.restrict U).IsTotallyIsotropic (Submodule.comap U.subtype W)

    The vectors of U lying in a totally isotropic submodule W form a totally isotropic submodule for the restriction of Q to U.

    source
    @[simp]
    theorem QuadraticMap.isTotallyIsotropic_bot {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} :
    Q.IsTotallyIsotropic ⊥

    The zero submodule is totally isotropic.

    source
    theorem QuadraticMap.IsTotallyIsotropic.mono {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {W W' : Submodule R M} (hW : Q.IsTotallyIsotropic W) (h : W' ≤ W) :
    Q.IsTotallyIsotropic W'

    A submodule of a totally isotropic submodule is totally isotropic.

    source
    @[simp]
    theorem QuadraticMap.isTotallyIsotropic_span_singleton_iff {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {v : M} :
    Q.IsTotallyIsotropic (R ∙ v) ↔ Q v = 0

    A line is totally isotropic exactly when its spanning vector is isotropic.

    source
    theorem QuadraticMap.maximal_isTotallyIsotropic_bot_iff {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} :
    Maximal Q.IsTotallyIsotropic ⊥ ↔ Q.Anisotropic

    The zero subspace is a maximal totally isotropic subspace exactly when the form is anisotropic.

    source
    theorem QuadraticMap.IsTotallyIsotropic.polar_eq_zero {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {Q : QuadraticMap R M N} {W : Submodule R M} (hW : Q.IsTotallyIsotropic W) {v w : M} (hv : v ∈ W) (hw : w ∈ W) :
    polar (⇑Q) v w = 0

    The polar form vanishes on pairs of vectors of a totally isotropic submodule.

    source
    theorem QuadraticMap.IsTotallyIsotropic.eq_zero_of_polar_eq_zero {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {Q : QuadraticMap R M N} {W W' : Submodule R M} (hW' : Q.IsTotallyIsotropic W') (hQ : Nondegenerate) (hWW' : Codisjoint W W') {y : M} (hy : y ∈ W') (hyW : ∀ x ∈ W, polar (⇑Q) x y = 0) :
    y = 0

    For a nondegenerate Q, if W ⊔ W' = ⊤ with W' totally isotropic, a vector of W' which is polar-orthogonal to W vanishes: it is then polar-orthogonal to all of M = W + W', hence lies in the radical.

    source
    theorem QuadraticMap.IsTotallyIsotropic.polarBilin_compl₁₂_flip_injective {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {Q : QuadraticMap R M N} {W W' : Submodule R M} (hW' : Q.IsTotallyIsotropic W') (hQ : Nondegenerate) (hWW' : Codisjoint W W') :
    Function.Injective ⇑(LinearMap.compl₁₂ Q.polarBilin W.subtype W'.subtype).flip

    For a nondegenerate Q and W ⊔ W' = ⊤ with W' totally isotropic, the polar pairing of W' with W is injective in the W' variable.

    source
    theorem QuadraticMap.IsTotallyIsotropic.finiteDimensional_of_codisjoint {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} (hW' : IsTotallyIsotropic Q W') (hQ : Nondegenerate) (hWW' : Codisjoint W W') [FiniteDimensional K ↥W] :
    FiniteDimensional K ↥W'

    If W is finite-dimensional and W ⊔ W' = ⊤ with W' totally isotropic in a nondegenerate space, then W' is finite-dimensional: the polar pairing embeds W' into the dual of W.

    source
    theorem QuadraticMap.IsTotallyIsotropic.finrank_le_of_codisjoint {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} (hW' : IsTotallyIsotropic Q W') (hQ : Nondegenerate) (hWW' : Codisjoint W W') [FiniteDimensional K ↥W] :
    Module.finrank K ↥W' ≤ Module.finrank K ↥W

    If W is finite-dimensional and W ⊔ W' = ⊤ with W' totally isotropic in a nondegenerate space, then W' has dimension at most that of W: the polar pairing embeds W' into the dual of W.

    source
    theorem QuadraticMap.IsTotallyIsotropic.finrank_eq_of_codisjoint {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} (hW : IsTotallyIsotropic Q W) (hW' : IsTotallyIsotropic Q W') (hQ : Nondegenerate) (hWW' : Codisjoint W W') :
    Module.finrank K ↥W' = Module.finrank K ↥W

    Two totally isotropic subspaces spanning a nondegenerate quadratic space have the same Module.finrank: the polar pairing embeds each into the dual of the other. This is the equality of their dimensions when they are finite-dimensional, and otherwise both finranks are 0.