OAI/Topology/ArtinGroups/ParabolicIntersections/SphericalReduction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ParabolicIntersections.pointed_testUpper_exists line 16
2. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveSupport_ambient_mem line 33

   Source documentation

   Support in a subtype becomes the corresponding ambient standard subgroup.

   lemma positiveSupport_ambient_mem (Y : Set S) (J : Set Y)
       (a : PositiveArtin (restrictedMatrix M Y))
       (ha : positiveSupport _ a ⊆ J) :
       restrictedArtinHom M Y (positiveToArtin _ a) ∈
         artinParabolic M (Subtype.val '' J) := by
   …

   Mentions: OAI.HarmonicArtin.PositiveArtin, OAI.HarmonicArtin.ParabolicIntersections.positiveSupport, OAI.HarmonicArtin.restrictedArtinHom, OAI.HarmonicArtin.positiveToArtin, OAI.HarmonicArtin.artinParabolic

3. theorem OAI.HarmonicArtin.ParabolicIntersections.spherical_reduction line 48

   Source documentation

   The spherical case of the local rank reduction. The positive-height argument, including its proper-support and containment steps, is proved here. Only the indicated published categorical and monoid inputs remain.

   theorem spherical_reduction (Y : Set S) (hY : IsSpherical M Y)
       (hf : f ∉ Y) (hGcd : PublishedFoldingGcd M Y hY)
       (hmesh : MeshNilpotent Q (fusionColorRegion m (Sum.inl '' Y)))
       (hAcyclic : PublishedAcyclicTwist Q)
       (x : Artin M) (hx : x ∈ artinParabolic M {f}ᶜ) :
       ReductionAt M (pointedInitial M f) Y x := by
   …

   Mentions: OAI.HarmonicArtin.IsSpherical, OAI.HarmonicArtin.ParabolicIntersections.PublishedFoldingGcd, OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent, OAI.HarmonicArtin.fusionColorRegion, OAI.HarmonicArtin.ParabolicIntersections.PublishedAcyclicTwist, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.ReductionAt, OAI.HarmonicArtin.ParabolicIntersections.pointedInitial