DirectedBound.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.LittleFinitistic.DirectedBound.DirectedSystem line 18
Source documentation
The displayed algebraic hypotheses of Section 3, Lemma directed-bound. The field and algebra are unital; zero idempotents are allowed by the source.
```
structure DirectedSystem (k A : Type u) [Field k] [Ring A] [Algebra k A] (n : ℕ) where
…
```
def OAI.LittleFinitistic.DirectedBound.DirectedSystem.Supported line 32
Source documentation
Vanishing of vertex components below p, for arbitrary modules.
```
def Supported (p : ℕ) : Prop := ∀ j : Fin n, j.val < p → ∀ m : M, D.e j • m = 0
```
def OAI.LittleFinitistic.DirectedBound.DirectedSystem.evaluation line 35
Source documentation
Evaluation of the free induced module.
```
def evaluation (_D : DirectedSystem k A n) : A ⊗[k] M →ₗ[A] M := AlgebraTensorModule.lift
…
```
Mentions: OAI.LittleFinitistic.DirectedBound.DirectedSystem
theorem OAI.LittleFinitistic.DirectedBound.DirectedSystem.evaluation_tmul line 43
def OAI.LittleFinitistic.DirectedBound.DirectedSystem.vertexProjection line 47
Source documentation
One summand of the separable diagonal projection.
```
def vertexProjection (i : Fin n) : A ⊗[k] M →ₗ[A] A ⊗[k] M :=
…
```
theorem OAI.LittleFinitistic.DirectedBound.DirectedSystem.vertexProjection_tmul line 61
def OAI.LittleFinitistic.DirectedBound.DirectedSystem.projection line 64
theorem OAI.LittleFinitistic.DirectedBound.DirectedSystem.projection_tmul line 66
lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.projection_vertexTensor line 71
lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.projection_idempotent line 80
lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.evaluation_projection line 88
abbrev OAI.LittleFinitistic.DirectedBound.DirectedSystem.Cover line 97
Source documentation
The manuscript's projective cover, realized as an actual direct summand.
```
abbrev Cover := LinearMap.range (D.projection M)
```
instance OAI.LittleFinitistic.DirectedBound.DirectedSystem.cover_addCommGroup line 99
instance OAI.LittleFinitistic.DirectedBound.DirectedSystem.cover_projective line 102
abbrev OAI.LittleFinitistic.DirectedBound.DirectedSystem.coverMap line 111
Source documentation
Evaluation restricted to the projective summand.
```
abbrev coverMap : D.Cover M →ₗ[A] M :=
…
```
lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.coverMap_surjective line 114
lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.low_tensor line 120
lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.low_projection line 134
lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.kernel_supported line 150
Source documentation
One syzygy raises the lower bound on the support by one.
```
lemma kernel_supported {p : ℕ} (hM : D.Supported M p) :
    D.Supported (LinearMap.ker (D.coverMap M)) (p + 1) := by
…
```
lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.supported_subsingleton line 166

theorem OAI.LittleFinitistic.DirectedBound.DirectedSystem.supported_projectiveDimensionLT line 177

Source documentation

The support induction uses genuine projective dimensions (vanishing Ext), via mathlib's short exact sequence dimension-shifting theorem.

theorem supported_projectiveDimensionLT (r : ℕ) :
    ∀ (p : ℕ), p + r = n → ∀ (N : Type (max u v))
      [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N],
      D.Supported N p → HasProjectiveDimensionLT (ModuleCat.of A N) r := by
…

theorem OAI.LittleFinitistic.DirectedBound.DirectedSystem.all_modules_projectiveDimensionLT line 199
Source documentation
Every left module is covered, with no finite generation restriction.
```
theorem all_modules_projectiveDimensionLT (N : ModuleCat.{max u v} A) :
    HasProjectiveDimensionLT N n := by
…
```
theorem OAI.LittleFinitistic.DirectedBound.DirectedSystem.all_modules_projectiveDimension_le line 207
def OAI.LittleFinitistic.DirectedBound.DirectedSystem.opposite line 214
Source documentation
Reversing the vertices transfers exactly the hypotheses to right modules.
```
def opposite : DirectedSystem k Aᵐᵒᵖ n where
…
```
Mentions: OAI.LittleFinitistic.DirectedBound.DirectedSystem

theorem OAI.LittleFinitistic.DirectedBound.DirectedSystem.both_sides_projectiveDimension_le line 243

Source documentation

Both sides, quantified over arbitrary modules in any larger universe.

theorem both_sides_projectiveDimension_le :
    (∀ N : ModuleCat.{max u v} A, projectiveDimension N ≤ (n - 1 : ℕ)) ∧
    (∀ N : ModuleCat.{max u v} Aᵐᵒᵖ, projectiveDimension N ≤ (n - 1 : ℕ)) :=
…

theorem OAI.LittleFinitistic.DirectedBound.DirectedSystem.both_sides_globalDimension_le line 249

Source documentation

The global dimensions are the suprema of the actual module projective dimensions.

theorem both_sides_globalDimension_le :
    (⨆ N : ModuleCat.{max u v} A, projectiveDimension N) ≤ (n - 1 : ℕ) ∧
    (⨆ N : ModuleCat.{max u v} Aᵐᵒᵖ, projectiveDimension N) ≤ (n - 1 : ℕ) :=
…

theorem OAI.LittleFinitistic.DirectedBound.directed_bound line 259

Source documentation

Section 3, Lemma directed-bound, with its displayed hypotheses expanded. Finite dimensionality is retained here although the proof proves a stronger result.

theorem directed_bound [FiniteDimensional k A] (e : Fin n → A)
    (idem : ∀ i, e i * e i = e i)
    (orthogonal : ∀ i j, i ≠ j → e i * e j = 0)
    (complete : ∑ i, e i = 1)
    (diagonal : ∀ i a, ∃ c : k, e i * a * e i = c • e i)
    (directed : ∀ i j, j < i → ∀ a, e j * a * e i = 0) :
    (⨆ N : ModuleCat.{max u v} A, projectiveDimension N) ≤ (n - 1 : ℕ) ∧
    (⨆ N : ModuleCat.{max u v} Aᵐᵒᵖ, projectiveDimension N) ≤ (n - 1 : ℕ) :=
…