MinimalExtensions.lean`

147 declarations, 0 contain sorry, 0 declared as axioms

Minimal-boundary extension sheaves, graded splittings and sheaf decomposition.

def OAI.KLInvariance.MomentGraph.GradedSheaf.lowerAt line 20
Source documentation
The actual lower restriction, with its source explicitly identified.
```
def lowerAt (x : V) (e : Sheaf.Outgoing (G := G) x) :
…
```
Mentions: OAI.KLInvariance.MomentGraph.Sheaf.Outgoing
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lowerAt_map line 25
def OAI.KLInvariance.MomentGraph.GradedSheaf.upwardSubmodule line 31
Source documentation
The same kernel, typed in the graded stalk so base-field instances are explicit.
```
def upwardSubmodule (x : V) (F : Set (Sheaf.Outgoing (G := G) x)) :
…
```
Mentions: OAI.KLInvariance.MomentGraph.Sheaf.Outgoing
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.upwardKernel_homogeneous line 34
def OAI.KLInvariance.MomentGraph.GradedSheaf.upwardKernel line 43
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.upwardKernel_insert line 47
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.hilbert_edge_increment line 59
def OAI.KLInvariance.MomentGraph.GradedSheaf.stalkHom line 93
theorem OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.extend_stalk_graded line 116
def OAI.KLInvariance.Graded.ModuleData.equivOfEq line 182
theorem OAI.KLInvariance.Graded.ModuleData.equivOfEq_graded line 185
theorem OAI.KLInvariance.Graded.ModuleData.quotient_iso_graded line 190
structure OAI.KLInvariance.MomentGraph.GradedSheaf.Iso line 210
structure OAI.KLInvariance.MomentGraph.GradedSheaf.OnIso line 214
def OAI.KLInvariance.MomentGraph.GradedSheaf.OnIso.ofUniv line 224
def OAI.KLInvariance.MomentGraph.GradedSheaf.OnIso.extend line 229
def OAI.KLInvariance.MomentGraph.Sheaf.zero line 271
def OAI.KLInvariance.MomentGraph.Sheaf.prod line 277
lemma OAI.KLInvariance.MomentGraph.Sheaf.prod_generated line 283
lemma OAI.KLInvariance.MomentGraph.Sheaf.prod_flabby line 290
lemma OAI.KLInvariance.MomentGraph.Sheaf.prod_upperQuotient line 298
lemma OAI.KLInvariance.MomentGraph.Sheaf.pi_upperQuotient line 315
lemma OAI.KLInvariance.MomentGraph.Sheaf.prod_kernel_iff line 332
lemma OAI.KLInvariance.MomentGraph.Sheaf.prod_minimal line 352
def OAI.KLInvariance.MomentGraph.Sheaf.addZeroRight line 382
lemma OAI.KLInvariance.MomentGraph.Sheaf.addZeroRight_apply line 391
def OAI.KLInvariance.MomentGraph.Sheaf.OnIso.prodZero line 395
lemma OAI.KLInvariance.MomentGraph.Sheaf.pi_subsingleton_vertex line 413
lemma OAI.KLInvariance.MomentGraph.Sheaf.pi_subsingleton_edge line 417
def OAI.KLInvariance.Graded.ModuleData.zero line 433
def OAI.KLInvariance.Graded.ModuleData.Hom.zero line 448
def OAI.KLInvariance.Graded.ModuleData.Hom.pi line 451
def OAI.KLInvariance.MomentGraph.GradedSheaf.shift line 465
def OAI.KLInvariance.MomentGraph.GradedSheaf.zero line 471
def OAI.KLInvariance.MomentGraph.GradedSheaf.prod line 477
def OAI.KLInvariance.MomentGraph.GradedSheaf.pi line 483
def OAI.KLInvariance.MomentGraph.GradedSheaf.OnIso.prodZero line 490
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.shift_forget line 498
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.zero_forget line 500
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.prod_forget line 501
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.pi_forget line 503
def OAI.KLInvariance.MomentGraph.lowerGraph line 522
abbrev OAI.KLInvariance.MomentGraph.GradedSheaf.Witness line 531
def OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtend line 535
def OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtendVertex line 546
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtendVertex_graded line 556
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtend_support line 560
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtend_free line 563
def OAI.KLInvariance.MomentGraph.GradedSheaf.liftLowerAssignment line 569
def OAI.KLInvariance.MomentGraph.GradedSheaf.projectLowerAssignment line 572
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.projectLower_compatible line 575
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.liftLower_compatible line 581
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtend_generated line 588
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtend_flabby line 598
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtend_quotient line 607
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lowerExtend_minimal line 627
instance OAI.KLInvariance.MomentGraph.GradedSheaf.zeroVertex_subsingleton line 656
instance OAI.KLInvariance.MomentGraph.GradedSheaf.zeroEdge_subsingleton line 658
structure OAI.KLInvariance.MomentGraph.GradedSheaf.BoundaryModels line 661
inductive OAI.KLInvariance.MomentGraph.GradedSheaf.ModelSum line 672
lemma OAI.KLInvariance.MomentGraph.GradedSheaf.ModelSum.mono line 683
lemma OAI.KLInvariance.MomentGraph.GradedSheaf.ModelSum.free line 689
lemma OAI.KLInvariance.MomentGraph.GradedSheaf.ModelSum.quotient line 698
lemma OAI.KLInvariance.MomentGraph.GradedSheaf.ModelSum.generated line 707
lemma OAI.KLInvariance.MomentGraph.GradedSheaf.ModelSum.flabby line 715
lemma OAI.KLInvariance.MomentGraph.GradedSheaf.ModelSum.minimal line 720
def OAI.KLInvariance.MomentGraph.lowerBoundary line 757
def OAI.KLInvariance.MomentGraph.actualBoundaryModels line 762
theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.extend_iso line 806
theorem OAI.KLInvariance.MomentGraph.BoundarySheaf.exists_gradedIso line 829
def OAI.KLInvariance.MomentGraph.Sheaf.quotientLinear line 888
def OAI.KLInvariance.MomentGraph.Sheaf.structureSheaf line 891
theorem OAI.KLInvariance.MomentGraph.Sheaf.structureSheaf_free line 898
theorem OAI.KLInvariance.MomentGraph.Sheaf.structureSheaf_finite line 901
theorem OAI.KLInvariance.MomentGraph.Sheaf.structureSheaf_support line 904
def OAI.KLInvariance.MomentGraph.Sheaf.structureVertexIso line 908
theorem OAI.KLInvariance.MomentGraph.Sheaf.structureSheaf_generated line 917
theorem OAI.KLInvariance.MomentGraph.Sheaf.structureSheaf_upperQuotient line 925
theorem OAI.KLInvariance.MomentGraph.Sheaf.structureSheaf_minimal line 944
def OAI.KLInvariance.MomentGraph.Sheaf.baseChange line 989
def OAI.KLInvariance.MomentGraph.Sheaf.tensorAssignments line 995
theorem OAI.KLInvariance.MomentGraph.Sheaf.tensorAssignments_tmul line 998
lemma OAI.KLInvariance.MomentGraph.Sheaf.baseChange_tmul_compatible line 1001
def OAI.KLInvariance.MomentGraph.Sheaf.tensorSections line 1007
theorem OAI.KLInvariance.MomentGraph.Sheaf.tensorSections_tmul line 1016
theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChange_generated line 1019

def OAI.KLInvariance.MomentGraph.Sheaf.constraint line 1031

Source documentation

The finite section constraint whose kernel is the actual section module.

noncomputable def constraint (Ω : Set V) : B.Assignment →ₗ[R]
    (∀ e : {e : E // G.source e ∈ Ω ∧ G.target e ∈ Ω}, B.edge e.val) :=
…

lemma OAI.KLInvariance.MomentGraph.Sheaf.ker_constraint line 1036
theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChange_vertex_free line 1061
theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChange_vertex_finite line 1065
theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChange_upperQuotient line 1069
theorem OAI.KLInvariance.MomentGraph.Sheaf.tensorAssignments_bijective line 1102
theorem OAI.KLInvariance.MomentGraph.Sheaf.constraint_tensorAssignments line 1107
theorem OAI.KLInvariance.MomentGraph.Sheaf.tensorSections_surjective line 1121
theorem OAI.KLInvariance.MomentGraph.Sheaf.tensorSections_injective line 1147
def OAI.KLInvariance.MomentGraph.Sheaf.tensorSectionsEquiv line 1157
Source documentation
Sections over every vertex subset commute with flat extension of scalars for a finite moment graph. No freeness or BMP character input is used.
```
 def tensorSectionsEquiv [Finite V] [Finite E] [Module.Flat R S] (Ω : Set V) :
    S ⊗[R] B.sections Ω ≃ₗ[S] (B.baseChange S).sections Ω :=
…
```
Mentions: OAI.KLInvariance.MomentGraph.Sheaf.sections
theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChange_flabby line 1162
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.flabby line 1206
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.generated line 1217
def OAI.KLInvariance.MomentGraph.Sheaf.baseChangeScalar line 1228
theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChangeScalar_tmul line 1230
theorem OAI.KLInvariance.MomentGraph.Sheaf.span_map line 1235
def OAI.KLInvariance.MomentGraph.Sheaf.baseChangeQuotient line 1239
theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChangeQuotient_tmul line 1244
def OAI.KLInvariance.MomentGraph.Sheaf.baseChangePiScalar line 1253
def OAI.KLInvariance.MomentGraph.Sheaf.baseChangePiQuotient line 1259
theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChangePiScalar_tmul line 1267
theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChangePiQuotient_tmul line 1271
def OAI.KLInvariance.MomentGraph.Sheaf.quotientPullback line 1275
theorem OAI.KLInvariance.MomentGraph.Sheaf.baseChangePi_natural line 1280
def OAI.KLInvariance.MomentGraph.Sheaf.structureBaseChangeIso line 1295
theorem OAI.KLInvariance.MomentGraph.Sheaf.structureSheaf_flat_flabby line 1304
def OAI.KLInvariance.MomentGraph.inducedGraph line 1323
def OAI.KLInvariance.MomentGraph.Sheaf.restrict line 1333
def OAI.KLInvariance.MomentGraph.Sheaf.restrictAssignment line 1339
def OAI.KLInvariance.MomentGraph.Sheaf.extendAssignment line 1341
theorem OAI.KLInvariance.MomentGraph.Sheaf.extendAssignment_mem line 1345
theorem OAI.KLInvariance.MomentGraph.Sheaf.restrict_compatible line 1353
theorem OAI.KLInvariance.MomentGraph.Sheaf.restrict_global line 1358
theorem OAI.KLInvariance.MomentGraph.Sheaf.restrict_generated line 1363
theorem OAI.KLInvariance.MomentGraph.Sheaf.extend_compatible line 1368
theorem OAI.KLInvariance.MomentGraph.Sheaf.restrict_flabby_live line 1385
Source documentation
The induced subgraph may use upper sets which are not ambient upper sets. All nonzero exiting edges must stay in the subgraph.
```
 theorem restrict_flabby_live [Finite V] (hb : B.Flabby) (live : Set E)
    (hdead : ∀ e, e ∉ live → Subsingleton (B.edge e))
    (hclosed : ∀ e ∈ live, G.source e ∈ K → G.target e ∈ K) :
    (B.restrict K).Flabby := by
…
```
Mentions: OAI.KLInvariance.MomentGraph.Sheaf.Flabby
theorem OAI.KLInvariance.MomentGraph.Sheaf.restrict_quotient line 1406
def OAI.KLInvariance.MomentGraph.Sheaf.structureRestrictIso line 1419
theorem OAI.KLInvariance.MomentGraph.Sheaf.structureSheaf_edge_subsingleton line 1427
theorem OAI.KLInvariance.MomentGraph.Sheaf.structureSheaf_lowerIdeal_flabby line 1431
structure OAI.KLInvariance.MomentGraph.GraphMap line 1457
def OAI.KLInvariance.MomentGraph.Sheaf.moduleEq line 1468
theorem OAI.KLInvariance.MomentGraph.Sheaf.moduleEq_apply line 1470
def OAI.KLInvariance.MomentGraph.Sheaf.pullback line 1473
def OAI.KLInvariance.MomentGraph.Sheaf.pullAssignment line 1479
theorem OAI.KLInvariance.MomentGraph.Sheaf.pull_lower line 1481
theorem OAI.KLInvariance.MomentGraph.Sheaf.pull_upper line 1486
theorem OAI.KLInvariance.MomentGraph.Sheaf.pull_global line 1491
theorem OAI.KLInvariance.MomentGraph.Sheaf.pullback_generated line 1497
def OAI.KLInvariance.MomentGraph.Sheaf.pushAssignment line 1502
theorem OAI.KLInvariance.MomentGraph.Sheaf.pull_push line 1507
theorem OAI.KLInvariance.MomentGraph.Sheaf.pullback_flabby_live line 1520
theorem OAI.KLInvariance.MomentGraph.Sheaf.pullback_quotient line 1554
theorem OAI.KLInvariance.MomentGraph.Sheaf.stalkMap_assignment line 1590
theorem OAI.KLInvariance.MomentGraph.Sheaf.pullback_kernel line 1596
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.moduleEq_graded line 1644
def OAI.KLInvariance.MomentGraph.GradedSheaf.pullback line 1650
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.forget_pullback line 1658
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.pullback_edgeFlabby line 1660
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.pullback_kernelMinimal line 1690
def OAI.KLInvariance.MomentGraph.BoundarySheaf.pullback line 1716