OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeLowerContractible.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Contractibility of nonempty descending lower neighborhoods of the relative height.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeNegativeBlock_contractible line 15
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePositiveBlock_contractible line 42
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeAllEligibleLower_contractible line 93

    Source documentation

    The lower-link argument uses no positivity assumption on invisible colors.

    theorem relativeAllEligibleLower_contractible (P:Deligne M)
    (hU:U⊆Set.range (Sum.inl:S→S⊕Unit)) (hf:(.inl f:S⊕Unit)∉U)
    (hxA:sourceCosetRepresentative M P∈artinParabolic M {f}ᶜ)
    (hne:Nonempty (RelativeAllEligibleLower M f U cutoff P)) :
    ContractibleSpace (OrderWeights (RelativeAllEligibleLower M f U cutoff P)) := by
…

    Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.sourceCosetRepresentative, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.RelativeAllEligibleLower, OAI.HarmonicArtin.OrderWeights