Statement and definitions
The formal theorems
The independent statement uses finite-dimensional right modules, represented in Lean as modules over Aᵐᵒᵖ. A complete finite family of indecomposable modules expresses finite representation type. The radical of A is Mathlib’s Jacobson radical.
For Theorem B, the radical J of the category of indecomposable modules gives the spaces of irreducible maps J/J2; their dimensions are the arrows of ΓA. The translate τX is defined by an almost split sequence 0 → τX → E → X → 0. The mesh category is the linear path category of ΓA modulo the mesh relations, the sums of all paths τX → Y → X. Standardness asks for a k-linear equivalence of this mesh category with the indecomposable modules, sending each vertex to its module. The statement also records that every space of irreducible maps has dimension at most one, so these are exactly the mesh relations of ΓA.
MultiplicativeBasisDeformations.Statement.theoremA and Statement.theoremB prove these statements. The bridge identifies the translate defined by almost split sequences with the one of the library and normalizes the mesh coefficients of the library to one.
Independent Challenge
This display is generated from Challenge.lean. Its two deliberate sorrys are the statement placeholders used by Comparator. The corresponding Solution.lean supplies the proofs and does not import the Challenge.
Show the complete Lean statement (290 lines)
-- Generated by scripts/generate_challenge.py; edit Statement.lean.
import Mathlib
/-!
# Independent statement of Theorems A and B
These definitions use only Mathlib. They state the two main theorems of
*Multiplicative bases and deformations of representation-finite algebras*:
* **Theorem A.** Every finite-dimensional representation-finite algebra over an
algebraically closed field has a normed multiplicative basis.
* **Theorem B.** Every basic finite-dimensional representation-finite algebra
over an algebraically closed field of characteristic different from two is
standard.
Modules are right modules, that is, modules over the opposite algebra.
Connections to the proof library are proved in separate modules.
-/
set_option autoImplicit false
noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped ModuleCat.Algebra
namespace MultiplicativeBasisDeformations.Statement
universe u
variable (k A : Type u) [Field k] [Ring A] [Algebra k A]
/-! ## Representation-finite algebras -/
/-- One representative of each isomorphism class of finite-dimensional
indecomposable right modules. Existence of such a family expresses finite
representation type. -/
structure IndecomposableFamily where
size : ℕ
obj : Fin size → ModuleCat.{u} Aᵐᵒᵖ
finite : ∀ i, Module.Finite k (obj i)
indecomposable : ∀ i, Indecomposable (obj i)
distinct : ∀ {i j}, Nonempty (obj i ≅ obj j) → i = j
complete : ∀ M : ModuleCat.{u} Aᵐᵒᵖ,
Module.Finite k M → Indecomposable M → ∃ i, Nonempty (M ≅ obj i)
/-- `A` is representation-finite: it has finitely many isomorphism classes of
finite-dimensional indecomposable right modules. -/
def IsRepresentationFinite : Prop := Nonempty (IndecomposableFamily k A)
/-! ## Normed multiplicative bases -/
/-- The power `(rad A)^n` of the Jacobson radical, as a `k`-subspace of `A`. -/
def radicalPow (n : ℕ) : Submodule k A :=
((Ring.jacobson A).restrictScalars k) ^ n
variable {A} in
/-- A primitive idempotent: a nonzero idempotent `e` such that the only
idempotents of the corner `eAe` are `0` and `e`. -/
def IsPrimitiveIdempotent (e : A) : Prop :=
IsIdempotentElem e ∧ e ≠ 0 ∧
∀ f : A, IsIdempotentElem f → e * f = f → f * e = f → f = 0 ∨ f = e
variable {k A} in
/-- A normed multiplicative basis: products of basis elements are zero or basis
elements; the basis contains a complete set of primitive orthogonal
idempotents; and it meets every radical power `(rad A)^n`, `n ≥ 1`, in a basis
of that power. -/
structure IsNormedMultiplicativeBasis {ι : Type*} (b : Module.Basis ι k A) : Prop where
multiplicative : ∀ i j, b i * b j = 0 ∨ ∃ l, b i * b j = b l
idempotents :
∃ E : Finset ι,
CompleteOrthogonalIdempotents (fun i : E => b i) ∧
∀ i ∈ E, IsPrimitiveIdempotent (b i)
radicalPow :
∀ n : ℕ, 1 ≤ n →
Submodule.span k (b '' {i | b i ∈ radicalPow k A n}) = radicalPow k A n
/-- `A` has a normed multiplicative basis. -/
def HasNormedMultiplicativeBasis : Prop :=
∃ (ι : Type u) (b : Module.Basis ι k A), IsNormedMultiplicativeBasis b
/-- **Theorem A**, as a proposition: a finite-dimensional representation-finite
algebra over an algebraically closed field has a normed multiplicative basis. -/
def TheoremA [IsAlgClosed k] [FiniteDimensional k A] : Prop :=
IsRepresentationFinite k A → HasNormedMultiplicativeBasis k A
/-! ## Basic algebras -/
/-- `A` is basic: it has a complete set of primitive orthogonal idempotents
`e_i` whose principal right ideals `e_i A` are pairwise nonisomorphic. Here
`e_i A ≅ e_j A` is expressed by elements `x ∈ e_i A e_j`, `y ∈ e_j A e_i` with
`xy = e_i` and `yx = e_j`. -/
def IsBasic : Prop :=
∃ (n : ℕ) (e : Fin n → A),
CompleteOrthogonalIdempotents e ∧ (∀ i, IsPrimitiveIdempotent (e i)) ∧
∀ i j, (∃ x y : A, e i * x * e j = x ∧ e j * y * e i = y ∧
x * y = e i ∧ y * x = e j) → i = j
/-! ## The Auslander–Reiten quiver -/
variable {k A}
variable (S : IndecomposableFamily k A)
/-- `ind(mod A)`: the full subcategory of right modules on the chosen
representatives. -/
abbrev Ind := InducedCategory (ModuleCat.{u} Aᵐᵒᵖ) S.obj
/-- A radical morphism of `ind(mod A)`: `1 - f ≫ g` is invertible for every
`g` in the opposite direction. -/
def IsRadical {X Y : Ind S} (f : X ⟶ Y) : Prop :=
∀ g : Y ⟶ X, IsIso (𝟙 X - f ≫ g)
/-- The powers `J^n(X, Y)` of the radical of `ind(mod A)`: `J⁰ = Hom`, and
`J^{n+1}(X, Y)` is spanned by the composites `f ≫ g` of a radical morphism
`f : X ⟶ Z` and some `g ∈ J^n(Z, Y)`. -/
def radPow : ℕ → ∀ X Y : Ind S, Submodule k (X ⟶ Y)
| 0, _, _ => ⊤
| n + 1, X, Y =>
Submodule.span k
{h | ∃ (Z : Ind S) (f : X ⟶ Z) (g : Z ⟶ Y),
IsRadical S f ∧ g ∈ radPow n Z Y ∧ h = f ≫ g}
/-- The space of irreducible maps `Irr(X, Y) = J(X, Y) / J²(X, Y)`. -/
abbrev Irr (X Y : Ind S) :=
↥(radPow S 1 X Y) ⧸ (radPow S 2 X Y).comap (radPow S 1 X Y).subtype
/-- The vertices of the Auslander–Reiten quiver `Γ_A`. -/
def Vertex : Type := Fin S.size
/-- The Auslander–Reiten quiver `Γ_A`: the arrows `i ⟶ j` are indexed by a
basis of `Irr(X_i, X_j)`. -/
instance arQuiver : Quiver (Vertex S) where
Hom i j := Fin (Module.finrank k (Irr S (show Ind S from i) (show Ind S from j)))
instance : Fintype (Vertex S) := inferInstanceAs (Fintype (Fin S.size))
instance (i j : Vertex S) : Fintype (i ⟶ j) := inferInstanceAs (Fintype (Fin _))
variable (k) in
/-- An almost split sequence `0 → U → E → V → 0` of right modules: a short
exact sequence whose first map is left almost split and whose second map is
right almost split, among finite-dimensional modules. -/
structure IsAlmostSplitSequence {U E V : ModuleCat.{u} Aᵐᵒᵖ} (f : U ⟶ E) (g : E ⟶ V) :
Prop where
comp_eq_zero : f ≫ g = 0
shortExact : (ShortComplex.mk f g comp_eq_zero).ShortExact
not_isSplitMono : ¬ IsSplitMono f
not_isSplitEpi : ¬ IsSplitEpi g
left : ∀ (X : ModuleCat.{u} Aᵐᵒᵖ), Module.Finite k X →
∀ h : U ⟶ X, ¬ IsSplitMono h → ∃ h' : E ⟶ X, f ≫ h' = h
right : ∀ (X : ModuleCat.{u} Aᵐᵒᵖ), Module.Finite k X →
∀ h : X ⟶ V, ¬ IsSplitEpi h → ∃ h' : X ⟶ E, h' ≫ g = h
/-- The Auslander–Reiten translate: `X_t = τ X_i` when there is an almost split
sequence `0 → X_t → E → X_i → 0`. -/
def IsTranslate (t i : Vertex S) : Prop :=
∃ (E : ModuleCat.{u} Aᵐᵒᵖ) (f : S.obj t ⟶ E) (g : E ⟶ S.obj i),
IsAlmostSplitSequence k f g
/-! ## The mesh category `k(Γ_A)` -/
/-- The `k`-linear path category of `Γ_A`: morphisms `i ⟶ j` are finite linear
combinations of paths from `i` to `j`, composed by concatenation. -/
abbrev PathCategory := CategoryTheory.Free k (Paths (Vertex S))
/-- The vertex `i` as an object of the path category. -/
abbrev pathObj (i : Vertex S) : PathCategory S := (i : Paths (Vertex S))
/-- A path as a morphism of the path category. -/
def path {i j : Vertex S} (p : Quiver.Path i j) : pathObj S i ⟶ pathObj S j :=
Finsupp.single p 1
/-- The mesh relation `∑ (σ a) a` from `τ X_i = X_t` to `X_i`: the sum of all
paths `t → j → i` of length two. -/
def meshRelation (t i : Vertex S) : pathObj S t ⟶ pathObj S i :=
∑ j : Vertex S, ∑ b : (t ⟶ j), ∑ a : (j ⟶ i), path S (b.toPath.comp a.toPath)
/-- The family of all mesh relations, indexed by their endpoints. -/
def meshRelations : ∀ X Y : PathCategory S, Set (X ⟶ Y) :=
fun X Y ↦ {r | ∃ (t i : Vertex S) (_ : IsTranslate S t i)
(hX : X = pathObj S t) (hY : Y = pathObj S i),
r = eqToHom hX ≫ meshRelation S t i ≫ eqToHom hY.symm}
/-- The two-sided ideal of the path category linearly generated by the mesh
relations. -/
def meshIdeal (X Y : PathCategory S) : Submodule k (X ⟶ Y) :=
Submodule.span k {f | ∃ (X' Y' : PathCategory S) (r : X' ⟶ Y'), r ∈ meshRelations S X' Y' ∧
∃ (a : X ⟶ X') (b : Y' ⟶ Y), f = a ≫ r ≫ b}
theorem meshIdeal_precomp {X Y Z : PathCategory S} (f : X ⟶ Y) {g : Y ⟶ Z}
(hg : g ∈ meshIdeal S Y Z) : f ≫ g ∈ meshIdeal S X Z := by
induction hg using Submodule.span_induction with
| mem g hg =>
obtain ⟨X', Y', r, hr, a, b, rfl⟩ := hg
exact Submodule.subset_span ⟨X', Y', r, hr, f ≫ a, b, by simp⟩
| zero => simp
| add g h _ _ hg hh => simpa using (meshIdeal S X Z).add_mem hg hh
| smul c g _ hg => simpa using (meshIdeal S X Z).smul_mem c hg
theorem meshIdeal_postcomp {X Y Z : PathCategory S} {f : X ⟶ Y} (g : Y ⟶ Z)
(hf : f ∈ meshIdeal S X Y) : f ≫ g ∈ meshIdeal S X Z := by
induction hf using Submodule.span_induction with
| mem f hf =>
obtain ⟨X', Y', r, hr, a, b, rfl⟩ := hf
exact Submodule.subset_span ⟨X', Y', r, hr, a, b ≫ g, by simp⟩
| zero => simp
| add f h _ _ hf hh => simpa using (meshIdeal S X Z).add_mem hf hh
| smul c f _ hf => simpa using (meshIdeal S X Z).smul_mem c hf
/-- Equality modulo the mesh ideal. -/
def meshRel : HomRel (PathCategory S) := fun {X Y} f g ↦ f - g ∈ meshIdeal S X Y
instance : Congruence (meshRel S) where
equivalence := {
refl := fun f ↦ by simp [meshRel]
symm := fun h ↦ by simpa [meshRel, neg_sub] using (meshIdeal S _ _).neg_mem h
trans := fun hfg hgh ↦ by simpa [meshRel] using (meshIdeal S _ _).add_mem hfg hgh }
comp_left := by
intro X Y Z f g g' h
simpa [meshRel, ← Preadditive.comp_sub] using meshIdeal_precomp S f h
comp_right := by
intro X Y Z f f' g h
simpa [meshRel, ← Preadditive.sub_comp] using meshIdeal_postcomp S g h
theorem meshRel_add {X Y : PathCategory S} (f₁ f₂ g₁ g₂ : X ⟶ Y)
(hf : meshRel S f₁ f₂) (hg : meshRel S g₁ g₂) : meshRel S (f₁ + g₁) (f₂ + g₂) := by
have h := (meshIdeal S X Y).add_mem hf hg
change (f₁ + g₁) - (f₂ + g₂) ∈ meshIdeal S X Y
convert h using 1
abel
/-- The mesh category `k(Γ_A)`: the path category of `Γ_A` modulo the mesh
relations. -/
abbrev MeshCategory := CategoryTheory.Quotient (meshRel S)
instance : Preadditive (MeshCategory S) :=
CategoryTheory.Quotient.preadditive (meshRel S) (fun {_ _} f₁ f₂ g₁ g₂ hf hg ↦
meshRel_add S f₁ f₂ g₁ g₂ hf hg)
instance : (CategoryTheory.Quotient.functor (meshRel S)).Additive :=
CategoryTheory.Quotient.functor_additive (meshRel S) (fun {_ _} f₁ f₂ g₁ g₂ hf hg ↦
meshRel_add S f₁ f₂ g₁ g₂ hf hg)
instance : Linear k (MeshCategory S) :=
CategoryTheory.Quotient.linear k (meshRel S) (fun c {_ _} f g h ↦ by
simpa [meshRel, ← smul_sub] using (meshIdeal S _ _).smul_mem c h)
/-- The vertex `i` as an object of the mesh category. -/
abbrev meshObj (i : Vertex S) : MeshCategory S :=
(CategoryTheory.Quotient.functor (meshRel S)).obj (pathObj S i)
/-- `A` is standard with respect to the family: every space of irreducible maps
has dimension at most one, so that `Γ_A` has at most one arrow between two
vertices and the mesh relations above are those of `Γ_A`, and there is a
`k`-linear equivalence `k(Γ_A) ≃ ind(mod A)` sending each vertex to its module. -/
def IsStandardFor : Prop :=
(∀ X Y : Ind S, Module.finrank k (Irr S X Y) ≤ 1) ∧
∃ F : MeshCategory S ⥤ Ind S, F.IsEquivalence ∧ F.Linear k ∧
∀ i : Vertex S, Nonempty (F.obj (meshObj S i) ≅ (show Ind S from i))
variable (k A)
/-- `A` is standard: it is standard with respect to every complete family of
indecomposable right modules. -/
def IsStandard : Prop := ∀ S : IndecomposableFamily k A, IsStandardFor S
/-- **Theorem B**, as a proposition: a basic finite-dimensional
representation-finite algebra over an algebraically closed field of
characteristic different from two is standard. -/
def TheoremB [IsAlgClosed k] [FiniteDimensional k A] : Prop :=
IsBasic A → IsRepresentationFinite k A → ringChar k ≠ 2 → IsStandard k A
end MultiplicativeBasisDeformations.Statement
universe u
/-- **Theorem A.** Every finite-dimensional representation-finite algebra over an
algebraically closed field has a normed multiplicative basis. -/
theorem MultiplicativeBasisDeformations.Challenge.theoremA
(k A : Type u) [Field k] [IsAlgClosed k] [Ring A] [Algebra k A]
[FiniteDimensional k A] : MultiplicativeBasisDeformations.Statement.TheoremA k A := by
sorry
/-- **Theorem B.** Every basic finite-dimensional representation-finite algebra over
an algebraically closed field of characteristic different from two is standard. -/
theorem MultiplicativeBasisDeformations.Challenge.theoremB
(k A : Type u) [Field k] [IsAlgClosed k] [Ring A] [Algebra k A]
[FiniteDimensional k A] : MultiplicativeBasisDeformations.Statement.TheoremB k A := by
sorry