GradedSheaves.lean`

112 declarations, 0 contain sorry, 0 declared as axioms

Graded moment-graph sheaves, boundary sections, graded covers and morphisms.

structure OAI.KLInvariance.MomentGraph.GradedSheaf line 20
def OAI.KLInvariance.MomentGraph.GradedSheaf.forget line 29
def OAI.KLInvariance.MomentGraph.GradedSheaf.EdgeFlabby line 37
Source documentation
Extension for sets closed under actual edges. It implies the source's ordinary flabbiness, and is convenient for the descending construction.
```
def EdgeFlabby : Prop :=
…
```
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.EdgeFlabby.flabby line 42
def OAI.KLInvariance.MomentGraph.GradedSheaf.assignments line 48
def OAI.KLInvariance.MomentGraph.GradedSheaf.lowerGlobal line 50
def OAI.KLInvariance.MomentGraph.GradedSheaf.upperGlobal line 53
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.sections_homogeneous line 57
def OAI.KLInvariance.MomentGraph.GradedSheaf.sections line 65
def OAI.KLInvariance.MomentGraph.GradedSheaf.boundary line 68
def OAI.KLInvariance.MomentGraph.GradedSheaf.boundaryHom line 74
def OAI.KLInvariance.MomentGraph.GradedSheaf.boundaryImage line 81
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.exists_boundaryCover line 84
def OAI.KLInvariance.MomentGraph.bottomGraph line 108
Source documentation
Adjoin a vertex below the old vertices, with specified outgoing edges. Only the edge orientations, not the extra comparabilities, enter sections.
```
def bottomGraph (τ : D → V) : OrderedGraph (WithBot V) (E ⊕ D) where
…
```
Mentions: OAI.KLInvariance.MomentGraph.OrderedGraph
def OAI.KLInvariance.MomentGraph.GradedSheaf.attachEdges line 122
def OAI.KLInvariance.MomentGraph.GradedSheaf.attachQuotient line 125
def OAI.KLInvariance.MomentGraph.GradedSheaf.attachBoundary line 129
def OAI.KLInvariance.MomentGraph.GradedSheaf.attachBoundaryMap line 132
def OAI.KLInvariance.MomentGraph.GradedSheaf.attachImage line 140
def OAI.KLInvariance.MomentGraph.GradedSheaf.attachStalkMap line 145
def OAI.KLInvariance.MomentGraph.GradedSheaf.extendBottom line 150
def OAI.KLInvariance.MomentGraph.GradedSheaf.attachAssignment line 166
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.attachAssignment_global line 169
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.lift_global line 179
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.extendBottom_generated line 190
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.extendBottom_edgeFlabby line 207
def OAI.KLInvariance.Graded.ModuleData.Hom.ofEq line 251
theorem OAI.KLInvariance.Graded.ModuleData.Hom.ofEq_rfl line 253
theorem OAI.KLInvariance.Graded.ModuleData.Hom.ofEq_apply line 255
structure OAI.KLInvariance.MomentGraph.GraphEquiv line 270
Source documentation
An isomorphism of directed graphs, with no order-reflection requirement.
```
structure GraphEquiv (G : OrderedGraph V E) (H : OrderedGraph W F) where
…
```
Mentions: OAI.KLInvariance.MomentGraph.OrderedGraph
def OAI.KLInvariance.MomentGraph.GradedSheaf.reindex line 279
def OAI.KLInvariance.MomentGraph.GradedSheaf.reindexAssignment line 285
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.reindex_lower line 288
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.reindex_upper line 296
def OAI.KLInvariance.MomentGraph.GradedSheaf.unreindexAssignment line 304
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.unreindex_reindexAssignment line 308
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.reindex_unreindexAssignment line 313
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.reindex_global line 325
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.reindex_generated line 331
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.reindex_edgeFlabby line 336
theorem OAI.KLInvariance.Graded.ModuleData.Hom.ofEq_bijective line 376
def OAI.KLInvariance.Graded.ModuleData.unit line 379
instance OAI.KLInvariance.Graded.ModuleData.unit_free line 383
def OAI.KLInvariance.MomentGraph.GradedSheaf.FreeStalks line 397
def OAI.KLInvariance.MomentGraph.GradedSheaf.UpperQuotient line 401
Source documentation
The genuine upper-end quotient rule, expressed without choosing a quotient presentation of the edge object.
```
 def UpperQuotient (B : GradedSheaf (𝓐 := 𝓐) G) (α : E → A) : Prop :=
…
```
Mentions: OAI.KLInvariance.MomentGraph.GradedSheaf
def OAI.KLInvariance.MomentGraph.GradedSheaf.KernelMinimal line 407
Source documentation
Minimality of the full outgoing boundary cover. The assignment formulation avoids dependent casts and is equivalent to the usual kernel containment.
```
 def KernelMinimal (B : GradedSheaf (𝓐 := 𝓐) G) (x : V) : Prop :=
…
```
Mentions: OAI.KLInvariance.MomentGraph.GradedSheaf
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.kernelMinimal_iff line 412
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.reindex_freeStalks line 434
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.reindex_upperQuotient line 437
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.reindex_kernelMinimal line 453
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.extendBottom_freeStalks line 472
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.extendBottom_upperQuotient line 479
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.extendBottom_kernelMinimal_bot line 493
theorem OAI.KLInvariance.MomentGraph.GradedSheaf.extendBottom_kernelMinimal_coe line 501
structure OAI.KLInvariance.MomentGraph.Sheaf.Iso line 521
def OAI.KLInvariance.MomentGraph.Sheaf.Iso.symm line 531
def OAI.KLInvariance.MomentGraph.Sheaf.Iso.assignments line 541
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.compatible_iff line 544
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.map_sections line 553
def OAI.KLInvariance.MomentGraph.Sheaf.Iso.sections line 565
def OAI.KLInvariance.MomentGraph.Sheaf.Iso.boundary line 568
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.stalkMap line 571
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.boundaryMap line 578
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.map_boundaryRange line 583
def OAI.KLInvariance.MomentGraph.Sheaf.upwardKernel line 599
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.upwardKernel_iff line 609
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.map_upwardKernel line 620
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.map_lowerImage line 631
theorem OAI.KLInvariance.MomentGraph.Sheaf.Iso.map_upperImage line 639
def OAI.KLInvariance.EmbeddedModule.scaled line 654
theorem OAI.KLInvariance.EmbeddedModule.map_scaled line 657
theorem OAI.KLInvariance.EmbeddedModule.map_eq_scaled_iff line 665
Source documentation
Scalar comparison is transported by one and the same edge isomorphism.
```
theorem map_eq_scaled_iff (j : M ≃ₗ[R] N) (r : R) (I J : Submodule R M) :
    I.map j.toLinearMap = scaled r (J.map j.toLinearMap) ↔ I = scaled r J := by
…
```
Mentions: OAI.KLInvariance.EmbeddedModule.scaled
structure OAI.KLInvariance.MomentGraph.Sheaf.AboveIso line 692
Source documentation
An isomorphism already constructed strictly above x, including the edge modules whose upper endpoints are above x. The latter are canonically supplied by the upper quotient rule in the local decomposition.
```
structure AboveIso where
…
```
def OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.symm line 704
def OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.mapAssignment line 714
lemma OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.mapAssignment_at line 719
lemma OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.compatible line 724
def OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.boundary line 732
lemma OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.boundaryMap line 735
lemma OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.map_boundaryImage line 743
lemma OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.map_stalk_image line 756

theorem OAI.KLInvariance.MomentGraph.Sheaf.AboveIso.extend_stalk line 766

Source documentation

One genuine descending splitting: the finite-free new top summand is proved from the local-ring minimum cover, and all outgoing restriction maps commute with the selected edge isomorphisms.

theorem extend_stalk [IsLocalRing R]
    [Module.Free R (B.vertex x)] [Module.Finite R (B.vertex x)]
    [Module.Free R (C.vertex x)] [Module.Finite R (C.vertex x)]
    (hBf : B.Flabby) (hBg : B.Generated) (hCf : C.Flabby) (hCg : C.Generated)
    (hmin : LinearMap.ker (C.stalkMap x) ≤
      IsLocalRing.maximalIdeal R • (⊤ : Submodule R (C.vertex x))) :
    ∃ (g : B.vertex x →ₗ[R] C.vertex x)
      (jv : B.vertex x ≃ₗ[R] C.vertex x × LinearMap.ker g),
      Module.Free R (LinearMap.ker g) ∧ Module.Finite R (LinearMap.ker g) ∧
      ∀ (b : B.vertex x) (e : Outgoing (G := G) x),
…

Mentions: OAI.KLInvariance.MomentGraph.Sheaf.Outgoing

def OAI.KLInvariance.MomentGraph.Sheaf.pi line 819
Source documentation
Finite direct sums represented by products, as used in the plane localization.
```
def pi (B : ι → Sheaf.{u,v,w,z} (R := R) G) : Sheaf (R := R) G where
…
```
Mentions: OAI.KLInvariance.MomentGraph.Sheaf
lemma OAI.KLInvariance.MomentGraph.Sheaf.pi_compatible line 825
lemma OAI.KLInvariance.MomentGraph.Sheaf.pi_generated line 835
lemma OAI.KLInvariance.MomentGraph.Sheaf.pi_flabby line 842
lemma OAI.KLInvariance.MomentGraph.Sheaf.pi_kernel_iff line 849

lemma OAI.KLInvariance.LocalCover.pi_mem_ideal_smul line 874

Source documentation

Coordinatewise membership in the ideal multiple of a finite product.

lemma pi_mem_ideal_smul (I : Ideal R) (f : ∀ i, M i)
    (hf : ∀ i, f i ∈ I • (⊤ : Submodule R (M i))) :
    f ∈ I • (⊤ : Submodule R (∀ i, M i)) := by
…

lemma OAI.KLInvariance.MomentGraph.Sheaf.pi_minimal line 893

def OAI.KLInvariance.QuotientEdge.iso line 913

Source documentation

The edge isomorphism forced by an upper stalk isomorphism and exact quotient maps.

noncomputable def iso (f : M →ₗ[R] E) (g : N →ₗ[R] F)
    (hf : Function.Surjective f) (hg : Function.Surjective g)
    (h : M ≃ₗ[R] N) (hk : (LinearMap.ker f).map h.toLinearMap = LinearMap.ker g) : E ≃ₗ[R] F :=
…

lemma OAI.KLInvariance.QuotientEdge.iso_apply line 919
lemma OAI.KLInvariance.QuotientEdge.map_kernel_scalar line 925

theorem OAI.KLInvariance.QuotientEdge.exists_scalar_iso line 940

Source documentation

No separate choice of edge data or scalar compatibility hypothesis is needed.

theorem exists_scalar_iso (f : M →ₗ[R] E) (g : N →ₗ[R] F) (r : R)
    (hfs : Function.Surjective f) (hgs : Function.Surjective g)
    (hf : ∀ v, f v = 0 ↔ ∃ w, v = r • w)
    (hg : ∀ v, g v = 0 ↔ ∃ w, v = r • w) (h : M ≃ₗ[R] N) :
    ∃ j : E ≃ₗ[R] F, ∀ v, j (f v) = g (h v) :=
…

def OAI.KLInvariance.MomentGraph.Sheaf.UpperQuotient line 963
def OAI.KLInvariance.MomentGraph.Sheaf.castStalkIso line 967
structure OAI.KLInvariance.MomentGraph.Sheaf.OnIso line 970
def OAI.KLInvariance.MomentGraph.Sheaf.OnIso.above line 981
def OAI.KLInvariance.MomentGraph.Sheaf.OnIso.ofUniv line 987

def OAI.KLInvariance.MomentGraph.Sheaf.OnIso.extend line 995

Source documentation

Given the new stalk and its outgoing commuting squares, all new incoming edges are forced by the scalar quotient rule.

noncomputable def extend (hU : IsUpperSet U) (x : V) (hx : x ∉ U)
    (hmax : Set.Ioi x ⊆ U) (α : E → R)
    (hBq : B.UpperQuotient α) (hCq : C.UpperQuotient α)
    (jv : B.vertex x ≃ₗ[R] C.vertex x)
    (hout : ∀ e (he : G.source e = x) v,
      j.edge e (hmax (lt_of_eq_of_lt he.symm (G.increasing e)))
        (B.lower e v) = C.lower e (castStalkIso B C he.symm jv v)) :
    OnIso B C (insert x U) := by
…

Mentions: OAI.KLInvariance.MomentGraph.Sheaf.castStalkIso, OAI.KLInvariance.MomentGraph.Sheaf.OnIso

def OAI.KLInvariance.MomentGraph.removeGraph line 1054
def OAI.KLInvariance.MomentGraph.removeTarget line 1060
def OAI.KLInvariance.MomentGraph.splitVertex line 1063
def OAI.KLInvariance.MomentGraph.splitEdge line 1075
theorem OAI.KLInvariance.MomentGraph.splitVertex_self line 1088
theorem OAI.KLInvariance.MomentGraph.splitVertex_ne line 1093
def OAI.KLInvariance.MomentGraph.splitGraph line 1098
theorem OAI.KLInvariance.MomentGraph.splitEdge_labels line 1115
structure OAI.KLInvariance.MomentGraph.BoundarySheaf line 1138
Source documentation
The outcome of the actual minimal boundary construction. Full upward-kernel freeness, integral duality and KL characters are NOT part of this structure.
```
structure BoundarySheaf {V E : Type um} [PartialOrder V] (G : OrderedGraph V E)
    (α : E → A) (b : V) where
…
```
Mentions: OAI.KLInvariance.MomentGraph.OrderedGraph
def OAI.KLInvariance.MomentGraph.singletonSheaf line 1150
theorem OAI.KLInvariance.MomentGraph.singleton_boundarySheaf line 1156
theorem OAI.KLInvariance.MomentGraph.exists_boundarySheaf_card line 1177
theorem OAI.KLInvariance.MomentGraph.exists_boundarySheaf line 1238