ConnectedSupport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Connected support of transported indecomposable projectives

This proves the support-cut form of the connectedness assertion in Proposition 2.7 of paper 082-03. The input is the dimension of the actual endomorphism cohomology, rather than an assumed connectedness property.

def OAI.HarmonicArtin.ParabolicIntersections.blockProjector line 27
theorem OAI.HarmonicArtin.ParabolicIntersections.blockProjector_diagonal line 32
theorem OAI.HarmonicArtin.ParabolicIntersections.no_proper_block line 53
Source documentation
A minimal complex with at most one-dimensional degree-zero endomorphism cohomology cannot have two nonempty differential blocks.
```
theorem no_proper_block (E : BasedComplex Q (K := K) I) (hE : E.IsMinimal Q)
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.differential_same_or_arrow line 72
Source documentation
Nonzero minimal differential entries either stay at one color or follow an arrow of the quiver. This includes the token entries between successive layers.
```
theorem differential_same_or_arrow (E : BasedComplex Q (K := K) I)
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.support_meets_boundary line 100
Source documentation
If the support meets both a color set and its complement, it must meet the exterior boundary of that set. This is the exact support fact needed to find a boundary level below an isolated null layer.
```
theorem support_meets_boundary (E : BasedComplex Q (K := K) I) (hE : E.IsMinimal Q)
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.fusionOrbit_support_meets_boundary line 131
Source documentation
The preceding support statement applies unconditionally to the minimal representative of every transported projective in the fusion packet action.
```
theorem fusionOrbit_support_meets_boundary (w : List (W × Bool)) (s : W)
    (L : FusionLabel m) (U : Set (FusionVertex (V := W) m))
…
```
Mentions: OAI.HarmonicArtin.FusionLabel, OAI.HarmonicArtin.FusionVertex