OAI/Combinatorics/Sidorenko/TripleRanks.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SidorenkoCounterexample.orthogonal_map_isometry_between line 12

   Source documentation

   Orthogonal complements commute with isometries between different spaces.

   theorem orthogonal_map_isometry_between
       (ω : LinearMap.BilinForm K E) (η : LinearMap.BilinForm K F)
       (e : E ≃ₗ[K] F) (he : ∀ x y, η (e x) (e y) = ω x y)
       (U : Submodule K E) :
       η.orthogonal (U.map e.toLinearMap) = (ω.orthogonal U).map e.toLinearMap := by
   …

2. def OAI.SidorenkoCounterexample.horizontalSpace line 33
3. theorem OAI.SidorenkoCounterexample.mem_horizontalSpace line 36
4. theorem OAI.SidorenkoCounterexample.horizontalSpace_selforthogonal line 39
5. def OAI.SidorenkoCounterexample.verticalSpaceEquiv line 53
6. theorem OAI.SidorenkoCounterexample.triple_pair_block line 72
7. theorem OAI.SidorenkoCounterexample.exists_complement_reduction_equiv line 196

   Source documentation

   If an isotropic space is Lagrangian in a nondegenerate block, its symplectic quotient is the orthogonal complement of that block, with the literal quotient map as isometry.

   theorem exists_complement_reduction_equiv (ha : ω.IsAlt)
       (S B : Submodule K E) (hB : (ω.restrict B).Nondegenerate)
       (hSB : S ≤ B) (hBS : B ⊓ ω.orthogonal S = S) :
       ∃ e : ω.orthogonal B ≃ₗ[K] ReducedSpace ω S,
         (∀ x : ω.orthogonal B, e x = (reductionKernel ω S).mkQ
           ⟨x.val,by intro s hs; exact x.property s (hSB hs)⟩) ∧
         (∀ x y, symplecticReductionForm ω S ha (e x) (e y) = ω x.val y.val) ∧
         ∀ L : Submodule K E, L = (L ⊓ B) ⊔ (L ⊓ ω.orthogonal B) →
           (L.comap (ω.orthogonal B).subtype).map e.toLinearMap = reduceSubspace ω S L := by
   …

   Mentions: OAI.SidorenkoCounterexample.ReducedSpace, OAI.SidorenkoCounterexample.reductionKernel, OAI.SidorenkoCounterexample.symplecticReductionForm, OAI.SidorenkoCounterexample.reduceSubspace

8. theorem OAI.SidorenkoCounterexample.exists_reduction_in_stages line 273

   Source documentation

   Symplectic reduction in two nested isotropic spaces agrees with direct reduction. The equivalence also identifies the general (not merely containing) reduction of every subspace.

   theorem exists_reduction_in_stages (S T : Submodule K E)
       (hST : S ≤ T) (hT : T ≤ ω.orthogonal T) :
       ∃ e : ReducedSpace ω T ≃ₗ[K]
           ReducedSpace (symplecticReductionForm ω S ha) (reduceSubspace ω S T),
         (∀ x y, symplecticReductionForm (symplecticReductionForm ω S ha)
             (reduceSubspace ω S T) (symplecticReductionForm_alt ω S ha) (e x) (e y) =
           symplecticReductionForm ω T ha x y) ∧
         ∀ L : Submodule K E,
           (reduceSubspace ω T L).map e.toLinearMap =
             reduceSubspace (symplecticReductionForm ω S ha)
               (reduceSubspace ω S T) (reduceSubspace ω S L) := by
   …

   Mentions: OAI.SidorenkoCounterexample.ReducedSpace, OAI.SidorenkoCounterexample.symplecticReductionForm, OAI.SidorenkoCounterexample.reduceSubspace, OAI.SidorenkoCounterexample.symplecticReductionForm_alt

9. theorem OAI.SidorenkoCounterexample.exists_reduction_isometry_between line 376

   Source documentation

   Naturality of symplectic reduction under an isometry between arbitrary ambient spaces. Both forms and every reduced subspace are preserved.

   theorem exists_reduction_isometry_between
       (ω : LinearMap.BilinForm K E) (η : LinearMap.BilinForm K F)
       (ha : ω.IsAlt) (hb : η.IsAlt) (e : E ≃ₗ[K] F)
       (he : ∀ x y, η (e x) (e y) = ω x y)
       (S : Submodule K E) (T : Submodule K F) (hST : S.map e.toLinearMap = T) :
       ∃ f : ReducedSpace ω S ≃ₗ[K] ReducedSpace η T,
         (∀ x y, symplecticReductionForm η T hb (f x) (f y) =
           symplecticReductionForm ω S ha x y) ∧
         ∀ L : Submodule K E,
           (reduceSubspace ω S L).map f.toLinearMap = reduceSubspace η T (L.map e.toLinearMap) := by
   …

   Mentions: OAI.SidorenkoCounterexample.ReducedSpace, OAI.SidorenkoCounterexample.symplecticReductionForm, OAI.SidorenkoCounterexample.reduceSubspace

10. theorem OAI.SidorenkoCounterexample.exists_orthogonal_isometry_between line 448

    Source documentation

    Assemble isometries on a nondegenerate block and its orthogonal complement.

    theorem exists_orthogonal_isometry_between
        (ω : LinearMap.BilinForm K E) (η : LinearMap.BilinForm K F)
        (ha : ω.IsAlt) (hb : η.IsAlt)
        (B : Submodule K E) (C : Submodule K F)
        (hB : (ω.restrict B).Nondegenerate) (hC : (η.restrict C).Nondegenerate)
        (f : B ≃ₗ[K] C) (g : ω.orthogonal B ≃ₗ[K] η.orthogonal C)
        (hf : ∀ x y, η (f x).val (f y).val = ω x.val y.val)
        (hg : ∀ x y, η (g x).val (g y).val = ω x.val y.val) :
        ∃ e : E ≃ₗ[K] F, (∀ x y, η (e x) (e y) = ω x y) ∧
          (∀ x : B, e x.val = (f x).val) ∧
          (∀ x : ω.orthogonal B, e x.val = (g x).val) := by
    …

11. theorem OAI.SidorenkoCounterexample.map_orthogonal_split line 484

    Source documentation

    Mapping the two honest summands maps their sum, including repeated or zero summands. This is used only for actual orthogonal splittings of Lagrangians.

    theorem map_orthogonal_split (e : E ≃ₗ[K] F)
        (B : Submodule K E) (C : Submodule K F)
        (f : B ≃ₗ[K] C) (heB : ∀ x : B, e x.val = (f x).val)
        (U : Submodule K E) (W : Submodule K F)
        (g : U ≃ₗ[K] W) (heU : ∀ x : U, e x.val = (g x).val)
        (L : Submodule K E) (M : Submodule K F)
        (hL : L = (L ⊓ B) ⊔ (L ⊓ U)) (hM : M = (M ⊓ C) ⊔ (M ⊓ W))
        (hf : (L.comap B.subtype).map f.toLinearMap = M.comap C.subtype)
        (hg : (L.comap U.subtype).map g.toLinearMap = M.comap W.subtype) :
        L.map e.toLinearMap = M := by
    …

12. theorem OAI.SidorenkoCounterexample.split_inter_block line 533
13. theorem OAI.SidorenkoCounterexample.split_over_block line 549
14. theorem OAI.SidorenkoCounterexample.triple_block_reduction_data line 570

    Source documentation

    A common-zero triple has honest pair-block coordinates and the same residual triple as direct symplectic reduction by that pair intersection.

    theorem triple_block_reduction_data (ha : ω.IsAlt)
        (L M N : Submodule K E) (hL : ω.orthogonal L = L)
        (hM : ω.orthogonal M = M) (hN : ω.orthogonal N = N)
        (hzero : (L ⊓ M) ⊓ N = ⊥) :
        ∃ B : Submodule K E, (ω.restrict B).Nondegenerate ∧
          ∃ e : (↥(L ⊓ M) × Module.Dual K ↥(L ⊓ M)) ≃ₗ[K] B,
          ∃ f : ω.orthogonal B ≃ₗ[K] ReducedSpace ω (L ⊓ M),
            (∀ x y, ω (e x).val (e y).val = canonicalSymplectic x y) ∧
            (∀ x y, symplecticReductionForm ω (L ⊓ M) ha (f x) (f y) = ω x.val y.val) ∧
            L.comap B.subtype = horizontalSpace.map e.toLinearMap ∧
            M.comap B.subtype = horizontalSpace.map e.toLinearMap ∧
            N.comap B.subtype = verticalSpace.map e.toLinearMap ∧
    …

    Mentions: OAI.SidorenkoCounterexample.ReducedSpace, OAI.SidorenkoCounterexample.canonicalSymplectic, OAI.SidorenkoCounterexample.symplecticReductionForm

15. theorem OAI.SidorenkoCounterexample.map_transport_equiv line 649
16. theorem OAI.SidorenkoCounterexample.map_conjugate_equiv line 663
17. theorem OAI.SidorenkoCounterexample.triple_one_block_lift line 681

    Source documentation

    The extension across one pair block. No extension invariant remains: any isometry of the three reduced Lagrangians lifts to the triple.

    theorem triple_one_block_lift
        (ω : LinearMap.BilinForm K E) (η : LinearMap.BilinForm K F)
        (ha : ω.IsAlt) (hb : η.IsAlt)
        (L M N : Submodule K E) (L' M' N' : Submodule K F)
        (hL : ω.orthogonal L = L) (hM : ω.orthogonal M = M) (hN : ω.orthogonal N = N)
        (hL' : η.orthogonal L' = L') (hM' : η.orthogonal M' = M')
        (hN' : η.orthogonal N' = N')
        (hzero : (L ⊓ M) ⊓ N = ⊥) (hzero' : (L' ⊓ M') ⊓ N' = ⊥)
        (hdim : finrank K ↥(L ⊓ M) = finrank K ↥(L' ⊓ M'))
        (r : ReducedSpace ω (L ⊓ M) ≃ₗ[K] ReducedSpace η (L' ⊓ M'))
        (hr : ∀ x y, symplecticReductionForm η (L' ⊓ M') hb (r x) (r y) =
          symplecticReductionForm ω (L ⊓ M) ha x y)
    …

    Mentions: OAI.SidorenkoCounterexample.ReducedSpace, OAI.SidorenkoCounterexample.symplecticReductionForm

18. theorem OAI.SidorenkoCounterexample.reduceSubspace_self line 763
19. theorem OAI.SidorenkoCounterexample.reduceSubspace_inf line 770

    Source documentation

    Intersections commute with quotienting when the first subspace contains its kernel. This includes the two pair intersections which survive a split.

    theorem reduceSubspace_inf (L N : Submodule K E) (hSL : S ≤ L) :
        reduceSubspace ω S (L ⊓ N) =
          reduceSubspace ω S L ⊓ reduceSubspace ω S N := by
    …

    Mentions: OAI.SidorenkoCounterexample.reduceSubspace

20. theorem OAI.SidorenkoCounterexample.reduceSubspace_finrank_of_disjoint line 787

    Source documentation

    Reduction preserves a subspace disjoint from the quotient kernel.

    theorem reduceSubspace_finrank_of_disjoint [FiniteDimensional K E]
        (A : Submodule K E) (hAP : A ≤ ω.orthogonal S) (hAS : Disjoint A S) :
        finrank K (reduceSubspace ω S A) = finrank K A := by
    …

    Mentions: OAI.SidorenkoCounterexample.reduceSubspace

21. theorem OAI.SidorenkoCounterexample.reduceSubspace_sup line 810
22. def OAI.SidorenkoCounterexample.triplePairSum line 832
23. theorem OAI.SidorenkoCounterexample.triplePairSum_isotropic line 835
24. theorem OAI.SidorenkoCounterexample.triple_pair_reduction_intersections line 853
25. def OAI.SidorenkoCounterexample.TripleIsometry line 901
26. def OAI.SidorenkoCounterexample.TripleResidualIsometry line 906
27. theorem OAI.SidorenkoCounterexample.TripleResidualIsometry.swap_right line 918
28. theorem OAI.SidorenkoCounterexample.TripleResidualIsometry.rotate line 931
29. theorem OAI.SidorenkoCounterexample.triple_residual_isometry_reduce_pair line 950
30. theorem OAI.SidorenkoCounterexample.triple_isometry_of_zero_pairs line 989

    Source documentation

    When the pair intersections vanish, the final quotient already carries all of the ambient ordered triple.

    theorem triple_isometry_of_zero_pairs
        (ω : LinearMap.BilinForm K E) (η : LinearMap.BilinForm K F)
        (ha : ω.IsAlt) (hb : η.IsAlt)
        (L M N : Submodule K E) (L' M' N' : Submodule K F)
        (hL : ω.orthogonal L = L) (hM : ω.orthogonal M = M) (hN : ω.orthogonal N = N)
        (hL' : η.orthogonal L' = L') (hM' : η.orthogonal M' = M') (hN' : η.orthogonal N' = N')
        (hLM : L ⊓ M = ⊥) (hLN : L ⊓ N = ⊥) (hMN : M ⊓ N = ⊥)
        (hLM' : L' ⊓ M' = ⊥) (hLN' : L' ⊓ N' = ⊥) (hMN' : M' ⊓ N' = ⊥)
        (h : TripleResidualIsometry ω η ha hb L M N L' M' N') :
        TripleIsometry ω η L M N L' M' N' := by
    …

    Mentions: OAI.SidorenkoCounterexample.TripleResidualIsometry, OAI.SidorenkoCounterexample.TripleIsometry

31. theorem OAI.SidorenkoCounterexample.reduceSubspace_bot line 1018
32. theorem OAI.SidorenkoCounterexample.triple_isometry_of_two_zero_pairs line 1023
33. theorem OAI.SidorenkoCounterexample.triple_isometry_of_one_zero_pair line 1071
34. theorem OAI.SidorenkoCounterexample.triple_common_zero_classification line 1123