OAI/Topology/ArtinGroups/ParabolicIntersections/SphericalMesh.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Discharging the finite spherical mesh input for the actual fusion quiver.

  1. def OAI.HarmonicArtin.ParabolicIntersections.sphericalRegionEquiv line 15
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.sphericalRegionEquiv_val line 21
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.sphericalRegionEquiv_symm_val line 25
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.spherical_mesh_simple line 29
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.fusion_mesh_arrow_exists line 56
  6. theorem OAI.HarmonicArtin.ParabolicIntersections.spherical_mesh_cartan line 69
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.spherical_mesh_nilpotent line 106

    Source documentation

    The finite-Dynkin mesh nilpotence input for every spherical set of colors, proved for the precise ambient fusion-quiver relations.

    theorem spherical_mesh_nilpotent (Y : Set S) (hY : IsSpherical M Y) : MeshNilpotent Q (U Y) := by
…

    Mentions: OAI.HarmonicArtin.IsSpherical, OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent