OAI/NumberTheory/DukePrimeDegree/Geometry/OrderedRootElimination.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Gaussian root elimination in row order

Clearing positive roots in lexicographic row order preserves all earlier zeros. The restricted one-root chart is an open embedding into the previous slice, so successive steps can build a chart for the full upper unipotent group.

  1. def OAI.DukePrimeDegree.rootsBefore line 21
  2. def OAI.DukePrimeDegree.pivotsBefore line 24
  3. lemma OAI.DukePrimeDegree.rootsBefore_stable line 27
  4. lemma OAI.DukePrimeDegree.notMem_pivotsBefore line 37
  5. lemma OAI.DukePrimeDegree.one_mem_ordered_eliminationSlice line 42
  6. theorem OAI.DukePrimeDegree.eliminationRoot_isOpenEmbedding line 55

    Source documentation

    The next root factor gives an open coordinate embedding into the slice left by the earlier eliminations.

    theorem eliminationRoot_isOpenEmbedding {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) :
    Topology.IsOpenEmbedding
      (fun z : EliminationSlice (insert (a, b) P) (insert a D) × ℝ =>
        ((eliminationRootHomeomorph P D hab hP hb).symm z).val) :=
…

    Mentions: OAI.DukePrimeDegree.EliminationSlice, OAI.DukePrimeDegree.eliminationRootHomeomorph

  7. def OAI.DukePrimeDegree.orderedEliminationRootHomeomorph line 65
  8. theorem OAI.DukePrimeDegree.eliminationRoot_extend_embedding line 71

    Source documentation

    An existing partial coordinate chart can be extended by the next root while retaining openness and injectivity of the actual map.

    theorem eliminationRoot_extend_embedding {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)
    {T Y : Type*} [TopologicalSpace T] [TopologicalSpace Y]
    (F : EliminationSlice P D × T → Y) (hF : Topology.IsOpenEmbedding F) :
    Topology.IsOpenEmbedding
      (fun z : EliminationSlice (insert (a, b) P) (insert a D) × (ℝ × T) =>
        F (((eliminationRootHomeomorph P D hab hP hb).symm (z.1, z.2.1)).val, z.2.2)) := by
…

    Mentions: OAI.DukePrimeDegree.EliminationSlice, OAI.DukePrimeDegree.eliminationRootHomeomorph