Documentation

DerivedAlgGeo.AlgebraicGeometry.Numerical.Stability.SurfaceChargeNumerical

Surface charge coordinates from numerical variety data #

This is the numerical adapter for ChargeCoordinates. The pure charge polynomial lives in SurfaceCharge.lean; this file supplies both the untwisted view and the general BField-twisted view from NumericalVarietyData and Polarization.

source
noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.rankHom {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) :
N →+ ℝ

The real rank coordinate induced by a numerical surface presentation.

Equations
Instances For
    source
    noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.degreeHom {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) :
    N →+ ℝ

    The degree coordinate induced by a numerical surface presentation and a polarisation.

    Equations
    Instances For
      source
      noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.chTwoHom {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) :
      N →+ ℝ

      The ∫ ch₂ coordinate induced by a numerical surface presentation.

      Equations
      Instances For
        source
        noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.degreeBHom {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (B : AlgebraicGeometry.Numerical.BField V.ring) :
        N →+ ℝ

        The twisted degree ∫ ch₁^B · H, bundled additively.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.chTwoBHom {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (B : AlgebraicGeometry.Numerical.BField V.ring) :
          N →+ ℝ

          The twisted top component ∫ ch₂^B, bundled additively.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.rankHom_apply {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (E : N) :
            (rankHom V) E = ↑(V.rank E)

            This is the coercion step that exposes the integer rank to the charge polynomial.

            source
            @[simp]
            theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.degreeHom_apply {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (E : N) :
            (degreeHom V P) E = ↑(AlgebraicGeometry.Numerical.degH V P E)

            This keeps consumers independent of the implementation of the bundled degree map.

            source
            @[simp]
            theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.chTwoHom_apply {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (E : N) :
            (chTwoHom V) E = ↑(V.ring.degree (V.chComp E 2))

            Applying chTwoHom is integration of the codimension-two Chern character.

            source
            @[simp]
            theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.degreeBHom_apply {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (B : AlgebraicGeometry.Numerical.BField V.ring) (E : N) :
            (degreeBHom V P B) E = ↑(V.ring.degree (AlgebraicGeometry.Numerical.chBComp V B E 1 * P.cls))

            Evaluation of the bundled twisted H-degree.

            source
            @[simp]
            theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.chTwoBHom_apply {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (B : AlgebraicGeometry.Numerical.BField V.ring) (E : N) :
            (chTwoBHom V B) E = ↑(V.ring.degree (AlgebraicGeometry.Numerical.chBComp V B E 2))

            Evaluation of the bundled integrated twisted second component.

            The derived view of a numerical presentation #

            source
            noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalData {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) :
            ChargeCoordinates N

            The surface charge coordinates extracted from NumericalVarietyData and a polarisation.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalDataB {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (B : AlgebraicGeometry.Numerical.BField V.ring) :
              ChargeCoordinates N

              Surface charge coordinates extracted after twisting by an arbitrary numerical B-field.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalData_rank {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (E : N) :
                (ofNumericalData V P).rank E = ↑(V.rank E)

                The derived-view rank coordinate agrees with the variety presentation.

                source
                @[simp]
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalData_degree {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (E : N) :
                (ofNumericalData V P).degree E = ↑(AlgebraicGeometry.Numerical.degH V P E)

                The derived-view degree coordinate agrees with degH.

                source
                @[simp]
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalData_chTwo {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (E : N) :
                (ofNumericalData V P).chTwo E = ↑(V.ring.degree (V.chComp E 2))

                The derived-view top Chern-character coordinate is the integrated ch₂.

                source
                @[simp]
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalData_hyperplaneSquare {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) :
                (ofNumericalData V P).hyperplaneSquare = ↑(V.ring.degree (P.cls ^ 2))

                The untwisted view retains the polarisation square from the numerical ring.

                source
                @[simp]
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalDataB_rank {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (B : AlgebraicGeometry.Numerical.BField V.ring) (E : N) :
                (ofNumericalDataB V P B).rank E = ↑(V.rank E)

                A B-field twist leaves the rank component unchanged.

                source
                @[simp]
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalDataB_degree {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (B : AlgebraicGeometry.Numerical.BField V.ring) (E : N) :
                (ofNumericalDataB V P B).degree E = ↑(V.ring.degree (AlgebraicGeometry.Numerical.chBComp V B E 1 * P.cls))

                The general B-field view exposes ∫H ch₁^B.

                source
                @[simp]
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalDataB_chTwo {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (B : AlgebraicGeometry.Numerical.BField V.ring) (E : N) :
                (ofNumericalDataB V P B).chTwo E = ↑(V.ring.degree (AlgebraicGeometry.Numerical.chBComp V B E 2))

                The general B-field view exposes ∫ch₂^B.

                source
                @[simp]
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalDataB_hyperplaneSquare {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (B : AlgebraicGeometry.Numerical.BField V.ring) :
                (ofNumericalDataB V P B).hyperplaneSquare = ↑(V.ring.degree (P.cls ^ 2))

                The general B-field view retains the chosen polarisation square.

                Compatibility of B and βH notation #

                source
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalDataB_along_degree {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (β : ℚ) (E : N) :
                (ofNumericalDataB V P (AlgebraicGeometry.Numerical.BField.along P β)).degree E = ((ofNumericalData V P).twistByScalar ↑β).degree E

                At B = βH, the general twisted degree is the scalar-twist formula.

                source
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.ofNumericalDataB_along_chTwo {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (β : ℚ) (E : N) :
                (ofNumericalDataB V P (AlgebraicGeometry.Numerical.BField.along P β)).chTwo E = ((ofNumericalData V P).twistByScalar ↑β).chTwo E

                At B = βH, the general twisted second component is the scalar-twist formula.

                source
                theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.centralCharge_ofNumericalDataB_along_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : AlgebraicGeometry.Numerical.NumericalVarietyData 2 A N) (P : AlgebraicGeometry.Numerical.Polarization V.ring) (a : ℝ) (β : ℚ) (E : N) :
                ((ofNumericalDataB V P (AlgebraicGeometry.Numerical.BField.along P β)).centralCharge a) E = (((ofNumericalData V P).twistByScalar ↑β).centralCharge a) E

                Switching between the general notation ch^B and the rank-one notation ch^(βH) does not change the central charge.