RelativeTies.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Visible and invisible sets along tied comparable vertices, §6.5 of paper 082-03.

lemma OAI.HarmonicArtin.ParabolicIntersections.relativeSign_eq_zero_iff line 15
lemma OAI.HarmonicArtin.ParabolicIntersections.relativeHeight_eq_profiles line 20
lemma OAI.HarmonicArtin.ParabolicIntersections.relativeHeight_eq_masks line 27
def OAI.HarmonicArtin.ParabolicIntersections.relativeInvisible line 35
Source documentation
Absence of recorded incidence, restricted to the group currently acting.
```
def relativeInvisible (Y : Set S) (P : Deligne M) : Set S :=
…
```
Mentions: OAI.HarmonicArtin.Deligne
def OAI.HarmonicArtin.ParabolicIntersections.relativeVisible line 38
lemma OAI.HarmonicArtin.ParabolicIntersections.relativeInvisible_eq_of_height_eq line 41
lemma OAI.HarmonicArtin.ParabolicIntersections.tied_new_color_invisible line 58
Source documentation
Each new closed color at a tied upper vertex has no recorded incidence.
```
lemma tied_new_color_invisible (Y : Set S) {P R : Deligne M}
    (hR : R.val.1 ⊆ Y)
    (he : relativeHeight M f U cutoff P = relativeHeight M f U cutoff R)
    (i : S) (hi : i ∈ R.val.1) (hn : i ∉ P.val.1) :
    i ∈ relativeInvisible M f cutoff Y R := by
…
```
Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.ParabolicIntersections.relativeHeight, OAI.HarmonicArtin.ParabolicIntersections.relativeInvisible
lemma OAI.HarmonicArtin.ParabolicIntersections.relativeVisible_eq_of_tie line 82
Source documentation
The visible closed set is constant across a tied comparability edge.
```
lemma relativeVisible_eq_of_tie (Y : Set S) {P R : Deligne M} (hPR : P ≤ R)
    (hR : R.val.1 ⊆ Y)
    (he : relativeHeight M f U cutoff P = relativeHeight M f U cutoff R) :
    relativeVisible M f cutoff Y P = relativeVisible M f cutoff Y R := by
…
```
Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.ParabolicIntersections.relativeHeight, OAI.HarmonicArtin.ParabolicIntersections.relativeVisible
lemma OAI.HarmonicArtin.ParabolicIntersections.relativeVisible_positive line 98
Source documentation
A visible closed color is positive at some recorded level.
```
lemma relativeVisible_positive (Y : Set S) (P : Deligne M) (hP : P.val.1 ⊆ Y)
    (i : S) (hi : i ∈ relativeVisible M f cutoff Y P) :
    ∃ k, 0 < pointedProfile M f P cutoff k (.inl i) := by
…
```
Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.ParabolicIntersections.relativeVisible, OAI.HarmonicArtin.ParabolicIntersections.pointedProfile
lemma OAI.HarmonicArtin.ParabolicIntersections.relativeVisible_nonadjacent line 114
Source documentation
Visible closed colors cannot be adjacent to any invisible color.
```
lemma relativeVisible_nonadjacent (Y : Set S) (P : Deligne M) (hP : P.val.1 ⊆ Y)
    (i j : S) (hi : i ∈ relativeInvisible M f cutoff Y P)
    (hj : j ∈ relativeVisible M f cutoff Y P) :
    ¬framedCartan M (.inl i) (.inl j) < 0 := by
…
```
Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.ParabolicIntersections.relativeInvisible, OAI.HarmonicArtin.ParabolicIntersections.relativeVisible, OAI.HarmonicArtin.framedCartan