Documentation

LeanPool.BrillNoetherGraphs.LowGenus.GenusFiveRow15

The Atanasov--Ranganathan construction on row 15 #

Row 15 is the eight-cycle with opposite chords. Put one chip on each even vertex 0,2,4,6. The chip-free core vertices form the two edges 1--5 and 3--7; together with their four incident chip vertices, each is configuration 3 of Atanasov--Ranganathan, Proposition 5.1.

The calculation itself is core generic and lives in LowGenus/ConfigurationThree.lean. All this file does is name the row's lookup tables and check the incidence facts that file asks for.

source
def AtanasovRanganathan.GenusFiveRow15.partner :
Fin 8 → Fin 8

The other chip-free centre in the same configuration-3 component.

Equations
Instances For
    source
    def AtanasovRanganathan.GenusFiveRow15.firstArm :
    Fin 8 → Fin 12

    The first arm from each chip-free centre to a chip vertex.

    Equations
    Instances For
      source
      def AtanasovRanganathan.GenusFiveRow15.secondArm :
      Fin 8 → Fin 12

      The second arm from each chip-free centre to a chip vertex.

      Equations
      Instances For
        source
        def AtanasovRanganathan.GenusFiveRow15.firstChip :
        Fin 8 → Fin 8

        The chip at the far end of the first arm.

        Equations
        Instances For
          source
          def AtanasovRanganathan.GenusFiveRow15.secondChip :
          Fin 8 → Fin 8

          The chip at the far end of the second arm.

          Equations
          Instances For
            source
            def AtanasovRanganathan.GenusFiveRow15.middleEdge :
            Fin 8 → Fin 12

            The edge joining the two chip-free centres.

            Equations
            Instances For
              source
              def AtanasovRanganathan.GenusFiveRow15.isCenter :
              Fin 8 → Bool

              The chip-free core vertices, as a decidable table.

              Equations
              Instances For
                source
                def AtanasovRanganathan.GenusFiveRow15.row15Config :
                ConfigurationThree.ConfigThree 8 12

                Row 15 read as a pair of AR configuration-3 pictures.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem AtanasovRanganathan.GenusFiveRow15.row15_closedConstruction :
                  Configurations.ClosedSubdivisionDharConstruction GenusFiveCoreAtlas.row15Core row15_closedConstruction._proof_1

                  AR configuration 3 on row 15, valid simultaneously on the open cell and every nonloopy forest face.