OAI/AlgebraicGeometry/CharacterVarieties/Foundation/MatrixExpressions.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.MatrixExpression.blockIndex line 13

   Source documentation

   Fixed coordinate identification for a rank sum. The choice is retained uniformly throughout the finite incidence presentation.

   def blockIndex {k : ℕ} (d : Fin k → ℕ) : Fin (∑ j, d j) ≃ ((j : Fin k) × Fin (d j)) :=
   …

2. def OAI.IntegralCharacterVarieties.MatrixExpression.blockUnit line 17

   Source documentation

   Direct-sum transport, with all summand indices retained.

   def blockUnit {k : ℕ} (d : Fin k → ℕ) (g : (j : Fin k) → (Matrix (Fin (d j)) (Fin (d j)) R)ˣ) :
       (Matrix (Fin (∑ j, d j)) (Fin (∑ j, d j)) R)ˣ where
   …

3. def OAI.IntegralCharacterVarieties.MatrixExpression.mapUnit line 39

   Source documentation

   Ring change on an GL transport.

   def mapUnit {S : Type*} [CommRing S] (φ : R →+* S) {n : ℕ}
       (g : (Matrix (Fin n) (Fin n) R)ˣ) : (Matrix (Fin n) (Fin n) S)ˣ :=
   …

4. lemma OAI.IntegralCharacterVarieties.MatrixExpression.mapUnit_val line 43
5. inductive OAI.IntegralCharacterVarieties.MatrixExpression.Term line 50

   Source documentation

   Concrete words used at seams, corners, coarsened swaps, split vertices and surface relations. A block is an direct sum, not an abstract map between unnamed quotient modules. All inverses are the preserved GL inverse variables.

   inductive Term : ℕ → Type _
     | generator (e : E) : Term (rank e)
     | constant {n : ℕ} (g : (Matrix (Fin n) (Fin n) R)ˣ) : Term n
     | mul {n : ℕ} (x y : Term n) : Term n
     | inv {n : ℕ} (x : Term n) : Term n
     | block {k : ℕ} (d : Fin k → ℕ) (x : (j : Fin k) → Term (d j)) : Term (∑ j, d j)
   
   variable {R E rank}

6. def OAI.IntegralCharacterVarieties.MatrixExpression.Term.eval line 59
7. def OAI.IntegralCharacterVarieties.MatrixExpression.Term.raw line 75

   Source documentation

   The polynomial matrix expression, before imposing any inverses or incidence conditions. The sign retains both orientations of every transport.

   def Term.raw : {n : ℕ} → Term R E rank n → Bool →
       Matrix (Fin n) (Fin n) (Polynomial R E (fun e => Fin (rank e)))
     | _, .generator e, b => variableMatrix R E (fun e => Fin (rank e)) e b
     | _, .constant h, b =>
       (if b then (↑h⁻¹ : Matrix _ _ R) else (h : Matrix _ _ R)).map MvPolynomial.C
     | _, .mul x y, b => if b then y.raw b*x.raw b else x.raw b*y.raw b
     | _, .inv x, b => x.raw (!b)
     | _, .block d x, b =>
       (Matrix.blockDiagonal' (fun j => (x j).raw b)).submatrix (blockIndex d) (blockIndex d)

   Mentions: OAI.IntegralCharacterVarieties.MatrixExpression.Term, OAI.IntegralCharacterVarieties.MatrixExpression.blockIndex

8. def OAI.IntegralCharacterVarieties.MatrixExpression.signed line 85
9. theorem OAI.IntegralCharacterVarieties.MatrixExpression.Term.raw_evaluation line 92

   Source documentation

   Polynomial expression evaluation is exactly the corresponding composition, inversion and direct sum of local-system transports.

   theorem Term.raw_evaluation {n : ℕ} (t : Term R E rank n)
       (g : (e : E) → (Matrix (Fin (rank e)) (Fin (rank e)) S)ˣ) (b : Bool) :
       (t.raw b).map (matrixEvaluation g).toRingHom=signed (t.eval (algebraMap R S) g) b := by
   …

   Mentions: OAI.IntegralCharacterVarieties.MatrixExpression.Term, OAI.IntegralCharacterVarieties.MatrixExpression.signed

10. structure OAI.IntegralCharacterVarieties.FlagCircuit.Data line 119

    Source documentation

    An incidence constraint compares transported flags with their named quotients. Constant grade zero imposes full equality (e.g. a surface relation). Coarsening the grade imposes the unchanged direct-sum block at an interchange.

    structure Data where
    …

11. abbrev OAI.IntegralCharacterVarieties.FlagCircuit.Data.Entry line 128
12. def OAI.IntegralCharacterVarieties.FlagCircuit.Data.difference line 130
13. def OAI.IntegralCharacterVarieties.FlagCircuit.Data.equation line 133
14. abbrev OAI.IntegralCharacterVarieties.FlagCircuit.Data.Coordinate line 136
15. def OAI.IntegralCharacterVarieties.FlagCircuit.Data.Holds line 141

    Source documentation

    Geometric meaning, including the grade identifications, not just ranks or underlying flag subspaces. It is meaningful over full integer rings as well.

    def Holds (g : (e : E) → (Matrix (Fin (rank e)) (Fin (rank e)) S)ˣ) : Prop :=
    …

16. abbrev OAI.IntegralCharacterVarieties.FlagCircuit.Data.Solution line 146
17. lemma OAI.IntegralCharacterVarieties.FlagCircuit.Data.equation_evaluation line 149
18. theorem OAI.IntegralCharacterVarieties.FlagCircuit.Data.holds_iff_equations line 167

    Source documentation

    These are precisely the finite polynomial equations for all identified-flag constraints. No event or wrap relation is omitted.

    theorem holds_iff_equations (g : (e : E) → (Matrix (Fin (rank e)) (Fin (rank e)) S)ˣ) :
        D.Holds g ↔ ∀ z, matrixEvaluation g (D.equation z)=0 := by
    …

19. def OAI.IntegralCharacterVarieties.FlagCircuit.Data.pointsEquiv line 180

    Source documentation

    The finite algebra representing the split-frame incidence scheme. This is not an abstract affine-bundle interface: all entries and all relations are in the explicit quotient algebra, and its ring-valued points are identified.

    def pointsEquiv : D.Solution S ≃ (D.Coordinate →ₐ[R] S) :=
    …

20. instance OAI.IntegralCharacterVarieties.FlagCircuit.Data.finiteType line 184
21. instance OAI.IntegralCharacterVarieties.FlagCircuit.Data.finiteEntry line 185