OAI/AlgebraicGeometry/CharacterVarieties/Frames/AtomicFlags.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IntegralCharacterVarieties.NamedBandGrades.actual_named_atomic_band line 14

   Source documentation

   A framed flag pair determines a finite atom-conservative band, with frames at every split, swap and merge vertex and the original named endpoint quotient projections.

   theorem actual_named_atomic_band
       (a : α → Fin n) (b : β → Fin m)
       (f : (α → K) ≃ₗ[K] V) (h : (β → K) ≃ₗ[K] V) :
       ∃ (d : RankShape n m (Module.finrank K V)) (e : (Atoms d → K) ≃ₗ[K] V)
         (row : (k : ℕ) → ({i // rowGrade d i=k} → K) ≃ₗ[K] ({i // (a i).val=k} → K))
         (col : (k : ℕ) → ({i // colGrade d i=k} → K) ≃ₗ[K] ({i // (b i).val=k} → K)),
         (∀ k,framedPrefix (rowGrade d) e k=framedPrefix (fun i => (a i).val) f k) ∧
         (∀ k,framedPrefix (colGrade d) e k=framedPrefix (fun i => (b i).val) h k) ∧
         (∀ k v,v∈framedPrefix (rowGrade d) e (k+1) →
           row k (framedGrade (rowGrade d) e k v)=framedGrade (fun i => (a i).val) f k v) ∧
         (∀ k v,v∈framedPrefix (colGrade d) e (k+1) →
           col k (framedGrade (colGrade d) e k v)=framedGrade (fun i => (b i).val) h k v) ∧
   …

   Mentions: OAI.IntegralCharacterVarieties.NamedBandGrades.Atoms, OAI.IntegralCharacterVarieties.NamedBandGrades.rowGrade, OAI.IntegralCharacterVarieties.NamedBandGrades.colGrade, OAI.IntegralCharacterVarieties.framedPrefix, OAI.IntegralCharacterVarieties.framedGrade