Contracted.lean`

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Contracted monoid algebras, selectors, and the simplicity criterion.

def OAI.FiniteAlgebraicEnvelopes.Contracted.zeroSupported line 18
Source documentation
The one-dimensional ideal spanned by the absorbing monoid zero.
```
def zeroSupported (f : MonoidAlgebra k H) : Prop := ∀ h : H, h ≠ 0 → f.coeff h = 0
```
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.zeroSupported_iff line 20
def OAI.FiniteAlgebraicEnvelopes.Contracted.zeroIdeal line 33
abbrev OAI.FiniteAlgebraicEnvelopes.Contracted.Algebra line 47
def OAI.FiniteAlgebraicEnvelopes.Contracted.quotient line 49
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.quotient_eq line 51
def OAI.FiniteAlgebraicEnvelopes.Contracted.basis line 59
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.basis_mul line 60
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.basis_zero line 63
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.basis_coeff_zero line 68
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.basis_one line 69
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.basis_identity line 70
instance OAI.FiniteAlgebraicEnvelopes.Contracted.(instance at line 72) line 72
def OAI.FiniteAlgebraicEnvelopes.Contracted.Selectors line 82
Source documentation
Ordered finite selectors, expressed by a finite support and distinguished entry.
```
def Selectors (H : Type*) [MonoidWithZero H] : Prop :=
…
```
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.exists_nonzero_coeff line 87
Source documentation
The quotient retains exactly the nonzero monoid coefficients.
```
theorem exists_nonzero_coeff (f : MonoidAlgebra k H) (hf : quotient k H f ≠ 0) :
    ∃ h : H, h ≠ 0 ∧ f.coeff h ≠ 0 := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.quotient
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.expansion line 97
Source documentation
Expansion in the exact contracted monoid basis.
```
theorem expansion (f : MonoidAlgebra k H) :
    quotient k H f = f.coeff.sum (fun h c => basis k H h c) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.quotient, OAI.FiniteAlgebraicEnvelopes.Contracted.basis
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.sandwich line 103
Source documentation
The selector sandwich extracts a single nonzero coefficient.
```
theorem sandwich (f : MonoidAlgebra k H) (h L R : H)
    (he : L*h*R=1) (hz : ∀ g ∈ f.coeff.support, g ≠ h → L*g*R=0) :
    basis k H L 1 * quotient k H f * basis k H R 1 =
      algebraMap k (Algebra k H) (f.coeff h) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.basis, OAI.FiniteAlgebraicEnvelopes.Contracted.quotient, OAI.FiniteAlgebraicEnvelopes.Contracted.Algebra
def OAI.FiniteAlgebraicEnvelopes.Contracted.coefficient line 119
Source documentation
Coefficients at nonzero monoid elements descend unchanged to the quotient.
```
def coefficient (h : H) (hh : h ≠ 0) : Algebra k H →ₗ[k] k where
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.Algebra
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.coefficient_quotient line 130
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.coefficient_basis line 132
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.coefficient_ext line 137
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.basis_linearIndependent line 144
Source documentation
The actual basis consists precisely of the nonzero monoid elements.
```
theorem basis_linearIndependent :
    LinearIndependent k (fun h : {h : H // h ≠ 0} => basis k H h 1) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.basis
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.basis_spans line 153
def OAI.FiniteAlgebraicEnvelopes.Contracted.monoidBasis line 175
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.monoidBasis_apply line 178
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.kill_zeroSupported line 186
def OAI.FiniteAlgebraicEnvelopes.Contracted.lift line 191
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.lift_quotient line 203
def OAI.FiniteAlgebraicEnvelopes.Contracted.shifted line 212
Source documentation
The shift by c(0), essential because c need not preserve either 0 or 1.
```
def shifted : H →ₙ* Algebra k J where
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.Algebra
def OAI.FiniteAlgebraicEnvelopes.Contracted.shiftedLift line 218
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.shiftedLift_single line 220
def OAI.FiniteAlgebraicEnvelopes.Contracted.embedding line 224
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.embedding_basis line 227
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.coefficient_embedding line 232
Source documentation
Every nonzero coefficient is retained at its distinct new basis element.
```
theorem coefficient_embedding (hc : Function.Injective c) (hz : ∀ h, c h ≠ 0)
    (h : H) (hh : h ≠ 0) (x : Algebra k H) :
    coefficient (c h) (hz h) (embedding (k:=k) c x) = coefficient h hh x := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.Algebra, OAI.FiniteAlgebraicEnvelopes.Contracted.coefficient, OAI.FiniteAlgebraicEnvelopes.Contracted.embedding
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.embedding_injective line 250
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.one_not_mem_range line 258
Source documentation
The unit of B is outside the entire embedded subalgebra, not only different from e.
```
theorem one_not_mem_range [Nontrivial k] [Nontrivial J] (hc : ∀ h, c h ≠ 1) :
    (1 : Algebra k J) ∉ Set.range (embedding (k:=k) c) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.Algebra, OAI.FiniteAlgebraicEnvelopes.Contracted.embedding
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.embedding_one_ne_one line 279
Source documentation
Source support identity e=c(1)−c(0) is proper in the ambient unital algebra.
```
theorem embedding_one_ne_one [Nontrivial k] [Nontrivial J]
    (hc : ∀ h, c h ≠ 1) : embedding (k:=k) c 1 ≠ 1 := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.embedding
def OAI.FiniteAlgebraicEnvelopes.Contracted.map line 293
Source documentation
Zero-preserving unital monoid maps induce unital maps of contracted algebras.
```
def map {J : Type*} [MonoidWithZero J] (c : H →*₀ J) : Algebra k H →ₐ[k] Algebra k J :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.Algebra
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.map_basis line 304
theorem OAI.FiniteAlgebraicEnvelopes.Contracted.simple_of_selectors line 320
Source documentation
The simplicity argument for contracted monoid algebras over any coefficient field.
```
theorem simple_of_selectors (hS : Selectors H) : IsSimpleRing (Algebra K H) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Contracted.Selectors, OAI.FiniteAlgebraicEnvelopes.Contracted.Algebra