Monotone invariants and the non-membership criterion

The abstract skeleton of the criterion used to prove that an inverse H⁻¹ does not have entries in a localization U_Σ (Definition 3.3 and Theorem 3.4).

A monotone invariant (MonotoneInvariant) is a function μ from square matrices over a ring P to ℕ∞ that is unchanged by relabelling, by padding with an identity block and by multiplication by invertible matrices, and that does not decrease when passing from F to a product G₁ F G₂. (In the paper square matrices are indexed by 1, …, n, so relabelling is invisible there; here matrices are indexed by arbitrary finite types and invariance under reindex is part of the definition.) Stable association (StablyAssociated, Cohn §0.5) is association after padding with identity blocks.

What is a hypothesis

The ring-theoretic input of Theorem 3.4 is not formalized here:

• the matrix localization lemma (Lemma 3.1), which rests on the theory of firs and semifirs (Cohn 2006, §3.2, Thm 3.2.3, Prop. 7.5.9; Schofield 2007, Thm 5.6);
• the existence of a complete factorization Q = G₁ 𝒜 G₂ with an atom 𝒜 stably associated with the given atomic factor, and the transitivity of stable association (Cohn 2006, Cor. 0.5.5).

not_inverseInU takes their combined conclusion as the named hypothesis hloc: if H⁻¹ has entries in U_Σ (an opaque proposition inverseInU), then some Q ∈ Σ factors as G₁ 𝒜 G₂ with 𝒜 stably associated with the atomic factor G of H. Neither atoms nor U_Σ appear otherwise: the argument only uses the two conditions of Definition 3.3.

Main results

• MonotoneInvariant.eq_of_stablyAssoc: a monotone invariant is constant on stable association classes.
• MonotoneInvariant.le_of_factor: if Q = G₁ 𝒜 G₂ with 𝒜 stably associated with G, then μ G ≤ μ Q.
• not_inverseInU (Theorem 3.4): if every Q ∈ Σ has a monotone invariant μ_Q with μ_Q Q < μ_Q G, then H⁻¹ does not have entries in U_Σ (given hloc).
• corankInvariant (Example (b)): for a ring homomorphism Θ : P →+* Matrix (Fin m) (Fin m) K into matrices over a field, the corank of the evaluated matrix F^Θ is a monotone invariant. The monotonicity is Mathlib's Matrix.rank_mul_le_left / Matrix.rank_mul_le_right; invariance under invertible factors is Matrix.rank_mul_eq_left_of_isUnit_det / Matrix.rank_mul_eq_right_of_isUnit_det; padding uses the block bounds of Formalizations.LinearAlgebra.Matrix.Rank. Here K is commutative (Mathlib's Matrix.rank needs a commutative ring); the paper allows a skew field.

References

• P. M. Cohn, Free ideal rings and localization in general rings, Cambridge Univ. Press, 2006, §0.5 (stable association), Cor. 0.5.5, §3.2.
• A. H. Schofield, Representations of rings over skew fields, and the 2007 preprint cited in the paper, Thm 5.6.

def ThreeAxes.Criterion.StablyAssociated {P : Type u_1} [Ring P] {ι ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] (F : Matrix ι ι P) (G : Matrix ι' ι' P) : Prop

F and G are stably associated: F ⊕ I_p and G ⊕ I_q are associated (after a relabelling e of the index sets), i.e. F ⊕ I_p = M (G ⊕ I_q) N with M, N invertible.

Equations

• One or more equations did not get rendered due to their size.

structure ThreeAxes.Criterion.MonotoneInvariant (P : Type u_1) [Ring P] : Type (max 1 u_1)

A monotone invariant (Definition 3.3): a function from square matrices over P to ℕ∞, invariant under relabelling, padding with identity blocks and multiplication by invertible matrices (condition 1), and satisfying μ F ≤ μ (G₁ F G₂) (condition 2).

• μ {ι : Type} [Fintype ι] [DecidableEq ι] : Matrix ι ι P → ℕ∞

  The invariant.

• reindex_eq {ι ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] (e : ι ≃ ι') (F : Matrix ι ι P) : self.μ ((Matrix.reindex e e) F) = self.μ F

  Relabelling the index set does not change μ.

• pad_eq {ι : Type} [Fintype ι] [DecidableEq ι] (p : ℕ) (F : Matrix ι ι P) : self.μ (Matrix.fromBlocks F 0 0 1) = self.μ F

  Condition 1: padding with an identity block.

• mul_eq {ι : Type} [Fintype ι] [DecidableEq ι] (M F N : Matrix ι ι P) : IsUnit M → IsUnit N → self.μ (M * F * N) = self.μ F

  Condition 1: invertible factors.

• le_mul {ι : Type} [Fintype ι] [DecidableEq ι] (G₁ F G₂ : Matrix ι ι P) : self.μ F ≤ self.μ (G₁ * F * G₂)

  Condition 2: μ F ≤ μ (G₁ F G₂).

theorem ThreeAxes.Criterion.MonotoneInvariant.eq_of_stablyAssoc {P : Type u_1} [Ring P] (I : MonotoneInvariant P) {ι ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] {F : Matrix ι ι P} {G : Matrix ι' ι' P} (h : StablyAssociated F G) : I.μ F = I.μ G

A monotone invariant is constant on stable association classes.

theorem ThreeAxes.Criterion.MonotoneInvariant.le_of_factor {P : Type u_1} [Ring P] (I : MonotoneInvariant P) {ι ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] {Q A G₁ G₂ : Matrix ι ι P} {G : Matrix ι' ι' P} (hQ : Q = G₁ * A * G₂) (hA : StablyAssociated A G) : I.μ G ≤ I.μ Q

If Q = G₁ 𝒜 G₂ and 𝒜 is stably associated with G, then μ G ≤ μ Q.

theorem ThreeAxes.Criterion.not_inverseInU {P : Type u_1} [Ring P] {ι : Type} [Fintype ι] [DecidableEq ι] (G : Matrix ι ι P) {J : Type u_2} (Q : J → (n : ℕ) × Matrix (Fin n) (Fin n) P) (inverseInU : Prop) (hloc : inverseInU → ∃ (j : J) (A : Matrix (Fin (Q j).fst) (Fin (Q j).fst) P) (G₁ : Matrix (Fin (Q j).fst) (Fin (Q j).fst) P) (G₂ : Matrix (Fin (Q j).fst) (Fin (Q j).fst) P), (Q j).snd = G₁ * A * G₂ ∧ StablyAssociated A G) (hμ : ∀ (j : J), ∃ (I : MonotoneInvariant P), I.μ (Q j).snd < I.μ G) : ¬inverseInU

Theorem 3.4 (skeleton). Let Q : J → (square matrices) be the family Σ and G an atomic factor of H. The proposition inverseInU stands for "H⁻¹ has entries in U_Σ". The hypothesis hloc is the combined content of the matrix localization lemma (Lemma 3.1), of the complete factorization of Q and of Cohn's Cor. 0.5.5 (not formalized; see the module docstring). If every Q j has a monotone invariant μ_Q with μ_Q (Q j) < μ_Q G, then ¬ inverseInU.

Example (b): the corank at a representation

def ThreeAxes.Criterion.evalHom {P : Type u_1} [Ring P] {K : Type u_2} [Field K] {m : ℕ} (Θ : P →+* Matrix (Fin m) (Fin m) K) (ι : Type) [Fintype ι] [DecidableEq ι] : Matrix ι ι P →+* Matrix (ι × Fin m) (ι × Fin m) K

The evaluation F ↦ F^Θ, an ι × Fin m square matrix over K.

Equations

• ThreeAxes.Criterion.evalHom Θ ι = (Matrix.compRingEquiv ι (Fin m) K).toRingHom.comp Θ.mapMatrix

theorem ThreeAxes.Criterion.evalHom_apply {P : Type u_1} [Ring P] {K : Type u_2} [Field K] {m : ℕ} (Θ : P →+* Matrix (Fin m) (Fin m) K) {ι : Type} [Fintype ι] [DecidableEq ι] (F : Matrix ι ι P) (i j : ι) (a b : Fin m) : (evalHom Θ ι) F (i, a) (j, b) = Θ (F i j) a b

noncomputable def ThreeAxes.Criterion.corankAt {P : Type u_1} [Ring P] {K : Type u_2} [Field K] {m : ℕ} (Θ : P →+* Matrix (Fin m) (Fin m) K) {ι : Type} [Fintype ι] [DecidableEq ι] (F : Matrix ι ι P) : ℕ

corank F^Θ = #rows − rank F^Θ.

Equations

• ThreeAxes.Criterion.corankAt Θ F = Fintype.card (ι × Fin m) - ((ThreeAxes.Criterion.evalHom Θ ι) F).rank

theorem ThreeAxes.Criterion.evalHom_reindex {P : Type u_1} [Ring P] {K : Type u_2} [Field K] {m : ℕ} (Θ : P →+* Matrix (Fin m) (Fin m) K) {ι ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] (e : ι ≃ ι') (F : Matrix ι ι P) : (evalHom Θ ι') ((Matrix.reindex e e) F) = (Matrix.reindex (e.prodCongr (Equiv.refl (Fin m))) (e.prodCongr (Equiv.refl (Fin m)))) ((evalHom Θ ι) F)

theorem ThreeAxes.Criterion.evalHom_fromBlocks {P : Type u_1} [Ring P] {K : Type u_2} [Field K] {m : ℕ} (Θ : P →+* Matrix (Fin m) (Fin m) K) {ι : Type} [Fintype ι] [DecidableEq ι] (p : ℕ) (F : Matrix ι ι P) : (evalHom Θ (ι ⊕ Fin p)) (Matrix.fromBlocks F 0 0 1) = (Matrix.reindex (Equiv.sumProdDistrib ι (Fin p) (Fin m)).symm (Equiv.sumProdDistrib ι (Fin p) (Fin m)).symm) (Matrix.fromBlocks ((evalHom Θ ι) F) 0 0 1)

theorem ThreeAxes.Criterion.rank_fromBlocks_one {K : Type u_2} [Field K] {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq κ] (A : Matrix ι ι K) : (Matrix.fromBlocks A 0 0 1).rank = A.rank + Fintype.card κ

noncomputable def ThreeAxes.Criterion.corankInvariant {P : Type u_1} [Ring P] {K : Type u_2} [Field K] {m : ℕ} (Θ : P →+* Matrix (Fin m) (Fin m) K) : MonotoneInvariant P

Example (b). The corank at a representation Θ : P → M_m(K) is a monotone invariant.

Equations

• One or more equations did not get rendered due to their size.

theorem ThreeAxes.Criterion.corankInvariant_μ {P : Type u_1} [Ring P] {K : Type u_2} [Field K] {m : ℕ} (Θ : P →+* Matrix (Fin m) (Fin m) K) {ι : Type} [Fintype ι] [DecidableEq ι] (F : Matrix ι ι P) : (corankInvariant Θ).μ F = ↑(corankAt Θ F)