OAI/AlgebraicGeometry/CharacterVarieties/Foundation/ExactSequences.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart line 17

   Source documentation

   Concrete frame equations defining one splitting chart. The domains are free modules in the matrix instantiation below; no affine-bundle hypothesis.

   structure Chart (f : U →ₗ[R] V) (g : V →ₗ[R] Q) where
   …

2. def OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.left line 28
3. def OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.sectionMap line 30
4. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.g_t line 32
5. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.g_eq line 35
6. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.g_section line 38
7. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.t_inl line 42
8. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.t_inr line 45
9. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.left_f line 48
10. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.left_section line 52
11. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.decompose line 56
12. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.f_left_of_g_zero line 60
13. abbrev OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.RightInverse line 63
14. def OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.fromParameter line 65
15. def OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.toParameter line 69
16. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.to_from line 72
17. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.from_to line 77
18. def OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.parameterEquiv line 86

    Source documentation

    All solutions of GS=1 on this matrix chart, with no missing rank-open constraints on S, form exactly the free affine parameter space.

    def parameterEquiv : (Q →ₗ[R] U) ≃ RightInverse (g := g) where
    …

    Mentions: OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.RightInverse

19. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart.overlap_formula line 92
20. theorem OAI.IntegralCharacterVarieties.ExactSequenceChart.chart_nonempty line 102

    Source documentation

    Every short exact sequence with projective (in particular free) quotient lies in one of the concrete charts. This includes integral lower solutions, with no inversion of a nonunit of the full integer ring.

    theorem chart_nonempty [Module.Projective R Q]
        (f : U →ₗ[R] V) (g : V →ₗ[R] Q)
        (hf : Function.Injective f) (hg : Function.Surjective g)
        (hex : LinearMap.ker g = LinearMap.range f) : Nonempty (Chart f g) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart

21. def OAI.IntegralCharacterVarieties.ExactSequenceChart.matrixChart line 151
22. structure OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData line 180

    Source documentation

    The five split-sequence identities, proved from each principal matrix chart below. They are preserved under arbitrary base change.

    structure MatrixSplitData (R : Type*) [CommRing R] (υ ν κ : Type*)
        [Fintype υ] [Fintype ν] [Fintype κ] [DecidableEq υ] [DecidableEq ν] [DecidableEq κ] where
    …

23. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.ofChart line 195

    Source documentation

    Taking coordinates of the explicitly constructed linear chart.

    def ofChart {f : (υ → R) →ₗ[R] (ν → R)} {g : (ν → R) →ₗ[R] (κ → R)}
        (C : Chart f g) : MatrixSplitData R υ ν κ where
    …

    Mentions: OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart, OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData

24. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.reconstruct line 235

    Source documentation

    Affine reconstruction and its coordinate readout.

    def reconstruct (h : Matrix υ κ R) : Matrix ν κ R := D.s + D.f * h

25. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.read line 237
26. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.difference line 239
27. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.read_reconstruct line 241
28. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.reconstruct_read line 245
29. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.difference_reconstruct line 254
30. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.map line 260
31. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.reconstruct_map line 282
32. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.read_map line 286
33. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.difference_map line 290
34. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.map_map line 295
35. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.map_algHom line 300
36. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.reconstruct_algHom line 307
37. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.read_algHom line 314
38. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.difference_algHom line 321
39. abbrev OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.AmbientPolynomial line 338
40. abbrev OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.FreePolynomial line 339
41. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.ambientVariables line 341
42. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.freeVariables line 344
43. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.relation line 347
44. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.relationIdeal line 350
45. abbrev OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.CoordinateRing line 353
46. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.coordinates line 355
47. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.coordinates_difference line 358
48. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.coordinates_solution line 368
49. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.reconstructionPolynomials line 372
50. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.polynomialToFree line 375
51. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.polynomialToFree_variable line 379
52. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.polynomialToFree_variables line 383
53. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.polynomialToFree_relation line 389
54. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.relationIdeal_le_ker line 399
55. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.toFree line 405

    Source documentation

    The map out of the algebra defined by all entries of GS−I.

    def toFree : D.CoordinateRing →ₐ[R] FreePolynomial (R := R) (υ := υ) (κ := κ) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.FreePolynomial

56. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.toFree_coordinate line 409
57. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.toFree_coordinates line 413
58. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.fromFree line 418
59. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.fromFree_variable line 421
60. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.fromFree_variables line 426
61. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.toFree_comp_fromFree line 432
62. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.fromFree_reconstruction line 445
63. lemma OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.fromFree_comp_toFree line 454
64. def OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.coordinateAlgEquiv line 463

    Source documentation

    The scheme of all right inverses, on each explicit splitting chart, is literally affine space over its base. This is a coefficient-algebra isomorphism, not merely a point-level or generic-fiber parametrization.

    def coordinateAlgEquiv : D.CoordinateRing ≃ₐ[R] FreePolynomial (R := R) (υ := υ) (κ := κ) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.FreePolynomial

65. theorem OAI.IntegralCharacterVarieties.ExactSequenceChart.exists_principal_chart line 474

    Source documentation

    The principal determinant charts exhaust all short exact sequences on these named free modules, over the full coefficient ring, not just a field.

    theorem exists_principal_chart
        (F : Matrix (υ ⊕ κ) υ R) (G : Matrix κ (υ ⊕ κ) R)
        (hf : Function.Injective (Matrix.toLin' F))
        (hg : Function.Surjective (Matrix.toLin' G))
        (hex : LinearMap.ker (Matrix.toLin' G) = LinearMap.range (Matrix.toLin' F)) :
        ∃ J : Matrix (υ ⊕ κ) κ R,
          IsUnit (Matrix.fromCols F J).det ∧ IsUnit (G * J).det := by
    …

66. def OAI.IntegralCharacterVarieties.ExactSequenceChart.chartDenominator line 493

    Source documentation

    The denominator defining one principal open.

    def chartDenominator (F : Matrix (υ ⊕ κ) υ R) (G : Matrix κ (υ ⊕ κ) R)
        (J : Matrix (υ ⊕ κ) κ R) : R := (Matrix.fromCols F J).det * (G * J).det

67. def OAI.IntegralCharacterVarieties.ExactSequenceChart.localizedMatrixChart line 497

    Source documentation

    Universal split coefficients over the principal open D(det[F,J]det(GJ)). The only equation required on the base matrices is GF=0.

    def localizedMatrixChart (F : Matrix (υ ⊕ κ) υ R) (G : Matrix κ (υ ⊕ κ) R)
        (J : Matrix (υ ⊕ κ) κ R) (hgf : G * F = 0) :
        Chart (Matrix.toLin' (F.map (algebraMap R (Localization.Away (chartDenominator F G J)))))
          (Matrix.toLin' (G.map (algebraMap R (Localization.Away (chartDenominator F G J))))) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.ExactSequenceChart.Chart, OAI.IntegralCharacterVarieties.ExactSequenceChart.chartDenominator

68. theorem OAI.IntegralCharacterVarieties.ExactSequenceChart.exact_sequence_chart_trivialization line 525

    Source documentation

    Exhaustive principal-open affine-space charts for extension lifts. The equation defining the lift algebra is GS=I, with no equations discarded.

    theorem exact_sequence_chart_trivialization
        (F : Matrix (υ ⊕ κ) υ R) (G : Matrix κ (υ ⊕ κ) R)
        (hgf : G * F = 0)
        (hf : Function.Injective (Matrix.toLin' F))
        (hg : Function.Surjective (Matrix.toLin' G))
        (hex : LinearMap.ker (Matrix.toLin' G) = LinearMap.range (Matrix.toLin' F)) :
        ∃ (J : Matrix (υ ⊕ κ) κ R) (ht : IsUnit (Matrix.fromCols F J).det)
          (hd : IsUnit (G * J).det),
          Nonempty ((MatrixSplitData.ofChart (matrixChart F G J hgf ht hd)).CoordinateRing ≃ₐ[R]
            MvPolynomial (υ × κ) R) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.ExactSequenceChart.MatrixSplitData.ofChart, OAI.IntegralCharacterVarieties.ExactSequenceChart.matrixChart