DeterminantActionWeights.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The differentiated lifted action preserves the actual fiber grading

This is the last interface in the manuscript's Proposition prop:lift. Once a normalized frame lift supplies the five coordinate coefficient laws, this file proves equivariance of its entire algebra homomorphism and hence preservation of every actual fiber-weight submodule after differentiation. The five identities are consumed as construction outputs, not as additional assumptions of the principal target; existence of the lifted action is separate.

theorem OAI.StableCoordinate.DeterminantActionWeights.generator_adjoin_eq_top line 28
Source documentation
The actual five quotient generators generate the determinant algebra.
```
theorem generator_adjoin_eq_top :
    Algebra.adjoin k (Set.range (generator k)) = ⊤ := by
…
```

theorem OAI.StableCoordinate.DeterminantActionWeights.commutesWithWeights_of_generator_coefficients line 38

Source documentation

Coordinatewise coefficient weights imply full equivariance of the actual polynomial algebra homomorphism on the determinant quotient.

theorem commutesWithWeights_of_generator_coefficients
    (α : C k →ₐ[k] Polynomial (C k))
    (hα : ∀ (i : Fin 5) (m : ℕ),
      DeterminantWeights.fiberCoaction k ((α (generator k i)).coeff m) =
        AddMonoidAlgebra.single (Obstruction.fiberWeight i)
          ((α (generator k i)).coeff m)) :
    CommutesWithWeights (DeterminantWeights.fiberCoaction k) α :=
…

Mentions: OAI.StableCoordinate.DeterminantWeights.fiberCoaction, OAI.StableCoordinate.Obstruction.fiberWeight

theorem OAI.StableCoordinate.DeterminantActionWeights.coefficient_preserves_fiberPiece line 51

Source documentation

Every coefficient of the lifted polynomial family preserves every piece of the constructed fiber grading, not only the five generator weights.

theorem coefficient_preserves_fiberPiece
    (α : C k →ₐ[k] Polynomial (C k))
    (hα : ∀ (i : Fin 5) (m : ℕ),
      DeterminantWeights.fiberCoaction k ((α (generator k i)).coeff m) =
        AddMonoidAlgebra.single (Obstruction.fiberWeight i)
          ((α (generator k i)).coeff m))
    {n : ℤ} {q : C k} (hq : q ∈ Obstruction.fiberPiece k n) (m : ℕ) :
    (α q).coeff m ∈ Obstruction.fiberPiece k n := by
…

Mentions: OAI.StableCoordinate.DeterminantWeights.fiberCoaction, OAI.StableCoordinate.Obstruction.fiberWeight, OAI.StableCoordinate.Obstruction.fiberPiece

theorem OAI.StableCoordinate.DeterminantActionWeights.derivation_preserves_fiberPiece line 66

Source documentation

Differentiation of the actual lifted polynomial family preserves the fiber grading required in the rigidity theorem.

theorem derivation_preserves_fiberPiece
    (α : C k →ₐ[k] Polynomial (C k))
    (hα : ∀ (i : Fin 5) (m : ℕ),
      DeterminantWeights.fiberCoaction k ((α (generator k i)).coeff m) =
        AddMonoidAlgebra.single (Obstruction.fiberWeight i)
          ((α (generator k i)).coeff m))
    (D : Derivation k (C k) (C k)) (hD : ∀ q, D q = (α q).coeff 1) :
    ∀ (n : ℤ) (q : C k), q ∈ Obstruction.fiberPiece k n →
      D q ∈ Obstruction.fiberPiece k n := by
…

Mentions: OAI.StableCoordinate.DeterminantWeights.fiberCoaction, OAI.StableCoordinate.Obstruction.fiberWeight, OAI.StableCoordinate.Obstruction.fiberPiece

theorem OAI.StableCoordinate.DeterminantActionWeights.generator_laws_of_five_coefficients line 81

Source documentation

Read the coordinate coefficient laws in the manuscript's names and order. This is the interface supplied by the normalized-frame scaling calculation.

theorem generator_laws_of_five_coefficients
    (α : C k →ₐ[k] Polynomial (C k))
    (ha : ∀ m, DeterminantWeights.fiberCoaction k ((α (a k)).coeff m) =
      AddMonoidAlgebra.single 1 ((α (a k)).coeff m))
    (hd : ∀ m, DeterminantWeights.fiberCoaction k ((α (d k)).coeff m) =
      AddMonoidAlgebra.single 1 ((α (d k)).coeff m))
    (hb : ∀ m, DeterminantWeights.fiberCoaction k ((α (b k)).coeff m) =
      AddMonoidAlgebra.single (-1) ((α (b k)).coeff m))
    (hc : ∀ m, DeterminantWeights.fiberCoaction k ((α (c k)).coeff m) =
      AddMonoidAlgebra.single (-1) ((α (c k)).coeff m))
    (hu : ∀ m, DeterminantWeights.fiberCoaction k ((α (u k)).coeff m) =
      AddMonoidAlgebra.single 0 ((α (u k)).coeff m)) :
…

Mentions: OAI.StableCoordinate.DeterminantWeights.fiberCoaction