OAI/Combinatorics/Sidorenko/Reduction.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SidorenkoCounterexample.reductionKernel line 12

   Source documentation

   The copy of an isotropic space inside its orthogonal complement.

   def reductionKernel : Submodule K (ω.orthogonal S) := S.comap (ω.orthogonal S).subtype

2. abbrev OAI.SidorenkoCounterexample.ReducedSpace line 13
3. theorem OAI.SidorenkoCounterexample.restricted_alt line 15
4. theorem OAI.SidorenkoCounterexample.reductionKernel_le_ker line 20
5. def OAI.SidorenkoCounterexample.symplecticReductionForm line 29
6. theorem OAI.SidorenkoCounterexample.reductionForm_mk line 34
7. theorem OAI.SidorenkoCounterexample.symplecticReductionForm_alt line 38
8. theorem OAI.SidorenkoCounterexample.symplecticReductionForm_nondegenerate line 44
9. theorem OAI.SidorenkoCounterexample.reducedSpace_finrank line 62
10. def OAI.SidorenkoCounterexample.liftReduction line 76
11. theorem OAI.SidorenkoCounterexample.mem_liftReduction line 79
12. theorem OAI.SidorenkoCounterexample.le_liftReduction line 89
13. theorem OAI.SidorenkoCounterexample.liftReduction_le line 99
14. theorem OAI.SidorenkoCounterexample.orthogonal_liftReduction line 105

    Source documentation

    Orthogonality commutes exactly with lifting from an isotropic quotient.

    theorem orthogonal_liftReduction (ha : ω.IsAlt) (hS : S ≤ ω.orthogonal S)
        (T : Submodule K (ReducedSpace ω S)) :
        ω.orthogonal (liftReduction ω S T) =
          liftReduction ω S ((symplecticReductionForm ω S ha).orthogonal T) := by
    …

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

15. theorem OAI.SidorenkoCounterexample.liftReduction_lagrangian line 128

    Source documentation

    Thus every quotient Lagrangian lifts to a Lagrangian containing S.

    theorem liftReduction_lagrangian (ha : ω.IsAlt) (hS : S ≤ ω.orthogonal S)
        (T : Submodule K (ReducedSpace ω S))
        (hT : (symplecticReductionForm ω S ha).orthogonal T = T) :
        ω.orthogonal (liftReduction ω S T) = liftReduction ω S T := by
    …

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

16. def OAI.SidorenkoCounterexample.reduceSubspace line 135

    Source documentation

    The image of a subspace intersected with Sᗮ in the quotient.

    def reduceSubspace (L : Submodule K E) : Submodule K (ReducedSpace ω S) :=
    …

    Mentions: OAI.SidorenkoCounterexample.ReducedSpace

17. theorem OAI.SidorenkoCounterexample.reduce_lift line 138
18. theorem OAI.SidorenkoCounterexample.liftReduction_injective line 152
19. theorem OAI.SidorenkoCounterexample.lift_reduce line 157
20. theorem OAI.SidorenkoCounterexample.lagrangian_le_orthogonal line 172
21. theorem OAI.SidorenkoCounterexample.reduce_lagrangian line 178
22. def OAI.SidorenkoCounterexample.containingLagrangianEquiv line 188
23. theorem OAI.SidorenkoCounterexample.orthogonal_sup_eq line 198
24. theorem OAI.SidorenkoCounterexample.orthogonal_inf_eq line 208
25. theorem OAI.SidorenkoCounterexample.general_lagrangian_reduction line 221

    Source documentation

    Every Lagrangian has a Lagrangian reduction, even when it does not contain or avoid the isotropic space S.

    theorem general_lagrangian_reduction [FiniteDimensional K E]
        (ha : ω.IsAlt) (hω : ω.Nondegenerate) (hS : S ≤ ω.orthogonal S)
        (L : Submodule K E) (hL : ω.orthogonal L = L) :
        (symplecticReductionForm ω S ha).orthogonal (reduceSubspace ω S L) =
          reduceSubspace ω S L := by
    …

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

26. theorem OAI.SidorenkoCounterexample.isotropic_sup_line line 264
27. theorem OAI.SidorenkoCounterexample.exists_containing_lagrangian line 278

    Source documentation

    Finite-dimensional finite-field spaces admit Lagrangian extensions of all isotropic spaces; no completion or existence axiom is used.

    theorem exists_containing_lagrangian (ha : ω.IsAlt) (S : Submodule K E)
        (hS : S ≤ ω.orthogonal S) :
        ∃ L : Submodule K E, S ≤ L ∧ ω.orthogonal L = L := by
    …

28. theorem OAI.SidorenkoCounterexample.form_orthogonal_sum line 302

    Source documentation

    The form splits as an orthogonal direct sum along a nondegenerate subspace.

    theorem form_orthogonal_sum (ha : ω.IsAlt) (U : Submodule K E)
        (x y : U × ω.orthogonal U) :
        ω (x.1.val + x.2.val) (y.1.val + y.2.val) =
          ω x.1.val y.1.val + ω x.2.val y.2.val := by
    …

29. theorem OAI.SidorenkoCounterexample.exists_orthogonal_extension line 313

    Source documentation

    An isometry of a nondegenerate subspace extends by identity on its orthogonal complement. This avoids any symplectic-basis assumptions.

    theorem exists_orthogonal_extension (ha : ω.IsAlt) (U : Submodule K E)
        (hU : (ω.restrict U).Nondegenerate) (f : U ≃ₗ[K] U)
        (hf : ∀ x y : U, ω (f x).val (f y).val = ω x.val y.val) :
        ∃ e : E ≃ₗ[K] E,
          (∀ x y, ω (e x) (e y) = ω x y) ∧
          (∀ x : U, e x.val = (f x).val) ∧
          (∀ x : ω.orthogonal U, e x.val = x.val) := by
    …

30. theorem OAI.SidorenkoCounterexample.reduction_section_isometry line 344

    Source documentation

    A linear section of the symplectic quotient automatically preserves the form, because that form was defined on representatives.

    theorem reduction_section_isometry (ha : ω.IsAlt)
        (s : ReducedSpace ω S →ₗ[K] ω.orthogonal S)
        (hs : (reductionKernel ω S).mkQ.comp s = LinearMap.id)
        (x y : ReducedSpace ω S) :
        ω (s x).val (s y).val = symplecticReductionForm ω S ha x y := by
    …

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

31. theorem OAI.SidorenkoCounterexample.exists_reduction_isometry_extension line 360
32. theorem OAI.SidorenkoCounterexample.equal_fiber_card_identity line 448

    Source documentation

    Equal fiber cardinalities imply an exactly uniform pushforward, without any measure-theoretic identification or conditional-independence assumption.

    theorem equal_fiber_card_identity {A B : Type*} [Finite A] [Finite B]
        (f : A → B) (b : B)
        (h : ∀ c : B, Nonempty ({a : A // f a = b} ≃ {a : A // f a = c})) :
        Nat.card {a : A // f a = b} * Nat.card B = Nat.card A := by
    …

33. theorem OAI.SidorenkoCounterexample.reduceSubspace_map line 470

    Source documentation

    Naturality of reduction for an actual extension of a quotient map.

    theorem reduceSubspace_map (e : E ≃ₗ[K] E)
        (f : ReducedSpace ω S ≃ₗ[K] ReducedSpace ω S)
        (hP : (ω.orthogonal S).map e.toLinearMap = ω.orthogonal S)
        (hQ : ∀ x y : ω.orthogonal S, e x.val = y.val →
          (reductionKernel ω S).mkQ y = f ((reductionKernel ω S).mkQ x))
        (L : Submodule K E) :
        reduceSubspace ω S (L.map e.toLinearMap) =
          (reduceSubspace ω S L).map f.toLinearMap := by
    …

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

34. theorem OAI.SidorenkoCounterexample.subspace_map_eq_of_fixed line 494

    Source documentation

    A pointwise-fixed subspace is fixed under the subspace action.

    theorem subspace_map_eq_of_fixed (e : E ≃ₗ[K] E) (U : Submodule K E)
        (h : ∀ x : U, e x.val = x.val) : U.map e.toLinearMap = U := by
    …

35. abbrev OAI.SidorenkoCounterexample.AvoidanceSpace line 505
36. def OAI.SidorenkoCounterexample.avoidanceIsometryEquiv line 510

    Source documentation

    An extension fixing S preserves separately each containment-and-avoidance condition A⊂L, L∩S=A used in the independent residual laws.

    noncomputable def avoidanceIsometryEquiv (A : Submodule K E) (hAS : A ≤ S)
        (e : E ≃ₗ[K] E) (he : ∀ x y, ω (e x) (e y) = ω x y)
        (hS : ∀ x : S, e x.val = x.val) :
        AvoidanceSpace ω S A ≃ AvoidanceSpace ω S A := by
    …

    Mentions: OAI.SidorenkoCounterexample.AvoidanceSpace

37. def OAI.SidorenkoCounterexample.avoidanceReduction line 542
38. theorem OAI.SidorenkoCounterexample.avoidanceReduction_fiber_equiv line 552
39. theorem OAI.SidorenkoCounterexample.avoidanceReduction_uniform line 588

    Source documentation

    The conditional residual law is exactly uniform, in cardinal form. It remains valid when the conditioning event is empty, without division by 0.

    theorem avoidanceReduction_uniform (h2 : (2 : K) ≠ 0) (ha : ω.IsAlt)
        (hω : ω.Nondegenerate) (hS : S ≤ ω.orthogonal S)
        (A : Submodule K E) (hAS : A ≤ S)
        (T : {T : Submodule K (ReducedSpace ω S) //
          (symplecticReductionForm ω S ha).orthogonal T = T}) :
        Nat.card {L : AvoidanceSpace ω S A // avoidanceReduction ω S ha hω hS A L = T} *
          Nat.card {U : Submodule K (ReducedSpace ω S) //
            (symplecticReductionForm ω S ha).orthogonal U = U} =
            Nat.card (AvoidanceSpace ω S A) := by
    …

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

40. theorem OAI.SidorenkoCounterexample.exists_linearEquiv_extension line 611

    Source documentation

    A prescribed equivalence of subspaces extends to the ambient spaces when both ambient dimensions and the complementary dimensions agree.

    theorem exists_linearEquiv_extension
        {K E F : Type*} [Field K] [AddCommGroup E] [Module K E]
        [AddCommGroup F] [Module K F] [FiniteDimensional K E] [FiniteDimensional K F]
        (U : Submodule K E) (W : Submodule K F)
        (hEF : finrank K E = finrank K F) (f : U ≃ₗ[K] W) :
        ∃ e : E ≃ₗ[K] F, ∀ u : U, e u.val = (f u).val := by
    …

41. theorem OAI.SidorenkoCounterexample.subspace_transitivity line 636

    Source documentation

    Full linear groups are transitive on subspaces of each dimension.

    theorem subspace_transitivity
        {K E F : Type*} [Field K] [AddCommGroup E] [Module K E]
        [AddCommGroup F] [Module K F] [FiniteDimensional K E] [FiniteDimensional K F]
        (U : Submodule K E) (W : Submodule K F)
        (hEF : finrank K E = finrank K F) (hUW : finrank K U = finrank K W) :
        ∃ e : E ≃ₗ[K] F, U.map e.toLinearMap = W := by
    …

42. theorem OAI.SidorenkoCounterexample.isotropic_transitivity line 669
43. theorem OAI.SidorenkoCounterexample.transverse_isCompl line 727
44. theorem OAI.SidorenkoCounterexample.exists_transverse_pair_coordinates line 736

    Source documentation

    Darboux coordinates respecting a specified ordered transverse pair.

    theorem exists_transverse_pair_coordinates (ha : ω.IsAlt) (hω : ω.Nondegenerate)
        (L M : Submodule K E) (hL : ω.orthogonal L = L) (hM : ω.orthogonal M = M)
        (hLM : L ⊓ M = ⊥) :
        ∃ e : (L × Module.Dual K L) ≃ₗ[K] E,
          (∀ x, e x ∈ L ↔ x.2 = 0) ∧ (∀ x, e x ∈ M ↔ x.1 = 0) ∧
          ∀ x y, ω (e x) (e y) = canonicalSymplectic x y := by
    …

    Mentions: OAI.SidorenkoCounterexample.canonicalSymplectic

45. theorem OAI.SidorenkoCounterexample.subspace_map_eq_of_mem_iff line 809
46. theorem OAI.SidorenkoCounterexample.transverse_pair_transitivity line 827
47. theorem OAI.SidorenkoCounterexample.liftReduction_inf line 875
48. theorem OAI.SidorenkoCounterexample.liftReduction_bot line 881
49. theorem OAI.SidorenkoCounterexample.reduced_pair_transverse line 893
50. theorem OAI.SidorenkoCounterexample.pair_transitivity_fixed_intersection line 906
51. theorem OAI.SidorenkoCounterexample.ordered_pair_transitivity line 962
52. theorem OAI.SidorenkoCounterexample.pairing_from_lagrangian_surjective line 1005
53. theorem OAI.SidorenkoCounterexample.exists_pair_block line 1028

    Source documentation

    A dual to a pair-intersection space may be chosen inside the third Lagrangian; the resulting block is nondegenerate and has canonical coordinates.

    theorem exists_pair_block (ha : ω.IsAlt)
        (S N : Submodule K E) (hS : S ≤ ω.orthogonal S)
        (hN : ω.orthogonal N = N) (hSN : S ⊓ N = ⊥) :
        ∃ B : Submodule K E, (ω.restrict B).Nondegenerate ∧ S ≤ B ∧
          ∃ e : (S × Module.Dual K S) ≃ₗ[K] B,
            (∀ s : S, (e (s,0)).val = s.val) ∧
            (∀ f : Module.Dual K S, (e (0,f)).val ∈ N) ∧
            ∀ x y, ω (e x).val (e y).val = canonicalSymplectic x y := by
    …

    Mentions: OAI.SidorenkoCounterexample.canonicalSymplectic

54. theorem OAI.SidorenkoCounterexample.forced_orthogonal_splitting line 1089

    Source documentation

    A Lagrangian containing a Lagrangian of a nondegenerate block splits orthogonally over that block. No choice of extensions is hidden here.

    theorem forced_orthogonal_splitting (ha : ω.IsAlt)
        (B L : Submodule K E) (hB : (ω.restrict B).Nondegenerate)
        (hL : L ≤ ω.orthogonal L) (T : Submodule K B)
        (hT : (ω.restrict B).orthogonal T = T) (hTL : T.map B.subtype ≤ L) :
        L = T.map B.subtype ⊔ (L ⊓ ω.orthogonal B) := by
    …

55. theorem OAI.SidorenkoCounterexample.split_residual_lagrangian line 1119

    Source documentation

    The remaining part of a split Lagrangian is a Lagrangian for the restricted form on the orthogonal complement.

    theorem split_residual_lagrangian (ha : ω.IsAlt)
        (B L : Submodule K E) (hB : (ω.restrict B).Nondegenerate)
        (hL : ω.orthogonal L = L) (T : Submodule K B)
        (hT : (ω.restrict B).orthogonal T = T) (hTL : T.map B.subtype ≤ L) :
        (ω.restrict (ω.orthogonal B)).orthogonal
          (L.comap (ω.orthogonal B).subtype) = L.comap (ω.orthogonal B).subtype := by
    …