Sheaves.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Ordered moment graphs, sheaves, flabbiness, sections and boundary images.

structure OAI.KLInvariance.MomentGraph.OrderedGraph line 21
structure OAI.KLInvariance.MomentGraph.Sheaf line 28
abbrev OAI.KLInvariance.MomentGraph.Sheaf.Assignment line 37
def OAI.KLInvariance.MomentGraph.Sheaf.CompatibleOn line 41
Source documentation
Exactly the usual section compatibility on edges with both endpoints in Ω; coordinates outside Ω are ignored and can be chosen arbitrarily.
```
def CompatibleOn (Ω : Set V) (f : B.Assignment) : Prop :=
…
```
def OAI.KLInvariance.MomentGraph.Sheaf.IsGlobal line 45
def OAI.KLInvariance.MomentGraph.Sheaf.Flabby line 48
Source documentation
Extension of ordinary sections over ambient upper sets.
```
def Flabby : Prop :=
…
```
def OAI.KLInvariance.MomentGraph.Sheaf.ClosedUnder line 54
Source documentation
Closure under the edges whose modules survive, strictly weaker than being an ambient upper set.
```
def ClosedUnder (_B : Sheaf (R := R) G) (live : Set E) (Ω : Set V) : Prop :=
…
```
Mentions: OAI.KLInvariance.MomentGraph.Sheaf
theorem OAI.KLInvariance.MomentGraph.Sheaf.compatible_mono line 57

theorem OAI.KLInvariance.MomentGraph.Sheaf.extend_one line 63

Source documentation

One step of the descending extension in loc:relative-flabbiness. Previously assigned lower neighbors can only be on zero edge modules.

theorem extend_one (hb : B.Flabby) (live : Set E)
    (hdead : ∀ e, e ∉ live → Subsingleton (B.edge e))
    (Ω : Set V) (hΩ : B.ClosedUnder live Ω) (a : V) (ha : a ∉ Ω)
    (hmax : ∀ y, a < y → y ∈ Ω) (f : B.Assignment) (hf : B.CompatibleOn Ω f) :
    ∃ g : B.Assignment, B.CompatibleOn (insert a Ω) g ∧
      (∀ x ∈ Ω, g x = f x) := by
…

theorem OAI.KLInvariance.MomentGraph.Sheaf.closedUnder_insert line 95

theorem OAI.KLInvariance.MomentGraph.Sheaf.extend_closedUnder line 106

Source documentation

A finite flabby graph sheaf extends from every set closed under its nonzero edges. This is the source's relative-flabbiness argument in full, not merely a restatement of flabbiness for ambient upper sets.

theorem extend_closedUnder [Finite V] (hb : B.Flabby) (live : Set E)
    (hdead : ∀ e, e ∉ live → Subsingleton (B.edge e))
    (Ω : Set V) (hΩ : B.ClosedUnder live Ω) (f : B.Assignment)
    (hf : B.CompatibleOn Ω f) :
    ∃ g : B.Assignment, B.IsGlobal g ∧ (∀ x ∈ Ω, g x = f x) := by
…

def OAI.KLInvariance.MomentGraph.Sheaf.sections line 161
Source documentation
The actual module of sections on a vertex set. Coordinates outside the set are harmless and ignored by all restriction maps.
```
def sections (Ω : Set V) : Submodule R B.Assignment where
…
```
def OAI.KLInvariance.MomentGraph.Sheaf.Generated line 175
Source documentation
Generation at a stalk by genuine global sections.
```
def Generated : Prop :=
…
```
abbrev OAI.KLInvariance.MomentGraph.Sheaf.Outgoing line 178
abbrev OAI.KLInvariance.MomentGraph.Sheaf.Boundary line 180
def OAI.KLInvariance.MomentGraph.Sheaf.stalkMap line 183
Source documentation
The lower-end stalk map on all upward edges.
```
def stalkMap (x : V) : B.vertex x →ₗ[R] B.Boundary x where
…
```
def OAI.KLInvariance.MomentGraph.Sheaf.boundaryMap line 189
Source documentation
Boundary values supplied by sections strictly above a vertex.
```
def boundaryMap (x : V) : B.sections (Set.Ioi x) →ₗ[R] B.Boundary x where
…
```
def OAI.KLInvariance.MomentGraph.Sheaf.boundaryImage line 194
theorem OAI.KLInvariance.MomentGraph.Sheaf.range_stalkMap_eq_boundaryImage line 199
Source documentation
The precise boundary-image identity in loc:decomposition. Generation supplies one inclusion and flabbiness supplies the other.
```
theorem range_stalkMap_eq_boundaryImage
    (hf : B.Flabby) (hg : B.Generated) (x : V) :
    LinearMap.range (B.stalkMap x) = B.boundaryImage x := by
…
```
def OAI.KLInvariance.MomentGraph.Sheaf.stalkCover line 230
Source documentation
A sheaf satisfying the two standard section properties gives an actual surjection of its stalk onto the boundary module.
```
def stalkCover (hf : B.Flabby) (hg : B.Generated) (x : V) :
    B.vertex x →ₗ[R] B.boundaryImage x :=
…
```
theorem OAI.KLInvariance.MomentGraph.Sheaf.stalkCover_surjective line 236