Defect.lean`

47 declarations, 0 contain sorry, 0 declared as axioms

Blocks, defect groups, and the bounded-order formulation of Donovan's conjecture

This file develops supporting results, not a proof of Donovan's conjecture. The algebra of a block is the actual corner b (KG) b = (KG) b, with identity b. Morita equivalence is Mathlib's equivalence of module categories by a linear functor.

We prove finiteness of blocks for a fixed finite-dimensional algebra, existence of defect groups, the conditional reduction from bounded-order to fixed-defect Morita finiteness, and equality of defect subgroups for blocks corresponding under a coefficient-field embedding.

Uniform bounded-defect-order Morita finiteness across varying finite groups remains unproved. Block-idempotent descent and bijectivity, preservation of primitivity, and scalar extension of Morita equivalences are also not established here.

def OAI.Donovan.IsBlockIdempotent line 33
Source documentation
A block is a nonzero primitive idempotent in the center, not necessarily a primitive idempotent of the whole ring.
```
def IsBlockIdempotent (b : A) : Prop :=
…
```
def OAI.Donovan.BlockIdempotent line 38
Source documentation
The block idempotents in a ring.
```
def BlockIdempotent (A : Type u) [Ring A] := {b : A // IsBlockIdempotent b}
…
```
Mentions: OAI.Donovan.IsBlockIdempotent
instance OAI.Donovan.BlockIdempotent.(instance at line 42) line 42
theorem OAI.Donovan.BlockIdempotent.ext line 44
theorem OAI.Donovan.BlockIdempotent.ne_zero line 47
theorem OAI.Donovan.BlockIdempotent.idempotent line 49
theorem OAI.Donovan.BlockIdempotent.central line 52
theorem OAI.Donovan.BlockIdempotent.primitive line 55
abbrev OAI.Donovan.BlockIdempotent.Algebra line 62
Source documentation
The ring of the block: the corner has identity b, rather than the identity of the ambient ring.
```
abbrev Algebra (b : BlockIdempotent A) := b.idempotent.Corner
```
Mentions: OAI.Donovan.BlockIdempotent
theorem OAI.Donovan.BlockIdempotent.mem_corner_iff line 65
Source documentation
For a central idempotent the corner is exactly the summand A b.
```
theorem mem_corner_iff (b : BlockIdempotent A) (x : A) :
    x ∈ Subsemigroup.corner (b : A) ↔ ∃ a : A, a * b = x :=
…
```
Mentions: OAI.Donovan.BlockIdempotent
def OAI.Donovan.BlockIdempotent.scalarHom line 72
Source documentation
Scalars in the block are k b. In particular the identity is b.
```
def scalarHom (b : BlockIdempotent A) : K →+* b.Algebra where
…
```
Mentions: OAI.Donovan.BlockIdempotent
instance OAI.Donovan.BlockIdempotent.algebra line 85
def OAI.Donovan.BlockIdempotent.inclusion line 94
Source documentation
Inclusion of the block into the ambient algebra is linear. It is not generally a unital homomorphism of rings, since the identities differ.
```
def inclusion (b : BlockIdempotent A) : b.Algebra →ₗ[K] A where
…
```
Mentions: OAI.Donovan.BlockIdempotent
theorem OAI.Donovan.BlockIdempotent.inclusion_injective line 101
theorem OAI.Donovan.BlockIdempotent.mul_eq_zero line 114
Source documentation
Distinct primitive central idempotents are orthogonal.
```
theorem mul_eq_zero {b c : BlockIdempotent A} (h : b ≠ c) : (b : A) * c = 0 := by
…
```
Mentions: OAI.Donovan.BlockIdempotent
theorem OAI.Donovan.BlockIdempotent.linearIndependent line 137
Source documentation
Primitive central idempotents form a linearly independent family.
```
theorem linearIndependent : LinearIndependent K (fun b : BlockIdempotent A => (b : A)) := by
…
```
Mentions: OAI.Donovan.BlockIdempotent
theorem OAI.Donovan.BlockIdempotent.finite line 150
Source documentation
A single finite-dimensional algebra has only finitely many blocks. This does not bound the number of Morita types as the algebra varies.
```
theorem finite [Module.Finite K A] : Finite (BlockIdempotent A) :=
…
```
Mentions: OAI.Donovan.BlockIdempotent
theorem OAI.Donovan.BlockIdempotent.finiteDimensional_corner line 155
Source documentation
A block of a finite-dimensional algebra is itself finite-dimensional, for its natural scalar structure.
```
theorem finiteDimensional_corner [Module.Finite K A] (b : BlockIdempotent A) :
    FiniteDimensional K b.Algebra :=
…
```
Mentions: OAI.Donovan.BlockIdempotent
theorem OAI.Donovan.BlockIdempotent.conjugation_fixed line 168
Source documentation
A block idempotent is fixed under conjugation by every group element. Thus it belongs to the domain of each genuine Brauer map.
```
theorem BlockIdempotent.conjugation_fixed (b : BlockIdempotent (MonoidAlgebra K G))
    (g : G) :
    MonoidAlgebra.single g 1 * (b : MonoidAlgebra K G) *
      MonoidAlgebra.single g⁻¹ 1 = (b : MonoidAlgebra K G) := by
…
```
Mentions: OAI.Donovan.BlockIdempotent
def OAI.Donovan.brauerProjection line 179
Source documentation
Delete coefficients outside the centralizer of D. On the D-fixed group algebra in characteristic p, for a p-subgroup D, this is the Brauer map. We only use it on central idempotents; no multiplicativity on the entire group algebra is asserted.
```
def brauerProjection (D : Subgroup G) (x : MonoidAlgebra K G) :
    MonoidAlgebra K (Subgroup.centralizer (D : Set G)) :=
…
```
theorem OAI.Donovan.brauerProjection_coeff line 184
theorem OAI.Donovan.brauerProjection_zero line 188
def OAI.Donovan.IsDefectGroup line 193
Source documentation
Defect groups are maximal, under inclusion, among the p-subgroups with nonzero Brauer image. This does not impose a commutativity condition.
```
def IsDefectGroup (p : ℕ) (b : BlockIdempotent (MonoidAlgebra K G))
    (D : Subgroup G) : Prop :=
…
```
Mentions: OAI.Donovan.BlockIdempotent
theorem OAI.Donovan.brauerProjection_bot_eq_zero_iff line 197
theorem OAI.Donovan.exists_defectGroup_ge line 210
Source documentation
Any p-subgroup with nonzero Brauer image is contained in a defect group. This uses finiteness of the subgroup poset.
```
theorem exists_defectGroup_ge [Finite G] (p : ℕ)
    (b : BlockIdempotent (MonoidAlgebra K G)) (Q : Subgroup G)
    (hQ : IsPGroup p Q) (hbQ : brauerProjection Q (b : MonoidAlgebra K G) ≠ 0) :
    ∃ D : Subgroup G, Q ≤ D ∧ IsDefectGroup p b D :=
…
```
Mentions: OAI.Donovan.BlockIdempotent, OAI.Donovan.brauerProjection, OAI.Donovan.IsDefectGroup
theorem OAI.Donovan.exists_defectGroup line 218
Source documentation
A finite-group block has at least one defect group as defined above.
```
theorem exists_defectGroup [Finite G] (p : ℕ)
    (b : BlockIdempotent (MonoidAlgebra K G)) :
    ∃ D : Subgroup G, IsDefectGroup p b D := by
…
```
Mentions: OAI.Donovan.BlockIdempotent, OAI.Donovan.IsDefectGroup
structure OAI.Donovan.FiniteGroupBlock line 234
Source documentation
A block of a finite group algebra over K. The group is allowed to vary over all finite group types in the specified universe.
```
structure FiniteGroupBlock (K : Type v) [Field K] where
…
```
abbrev OAI.Donovan.FiniteGroupBlock.Algebra line 247
Source documentation
The actual block algebra KGb.
```
abbrev Algebra (B : FiniteGroupBlock.{u, v} K) := B.block.Algebra
```
def OAI.Donovan.FiniteGroupBlock.moritaSetoid line 251
Source documentation
The equivalence relation is linear Morita equivalence, not ring isomorphism or equivalence of the underlying un-enriched categories.
```
def moritaSetoid (K : Type v) [Field K] : Setoid (FiniteGroupBlock.{u, v} K) where
…
```
def OAI.Donovan.MoritaClass line 259
Source documentation
Morita classes of all finite-group blocks over the fixed field K.
```
def MoritaClass (K : Type v) [Field K] :=
…
```

def OAI.Donovan.moritaClass line 263

Source documentation

The Morita class represented by a block.

def moritaClass {K : Type v} [Field K] (B : FiniteGroupBlock.{u, v} K) :
    MoritaClass.{u, v} K := Quotient.mk _ B

def OAI.Donovan.HasDefectAtMost line 267
Source documentation
The block has a defect group whose order is at most M.
```
def HasDefectAtMost {K : Type v} [Field K] (p M : ℕ) (B : FiniteGroupBlock.{u, v} K) :
    Prop :=
…
```

def OAI.Donovan.HasDefectIsomorphic line 272

Source documentation

The block has a defect group isomorphic to the given group P.

def HasDefectIsomorphic {K : Type v} [Field K] (p : ℕ) (P : Type w) [Group P]
    (B : FiniteGroupBlock.{u, v} K) : Prop :=
…

def OAI.Donovan.boundedClasses line 277
Source documentation
Morita classes represented by blocks with a defect group of order at most M.
```
def boundedClasses (p : ℕ) (K : Type v) [Field K] (M : ℕ) :
    Set (MoritaClass.{u, v} K) :=
…
```
def OAI.Donovan.fixedDefectClasses line 282
Source documentation
Morita classes represented by blocks with a defect group isomorphic to P.
```
def fixedDefectClasses (p : ℕ) (K : Type v) [Field K] (P : Type w) [Group P] :
    Set (MoritaClass.{u, v} K) :=
…
```
theorem OAI.Donovan.moritaClass_eq_iff line 289
Source documentation
Equality of classes means linear Morita equivalence of the actual block algebras.
```
theorem moritaClass_eq_iff (B C : FiniteGroupBlock.{u, v} K) :
    moritaClass B = moritaClass C ↔ IsMoritaEquivalent K B.Algebra C.Algebra :=
…
```
Mentions: OAI.Donovan.moritaClass
theorem OAI.Donovan.HasDefectAtMost.pos line 294
Source documentation
The order of a defect group is positive.
```
theorem HasDefectAtMost.pos {M : ℕ} {B : FiniteGroupBlock.{u, v} K}
    (h : HasDefectAtMost p M B) : 0 < M := by
…
```
Mentions: OAI.Donovan.HasDefectAtMost
theorem OAI.Donovan.exists_positive_defect_bound line 301
Source documentation
Every block is covered by some positive bound; the bounded-order classes are not made empty by the definition of a defect group.
```
theorem exists_positive_defect_bound (p : ℕ) (B : FiniteGroupBlock.{u, v} K) :
    ∃ M : ℕ, 0 < M ∧ HasDefectAtMost p M B := by
…
```
Mentions: OAI.Donovan.HasDefectAtMost
theorem OAI.Donovan.HasDefectIsomorphic.hasDefectAtMost line 307
Source documentation
An isomorphism of defect groups gives equality of their orders.
```
theorem HasDefectIsomorphic.hasDefectAtMost {P : Type w} [Group P]
    {B : FiniteGroupBlock.{u, v} K} (h : HasDefectIsomorphic p P B) :
    HasDefectAtMost p (Nat.card P) B := by
…
```
Mentions: OAI.Donovan.HasDefectIsomorphic, OAI.Donovan.HasDefectAtMost

theorem OAI.Donovan.fixedDefectClasses_subset line 314

Source documentation

The fixed-defect classes are a subset of the bounded-order classes.

theorem fixedDefectClasses_subset (p : ℕ) (K : Type v) [Field K]
    (P : Type w) [Group P] :
    fixedDefectClasses.{u, v, w} p K P ⊆ boundedClasses p K (Nat.card P) := by
…

Mentions: OAI.Donovan.boundedClasses

theorem OAI.Donovan.finite_fixedDefectClasses_of_bounded line 322
Source documentation
The elementary fixed-defect reduction. Uniform bounded-order finiteness is an assumption, not a result proved here. There is no abelian hypothesis on P.
```
theorem finite_fixedDefectClasses_of_bounded
    (h : ∀ M : ℕ, 0 < M → (boundedClasses.{u, v} p K M).Finite)
    (P : Type w) [Group P] [Finite P] :
    (fixedDefectClasses.{u, v, w} p K P).Finite :=
…
```
def OAI.Donovan.FiniteGroupBlock.ofBlock line 334
Source documentation
Regard a block for one fixed ambient group as a member of the class of all finite-group blocks.
```
def ofBlock (b : BlockIdempotent (MonoidAlgebra K G)) : FiniteGroupBlock.{u, v} K where
…
```
Mentions: OAI.Donovan.BlockIdempotent
theorem OAI.Donovan.finite_classes_for_one_group line 342
Source documentation
For a fixed finite group, its blocks give a finite collection of Morita classes. This is only the fixed-ambient-group claim, not Donovan's theorem.
```
theorem finite_classes_for_one_group (K : Type v) [Field K]
    (G : Type u) [Group G] [Finite G] :
    (Set.range (fun b : BlockIdempotent (MonoidAlgebra K G) =>
      moritaClass (FiniteGroupBlock.ofBlock b))).Finite := by
…
```
Mentions: OAI.Donovan.BlockIdempotent, OAI.Donovan.moritaClass, OAI.Donovan.FiniteGroupBlock.ofBlock
theorem OAI.Donovan.coefficientExtension_injective line 357
Source documentation
Applying a field embedding to group-ring coefficients is injective.
```
theorem coefficientExtension_injective (f : K →+* L) :
    Function.Injective (MonoidAlgebra.mapRingHom G f) := by
…
```

theorem OAI.Donovan.brauerProjection_coefficientExtension line 368

Source documentation

Deleting coefficients outside the centralizer commutes with applying a field embedding. This is the coefficient calculation for the Brauer map.

theorem brauerProjection_coefficientExtension (f : K →+* L) (D : Subgroup G)
    (x : MonoidAlgebra K G) :
    brauerProjection D (MonoidAlgebra.mapRingHom G f x) =
      MonoidAlgebra.mapRingHom (Subgroup.centralizer (D : Set G)) f
        (brauerProjection D x) := by
…

Mentions: OAI.Donovan.brauerProjection

theorem OAI.Donovan.brauerProjection_coefficientExtension_eq_zero_iff line 379
Source documentation
The vanishing criterion used to compute defects is unchanged by a coefficient-field embedding.
```
theorem brauerProjection_coefficientExtension_eq_zero_iff (f : K →+* L)
    (D : Subgroup G) (x : MonoidAlgebra K G) :
    brauerProjection D (MonoidAlgebra.mapRingHom G f x) = 0 ↔
      brauerProjection D x = 0 := by
…
```
Mentions: OAI.Donovan.brauerProjection
theorem OAI.Donovan.isDefectGroup_coefficientExtension_iff line 394
Source documentation
If two actual block idempotents correspond by coefficient extension, then their defect subgroups are identical. This lemma does not assert that every block descends, or that primitivity is preserved.
```
theorem isDefectGroup_coefficientExtension_iff (f : K →+* L) (p : ℕ)
    (b : BlockIdempotent (MonoidAlgebra K G))
    (c : BlockIdempotent (MonoidAlgebra L G))
    (h : MonoidAlgebra.mapRingHom G f (b : MonoidAlgebra K G) = (c : MonoidAlgebra L G))
    (D : Subgroup G) : IsDefectGroup p c D ↔ IsDefectGroup p b D := by
…
```
Mentions: OAI.Donovan.BlockIdempotent, OAI.Donovan.IsDefectGroup