OAI/NumberTheory/DukePrimeDegree/Geometry/EliminationRootChart.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Root charts preserving earlier Gaussian eliminations

A root translation preserves all previously eliminated entries when each affected source entry is already zero. Restricting the actual root chart gives the next coordinate chart without losing the earlier zeros or the already chosen nonzero diagonal pivots.

  1. def OAI.DukePrimeDegree.ZeroPattern line 21
  2. def OAI.DukePrimeDegree.NonzeroPivots line 24
  3. abbrev OAI.DukePrimeDegree.EliminationSlice line 27
  4. theorem OAI.DukePrimeDegree.zeroPattern_root_translate line 30
  5. theorem OAI.DukePrimeDegree.nonzeroPivots_root_translate line 43
  6. lemma OAI.DukePrimeDegree.elimination_pivot_isOpen line 51
  7. def OAI.DukePrimeDegree.eliminationRootHomeomorph line 59

    Source documentation

    One Gaussian coordinate, restricted to the already eliminated entries and nonzero pivots. The new transverse slice records the next zero and pivot exactly.

    def eliminationRootHomeomorph {n : ℕ} (P : Finset (Fin n × Fin n))
    (D : Finset (Fin n)) {a b : Fin n} (hab : a ≠ b)
    (hP : ∀ r, (r, b) ∈ P → (r, a) ∈ P) (hb : b ∉ D) :
    {g : EliminationSlice P D // g.val.val a a ≠ 0} ≃ₜ
      EliminationSlice (insert (a, b) P) (insert a D) × ℝ where
…

    Mentions: OAI.DukePrimeDegree.EliminationSlice