Finite-codimensional symplectic reduction

This file relates symplectic orthogonals to finite codimension, constructs the relevant quotient forms, and proves the finite-codimensional parity theorem.

theorem KaltonPeck.Support.FiniteCodim.strongOrthogonals {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (omega : StrongSymplecticForm X) (W : Submodule ℝ X) [IsClosed ↑W] [FiniteDimensional ℝ (X ⧸ W)] : FiniteDimensional ℝ ↥(omega.toContinuousAlternatingForm.orthogonal W) ∧ Module.finrank ℝ ↥(omega.toContinuousAlternatingForm.orthogonal W) = Module.finrank ℝ (X ⧸ W) ∧ omega.toContinuousAlternatingForm.orthogonal (omega.toContinuousAlternatingForm.orthogonal W) = W

Orthogonal dimensions and the double orthogonal in a strong symplectic Banach space.

Blueprint: lem:strong-orthogonals; audit: AUX-STRONG-ORTHOGONAL-DIMENSIONS.

theorem KaltonPeck.Support.FiniteCodim.strongCodimParity {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (omega : StrongSymplecticForm X) (W : Submodule ℝ X) [IsClosed ↑W] [FiniteDimensional ℝ (X ⧸ W)] : Module.finrank ℝ (X ⧸ W) ≡ Module.finrank ℝ ↥(omega.toContinuousAlternatingForm.restrictedRadical W) [MOD 2]

Parity of codimension and restricted radical in a strong symplectic Banach space.

Blueprint: lem:strong-codim-parity; audit: LEM-STRONG-SYMPLECTIC-CODIM-PARITY.

theorem KaltonPeck.Support.FiniteCodim.finiteCodimParity {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (eta : ContinuousAlternatingForm X) (hReflexive : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual ℝ X)) (hFredholm : IsFredholm eta.toDual) (E : Submodule ℝ X) [IsClosed ↑E] [FiniteDimensional ℝ (X ⧸ E)] : FiniteDimensional ℝ ↥(eta.restrictedRadical E) ∧ Module.finrank ℝ (X ⧸ E) ≡ Module.finrank ℝ ↥eta.radical + Module.finrank ℝ ↥(eta.restrictedRadical E) [MOD 2]

Finite-codimensional parity for a Fredholm alternating form.

Blueprint: thm:finite-codim-parity; audit: LEM-FINCODIM-PARITY and AUX-FINCODIM-PARITY-ARITHMETIC.