Flags.lean`

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Split flags and their matrix equations, following Integral points on character varieties of curves.

def OAI.IntegralCharacterVarieties.coordinatePrefix line 16
Source documentation
The coordinate prefix attached to a split finite filtration.
```
def coordinatePrefix (R : Type*) [CommRing R] {α : Type*}
    (a : α → ℕ) (k : ℕ) : Submodule R (α → R) where
…
```
def OAI.IntegralCharacterVarieties.coordinateGrade line 23
def OAI.IntegralCharacterVarieties.filteredMatrixStabilizer line 29
def OAI.IntegralCharacterVarieties.retainedLiftEntries line 37
Source documentation
Free blocks in the identified-quotient lift itself.
```
def retainedLiftEntries {α β : Type*} (a : α → ℕ) (b : β → ℕ) :=
…
```
def OAI.IntegralCharacterVarieties.refinementFiberEntries line 41
Source documentation
Additional stabilizer blocks after refining a coarse block.
```
def refinementFiberEntries {α β : Type*} (a : α → ℕ) (b : β → ℕ) (f : ℕ → ℕ) :=
…
```
lemma OAI.IntegralCharacterVarieties.filteredMatrixStabilizer_iff line 44
lemma OAI.IntegralCharacterVarieties.prefix_zero_eq_bot line 71
lemma OAI.IntegralCharacterVarieties.prefix_mono line 83
def OAI.IntegralCharacterVarieties.SameCoordinateFlag line 89
Source documentation
Equality of parallel identified flags in a fixed split basis: not only preservation of dimensions, but equality of each submodule and each induced coordinate projection on the named grade.
```
def SameCoordinateFlag (e : (α → R) ≃ₗ[R] (α → R)) : Prop :=
…
```
theorem OAI.IntegralCharacterVarieties.sameCoordinateFlag_iff_lowering line 95
Source documentation
The strict-upper criterion is valid over every full coefficient ring.
```
theorem sameCoordinateFlag_iff_lowering (e : (α → R) ≃ₗ[R] (α → R)) :
    SameCoordinateFlag a e ↔ ∀ k v, v ∈ coordinatePrefix R a (k+1) →
      e v-v ∈ coordinatePrefix R a k := by
…
```
Mentions: OAI.IntegralCharacterVarieties.SameCoordinateFlag, OAI.IntegralCharacterVarieties.coordinatePrefix
def OAI.IntegralCharacterVarieties.framedPrefix line 148
Source documentation
A freely split flag with its named quotient identifications.
```
def framedPrefix (e : (α → R) ≃ₗ[R] V) (k : ℕ) : Submodule R V :=
…
```
def OAI.IntegralCharacterVarieties.framedGrade line 151
def OAI.IntegralCharacterVarieties.SameFramedFlag line 155
Source documentation
Equality includes the quotient maps, not just the underlying flag.
```
def SameFramedFlag (e f : (α → R) ≃ₗ[R] V) : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.sameFramedFlag_iff line 159
def OAI.IntegralCharacterVarieties.HomTransport.coefficients line 212
Source documentation
The coefficient matrix for h ↦ U h Q (column indices on Hom).
```
def coefficients (U : Matrix α α R) (Q : Matrix β β R) :
    Matrix (α × β) (α × β) R := Matrix.kronecker U Q.transpose
…
```
lemma OAI.IntegralCharacterVarieties.HomTransport.coefficients_apply line 216
lemma OAI.IntegralCharacterVarieties.HomTransport.coefficients_mul line 220
lemma OAI.IntegralCharacterVarieties.HomTransport.coefficients_one line 227
def OAI.IntegralCharacterVarieties.HomTransport.unit line 232
Source documentation
Every change of the named U,Q bases induces this invertible matrix on the free module of extension entries. Inverses are polynomial in the inverse base-change entries retained in the GL presentation.
```
def unit (U : (Matrix α α R)ˣ) (Q : (Matrix β β R)ˣ) :
    (Matrix (α × β) (α × β) R)ˣ where
…
```
lemma OAI.IntegralCharacterVarieties.HomTransport.coefficients_map line 243
Source documentation
Coefficient-ring functoriality, including at non-field points.
```
lemma coefficients_map {S : Type*} [CommRing S] (φ : R →+* S)
    (U : Matrix α α R) (Q : Matrix β β R) :
    (coefficients U Q).map φ=coefficients (U.map φ) (Q.map φ) := by
…
```
Mentions: OAI.IntegralCharacterVarieties.HomTransport.coefficients
lemma OAI.IntegralCharacterVarieties.HomTransport.coefficients_mulVec line 250
def OAI.IntegralCharacterVarieties.HomTransport.matrixUnitEquiv line 264
Source documentation
Linear equivalence defined by a transport and its inverse.
```
def matrixUnitEquiv {ι : Type*} [Fintype ι] [DecidableEq ι]
    (U : (Matrix ι ι R)ˣ) : (ι → R) ≃ₗ[R] (ι → R) where
…
```
lemma OAI.IntegralCharacterVarieties.HomTransport.matrixUnitEquiv_apply line 275
lemma OAI.IntegralCharacterVarieties.HomTransport.matrixUnitEquiv_symm_apply line 278
lemma OAI.IntegralCharacterVarieties.HomTransport.hom_coordinate_transform line 282
theorem OAI.IntegralCharacterVarieties.sameFramedFlag_matrix_iff line 300
Source documentation
Exact split-frame polynomial equations for equality of flags and identified quotients. Both inverse matrices are variables in the ambient GL scheme; no inversion is added to the integers.
```
theorem sameFramedFlag_matrix_iff (P Q : (Matrix α α R)ˣ) :
    SameFramedFlag a (matrixUnitEquiv P) (matrixUnitEquiv Q) ↔
    ∀ i j, a j ≤ a i → ((↑Q⁻¹ : Matrix α α R)*(P : Matrix α α R)) i j=
      (1 : Matrix α α R) i j := by
…
```
Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag