RelativeMinimumContainment.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Confinement of the actual categorical stabilizer from a harmonic minimum.

def OAI.HarmonicArtin.ParabolicIntersections.RelativeMinimum line 12
def OAI.HarmonicArtin.ParabolicIntersections.relativeContainingType line 15
lemma OAI.HarmonicArtin.ParabolicIntersections.relative_type_subset_containing line 18
lemma OAI.HarmonicArtin.ParabolicIntersections.relative_containing_subset line 25
theorem OAI.HarmonicArtin.ParabolicIntersections.relative_minimum_exists line 29
lemma OAI.HarmonicArtin.ParabolicIntersections.relative_minimum_path_confined line 36
theorem OAI.HarmonicArtin.ParabolicIntersections.relative_minimum_stabilizer_containment line 65
Source documentation
Proposition 6.9: the stabilizer lies in the conjugate standard subgroup specified by the visible and invisible colors at a minimum.
```
theorem relative_minimum_stabilizer_containment
    (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}ᶜ) (P:RelativeVertex M Y x)
    (hP:RelativeMinimum M f U cutoff P)
    (a:Artin M) (ha:a∈artinParabolic M Y)
    (hfix:pointedFamily M f (a*x)=pointedFamily M f x) :
    a∈conjugate (sourceCosetRepresentative M P.val*x⁻¹)⁻¹
      (artinParabolic M (relativeContainingType M f cutoff Y P.val)) := by
…
```
Mentions: OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.RelativeVertex, OAI.HarmonicArtin.ParabolicIntersections.RelativeMinimum, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily, OAI.HarmonicArtin.sourceCosetRepresentative, OAI.HarmonicArtin.ParabolicIntersections.relativeContainingType