PlaneLocalization.lean`

132 declarations, 0 contain sorry, 0 declared as axioms

Symmetric plane ideals, sheaf localization and scaled local products along genuine edges.

def OAI.KLInvariance.SymmetricPlaneIdeal.ideal line 16
def OAI.KLInvariance.SymmetricPlaneIdeal.quotientMap line 19
theorem OAI.KLInvariance.SymmetricPlaneIdeal.quotientMap_ι line 23
theorem OAI.KLInvariance.SymmetricPlaneIdeal.ideal_le_ker line 27
def OAI.KLInvariance.SymmetricPlaneIdeal.forward line 33
def OAI.KLInvariance.SymmetricPlaneIdeal.linearQuotient line 37
def OAI.KLInvariance.SymmetricPlaneIdeal.backward line 44
theorem OAI.KLInvariance.SymmetricPlaneIdeal.forward_mk line 47
theorem OAI.KLInvariance.SymmetricPlaneIdeal.backward_ι_mk line 50
def OAI.KLInvariance.SymmetricPlaneIdeal.quotientEquiv line 56
theorem OAI.KLInvariance.SymmetricPlaneIdeal.quotientEquiv_mk_ι line 76
theorem OAI.KLInvariance.SymmetricPlaneIdeal.ι_mem_iff line 80
theorem OAI.KLInvariance.SymmetricPlaneIdeal.ideal_eq_ker line 98
instance OAI.KLInvariance.SymmetricPlaneIdeal.ideal_isPrime line 107
theorem OAI.KLInvariance.SymmetricPlaneIdeal.ideal_span_eq line 111
theorem OAI.KLInvariance.MomentGraph.Sheaf.extend_modelSum line 147
theorem OAI.KLInvariance.MomentGraph.Sheaf.exists_modelSumIso line 207
Source documentation
Actual finite descending decomposition over a local ring. This does not assume that localization preserves indecomposability. Its explicitly stated rank-one model criteria must be proved before applying it to a root plane.
```
theorem exists_modelSumIso [Finite V]
    (hBfree : ∀ x, Module.Free R (B.vertex x))
    (hBfinite : ∀ x, Module.Finite R (B.vertex x))
    (hBq : B.UpperQuotient α) (hBf : B.Flabby) (hBg : B.Generated) :
    ∃ C : Sheaf.{u,v,w,z} (R := R) G,
…
```
theorem OAI.KLInvariance.BruhatGraph.exists_outgoing_below line 273
def OAI.KLInvariance.MomentGraph.Sheaf.structureLocalModels line 289
def OAI.KLInvariance.TitsSpace.PlaneBasis.localModels line 317
def OAI.KLInvariance.TitsSpace.embedLinear line 346
theorem OAI.KLInvariance.TitsSpace.embedLinear_injective line 351
def OAI.KLInvariance.TitsSpace.planePrime line 355
instance OAI.KLInvariance.TitsSpace.planePrime_isPrime line 359
theorem OAI.KLInvariance.TitsSpace.linear_mem_planePrime_iff line 362
abbrev OAI.KLInvariance.TitsSpace.PlaneRing line 381
theorem OAI.KLInvariance.TitsSpace.linear_mem_maximal_iff line 383
theorem OAI.KLInvariance.TitsSpace.linear_isUnit_iff line 389
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.modelLabel_mem_maximal line 408
def OAI.KLInvariance.TitsSpace.PlaneBasis.localizedModels line 415
def OAI.KLInvariance.TitsSpace.PlaneBasis.CosetVertex line 439
instance OAI.KLInvariance.TitsSpace.PlaneBasis.cosetOrder line 442
def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetAmbient line 448
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.cosetAmbient_injective line 451
instance OAI.KLInvariance.TitsSpace.PlaneBasis.cosetFinite line 457
def OAI.KLInvariance.TitsSpace.PlaneBasis.CosetEdge line 461
def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetGraph line 464
def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetEdgeAmbient line 472
def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetGraphMap line 476
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_lower line 483
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_outgoing_below line 488
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_lift_live line 497
theorem OAI.KLInvariance.MomentGraph.Sheaf.edge_subsingleton_of_unit line 534
def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetLabel line 558
def OAI.KLInvariance.TitsSpace.PlaneBasis.localizedCoset line 562
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.polynomialLabel_unit_iff line 567
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.localizedCoset_quotient line 577
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.localizedCoset_generated line 585
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.localizedCoset_flabby line 591
def OAI.KLInvariance.MomentGraph.Sheaf.propPiEquiv line 621
theorem OAI.KLInvariance.MomentGraph.Sheaf.moduleEq_pi_apply line 630
def OAI.KLInvariance.MomentGraph.Sheaf.structurePullbackIso line 637
def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetInto line 681
def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetIntoEdge line 684
def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetIntoGraph line 688
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.cosetInto_injective line 696
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_label_eq line 703
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_modelLabel_eq line 708
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_model_flabby line 724
def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetModels line 761
def OAI.KLInvariance.MomentGraph.Sheaf.supportedOutgoing line 791
def OAI.KLInvariance.MomentGraph.Sheaf.kernelProduct line 795
theorem OAI.KLInvariance.MomentGraph.Sheaf.structure_kernel_iff_dvd line 798
theorem OAI.KLInvariance.MomentGraph.Sheaf.structure_kernel_product line 823
theorem OAI.KLInvariance.MomentGraph.Sheaf.lower_surjective_of_generated line 857
theorem OAI.KLInvariance.MomentGraph.Sheaf.structure_lower_image line 867
theorem OAI.KLInvariance.MomentGraph.Sheaf.structure_upper_image line 878
theorem OAI.KLInvariance.LocalizationRelativePrime.not_dvd_map line 901
theorem OAI.KLInvariance.LocalizationRelativePrime.map_prime line 909
theorem OAI.KLInvariance.LocalizationRelativePrime.map_relPrime line 918
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.cosetEdgeAmbient_injective line 945
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.cosetLabel_relPrime line 952
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_supported_pairwise line 963
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.coset_kernel_product line 973
def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetUpperVertex line 1001
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.outgoing_step line 1004
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.outgoing_upper line 1013
def OAI.KLInvariance.TitsSpace.PlaneBasis.scheduledOutgoing line 1018
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.outgoing_target_injective line 1024
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.supported_card_count line 1031
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.planeWeight_coset_edge line 1096
Source documentation
The combinatorial factor already constructed from ambient inversion pairs is exactly the intrinsic relative dihedral edge degree.
```
 theorem planeWeight_coset_edge {a₀ : W}
    (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀))
    {x y : planeSubgroup M cs P} (hxy : BruhatStep B.system x y) :
    (planeWeight ((x:W)*a₀) (B.edgeRoot hxy) P).toNat =
      (B.system.length y-B.system.length x-1)/2 := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.TitsSpace.planeWeight
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.cosetEdge_target_upper line 1148
def OAI.KLInvariance.TitsSpace.PlaneBasis.mappedCosetRoot line 1152
def OAI.KLInvariance.TitsSpace.PlaneBasis.scheduledLower line 1159
def OAI.KLInvariance.TitsSpace.PlaneBasis.scheduledUpper line 1163
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.scheduledLower_self line 1168
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.supported_count_difference line 1175
def OAI.KLInvariance.BruhatGraph.ambientLater line 1215
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.scheduledOutgoing_eq line 1237
theorem OAI.KLInvariance.PlaneReduction.scalar_reduction line 1268
theorem OAI.KLInvariance.PlaneReduction.associated_reduction line 1281
def OAI.KLInvariance.TitsSpace.localizedLinear line 1305
def OAI.KLInvariance.TitsSpace.localizedEdgeIdeal line 1309
abbrev OAI.KLInvariance.TitsSpace.LocalizedEdgeRing line 1312
def OAI.KLInvariance.TitsSpace.localizedReduction line 1315
theorem OAI.KLInvariance.TitsSpace.localizedReduction_self line 1320
theorem OAI.KLInvariance.TitsSpace.positiveRoot_not_line line 1324
theorem OAI.KLInvariance.TitsSpace.localizedReduction_associated line 1330
def OAI.KLInvariance.BruhatGraph.polynomialRoot line 1356
theorem OAI.KLInvariance.BruhatGraph.polynomialRoot_homogeneous line 1360
theorem OAI.KLInvariance.BruhatGraph.polynomialRoot_prime line 1372
theorem OAI.KLInvariance.BruhatGraph.polynomialRoot_not_dvd line 1379
def OAI.KLInvariance.BruhatGraph.edgeFactorLift line 1389
theorem OAI.KLInvariance.BruhatGraph.edgeFactorLift_homogeneous line 1393
theorem OAI.KLInvariance.BruhatGraph.edgeFactorLift_not_dvd line 1404
theorem OAI.KLInvariance.BruhatGraph.edgeFactorLift_reduction line 1413
theorem OAI.KLInvariance.BruhatGraph.rootRef_root line 1424
theorem OAI.KLInvariance.BruhatGraph.root_not_inverted line 1429
theorem OAI.KLInvariance.BruhatGraph.edgeFactorDegree_edge line 1440
def OAI.KLInvariance.BruhatGraph.edgeFactorMap line 1449
Source documentation
Multiplication by the genuine plane product on the actual edge module.
```
 def edgeFactorMap (e : Edge cs u b) : B.sheaf.edge e →ₗ[Coefficient (σ := σ)] B.sheaf.edge e :=
…
```
Mentions: OAI.KLInvariance.BruhatGraph.Edge, OAI.KLInvariance.BruhatGraph.Coefficient
theorem OAI.KLInvariance.BruhatGraph.edgeFactorMap_graded line 1453
theorem OAI.KLInvariance.BruhatGraph.edgeFactorLift_regular line 1462
theorem OAI.KLInvariance.LocalProducts.smul_top_le_of_map_dvd line 1488
theorem OAI.KLInvariance.LocalProducts.smul_top_eq_of_map_associated line 1498
theorem OAI.KLInvariance.LocalProducts.associated_prod_power line 1505
theorem OAI.KLInvariance.LocalProducts.associated_prod_scale line 1509

theorem OAI.KLInvariance.LocalProducts.product_image_scale line 1523

Source documentation

The local embedded product images agree whenever the reduced labels are associated and the actual later-edge count has the required difference.

 theorem product_image_scale (s : Finset ι) (t : Finset κ) (a : ι → R) (b : κ → R)
    (p : S) (f : R) (k : ℕ)
    (ha : ∀ i ∈ s, Associated (algebraMap R S (a i)) p)
    (hb : ∀ j ∈ t, Associated (algebraMap R S (b j)) p)
    (hf : Associated (algebraMap R S f) (p^k)) (hcount : s.card=t.card+k) :
    (∏ i ∈ s, a i) • (⊤ : Submodule R M) =
      f • ((∏ j ∈ t, b j) • (⊤ : Submodule R M)) := by
…

theorem OAI.KLInvariance.TitsSpace.polynomialRoot_localized line 1551
theorem OAI.KLInvariance.TitsSpace.polynomialRoot_reduced line 1555
theorem OAI.KLInvariance.TitsSpace.planeRoot_outside line 1560
theorem OAI.KLInvariance.TitsSpace.reduced_planeRoot_other_isUnit line 1569
theorem OAI.KLInvariance.TitsSpace.edgeFactor_local_associated line 1579
Source documentation
The actual integral edge factor reduces, in each actual plane, to precisely its plane weight. All other factors are proven units, not discarded formally.
```
 theorem edgeFactor_local_associated (x : W) (a b : PositiveRoot M cs) (hab : a ≠ b) :
    Associated
      (algebraMap (PlaneRing basis (rootPlane a b)) (LocalizedEdgeRing basis (rootPlane a b) a.val)
        (algebraMap (MvPolynomial σ ℝ) (PlaneRing basis (rootPlane a b)) (edgeFactorLift cs basis x a)))
      ((localizedReduction basis (rootPlane a b) a.val b.val)^((planeWeight x a (rootPlane a b)).toNat)) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.PlaneRing, OAI.KLInvariance.TitsSpace.rootPlane, OAI.KLInvariance.TitsSpace.LocalizedEdgeRing, OAI.KLInvariance.TitsSpace.localizedReduction, OAI.KLInvariance.TitsSpace.planeWeight
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.cosetRoot_eq line 1635
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.cosetLabel_eq_root line 1640
def OAI.KLInvariance.TitsSpace.PlaneBasis.reducedCosetRoot line 1647
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.cosetLabel_reduction_associated line 1651
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.cosetFactor_reduction_associated line 1663
def OAI.KLInvariance.BruhatGraph.upperSource line 1696
def OAI.KLInvariance.BruhatGraph.upperTarget line 1698
def OAI.KLInvariance.BruhatGraph.mappedEdgeRoot line 1700
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.exists_coset_edge line 1715
theorem OAI.KLInvariance.TitsSpace.PlaneBasis.mappedCosetRoot_eq line 1744