PointedNullObstruction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The relative null obstruction for actual group elements avoiding the frame.

theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_null_obstruction line 20

Source documentation

Proposition 5.1 of 082-03, expressed using the pointed group orbit. The avoidance hypothesis is automatic in the relative enlarged diagram.

theorem pointed_null_obstruction (I J : Set S) (hI : I.Nonempty) (hf : f ∉ I)
    (hJI : J ⊆ I) (hJ : IsSpherical M J) (x : Artin M)
    (hx : x ∈ artinParabolic M {f}ᶜ) (q : ℤ)
    (c : S ⊕ Unit → ℝ) (hc : ∀ v, 0 ≤ c v)
    (hcSupp : ∀ v, v ∉ Sum.inl '' I → c v = 0)
    (hcPos : ∀ v, v ∈ Sum.inl '' I → 0 < c v)
    (hcNull : ∀ v, v ∈ Sum.inl '' I → (framedCartan M *ᵥ c) v = 0)
    (hE : ∀ L, ClassCapOn Q (pointedFamily M f x L)
      (closedNeighborhood Q (fusionColorRegion m (Sum.inl '' I)) \
        fusionColorRegion m (Sum.inl '' J)) q)
    (hdata : ∀ v, (v ∈ Sum.inl '' I ∧ v ∉ Sum.inl '' J) ∨
      (v ∉ Sum.inl '' I ∧ ∃ u ∈ Sum.inl '' I, framedCartan M v u < 0) →
…

Mentions: OAI.HarmonicArtin.IsSpherical, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.framedCartan, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily, OAI.HarmonicArtin.fusionColorRegion