OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeTiedDescent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of descending neighborhoods across equal-height inclusions.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeTie_active_common line 12
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeTie_common_from_larger line 33
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeTie_common_from_smaller line 55
  4. theorem OAI.HarmonicArtin.ParabolicIntersections.relative_localDescent line 71

    Source documentation

    The local hypotheses used by path lowering are verified for the actual relative coset poset and the actual pointed-family height.

    theorem relative_localDescent
    (hYU:∀i∈Y,(.inl i:S⊕Unit)∈U)
    (hU:U⊆Set.range (Sum.inl:S→S⊕Unit)) (hf:(.inl f:S⊕Unit)∉U)
    (hx:x∈artinParabolic M {f}ᶜ) :
    LocalDescent (relativeAdjacent M (Y:=Y) (x:=x))
…

    Mentions: OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.LocalDescent, OAI.HarmonicArtin.ParabolicIntersections.relativeAdjacent

  5. theorem OAI.HarmonicArtin.ParabolicIntersections.relative_minimum_path line 94