OAI/AlgebraicGeometry/CharacterVarieties/Foundation/MatrixPresentation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Entry line 17

    Source documentation

    Every transport and every chosen split frame has its own occurrence index. The sign distinguishes its matrix from its inverse, not a second occurrence.

    abbrev Entry := (e : E) × Bool × (ι e × ι e)
  2. abbrev OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Polynomial line 18
  3. def OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.variableMatrix line 20
  4. inductive OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Relation line 26

    Source documentation

    The inverse equations are imposed in both directions over the full ring. Every incidence equation is included individually, even for repeated sides.

    inductive Relation : Polynomial R E ι → Prop
  | inverse (e : E) (b : Bool) (i j : ι e) : Relation
      ((variableMatrix R E ι e b * variableMatrix R E ι e (!b)) i j -
        (1 : Matrix (ι e) (ι e) (Polynomial R E ι)) i j)
  | incidence (j : J) : Relation (equation j)

    Mentions: OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Polynomial, OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.variableMatrix

  5. def OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.relationIdeal line 32
  6. abbrev OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Coordinate line 35
  7. def OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.universalMatrix line 39
  8. lemma OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.relation_zero line 42
  9. lemma OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.universal_inverse line 46
  10. def OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.universalUnit line 59

    Source documentation

    These are general linear transports, not only matrices with nonvanishing determinant at complex points.

    def universalUnit (e : E) : (Matrix (ι e) (ι e) (Coordinate R E ι equation))ˣ where
…

    Mentions: OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Coordinate

  11. def OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.matrixEvaluation line 68

    Source documentation

    Evaluation retains every occurrence's forward and backward transport.

    def matrixEvaluation (g : (e : E) → (Matrix (ι e) (ι e) S)ˣ) :
    Polynomial R E ι →ₐ[R] S :=
…

    Mentions: OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Polynomial

  12. lemma OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.matrixEvaluation_variable line 73
  13. abbrev OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Solution line 81

    Source documentation

    A split-frame solution of the finite incidence equations over S.

    abbrev Solution (S : Type*) [CommRing S] [Algebra R S] :=
…
  14. lemma OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.ideal_le_ker line 84
  15. def OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.solutionToPoint line 106
  16. lemma OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.solutionToPoint_mk line 109
  17. def OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.pointMatrices line 114

    Source documentation

    Reading the universal transports along an ring-valued point.

    def pointMatrices (φ : Coordinate R E ι equation →ₐ[R] S) (e : E) :
    (Matrix (ι e) (ι e) S)ˣ :=
…

    Mentions: OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Coordinate

  18. lemma OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.pointMatrices_val line 118
  19. lemma OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.pointMatrices_inv line 122
  20. lemma OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.point_evaluation line 126
  21. def OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.pointToSolution line 134
  22. def OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.pointsEquiv line 142

    Source documentation

    Exact representability over arbitrary coefficient rings, including the full ring of integers. No reduction, localization or rank condition is dropped.

    def pointsEquiv : Solution equation S ≃ (Coordinate R E ι equation →ₐ[R] S) where
…

    Mentions: OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Solution, OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Coordinate

  23. instance OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.finiteEntry line 160

    Source documentation

    There are finitely many matrix entries when the diagram is finite.

    instance finiteEntry [Finite E] [∀ e, Finite (ι e)] : Finite (Entry E ι) := inferInstance

    Mentions: OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.Entry

  24. instance OAI.IntegralCharacterVarieties.FiniteMatrixPresentation.finiteType line 162