HomogeneousQuotientWeight.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

An integral weight coaction on a homogeneous principal quotient

This construction supplies the fiber-weight action for the actual presentation k[a,d,b,c,u]/(ac-bd-1). It works for an arbitrary weighted-homogeneous principal relation and uses genuine quotient algebra homomorphisms. Its hypotheses are construction data, not assumptions added to the principal package.

abbrev OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing line 26
Source documentation
The principal quotient determined by a relation.
```
abbrev QuotientRing (H : MvPolynomial σ k) :=
…
```
def OAI.StableCoordinate.HomogeneousQuotientWeight.generator line 30
Source documentation
The coordinate images in a principal quotient.
```
def generator (H : MvPolynomial σ k) (i : σ) : QuotientRing H :=
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing
theorem OAI.StableCoordinate.HomogeneousQuotientWeight.aeval_variable line 34
theorem OAI.StableCoordinate.HomogeneousQuotientWeight.defining_relation_zero line 44
theorem OAI.StableCoordinate.HomogeneousQuotientWeight.weightedEval_relation_zero line 50
Source documentation
Weighted evaluation annihilates a weighted-homogeneous defining relation.
```
theorem weightedEval_relation_zero (w : σ → ℤ) (H : MvPolynomial σ k) {n : ℤ}
    (hH : H.IsWeightedHomogeneous w n) :
    LaurentWeightObstruction.weightedEval w (generator H) H = 0 := by
…
```
Mentions: OAI.StableCoordinate.LaurentWeightObstruction.weightedEval, OAI.StableCoordinate.HomogeneousQuotientWeight.generator
def OAI.StableCoordinate.HomogeneousQuotientWeight.coaction line 57
Source documentation
The Laurent weight coaction on the principal quotient by a homogeneous relation.
```
def coaction (w : σ → ℤ) (H : MvPolynomial σ k) {n : ℤ}
    (hH : H.IsWeightedHomogeneous w n) :
    QuotientRing H →ₐ[k] LaurentPolynomial (QuotientRing H) :=
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing
theorem OAI.StableCoordinate.HomogeneousQuotientWeight.coaction_mk line 67
theorem OAI.StableCoordinate.HomogeneousQuotientWeight.coaction_variable line 74

theorem OAI.StableCoordinate.HomogeneousQuotientWeight.coaction_mk_of_homogeneous line 83

Source documentation

A homogeneous polynomial representative gives the expected weight identity in the quotient algebra.

theorem coaction_mk_of_homogeneous (w : σ → ℤ) (H : MvPolynomial σ k) {n : ℤ}
    (hH : H.IsWeightedHomogeneous w n) {p : MvPolynomial σ k} {m : ℤ}
    (hp : p.IsWeightedHomogeneous w m) :
    coaction w H hH ((Ideal.Quotient.mkₐ k _ :
      MvPolynomial σ k →ₐ[k] QuotientRing H) p) =
      AddMonoidAlgebra.single m ((Ideal.Quotient.mkₐ k _ :
        MvPolynomial σ k →ₐ[k] QuotientRing H) p) := by
…

Mentions: OAI.StableCoordinate.HomogeneousQuotientWeight.coaction, OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing

theorem OAI.StableCoordinate.HomogeneousQuotientWeight.coeff_coaction_mk line 96

Source documentation

Coefficients of the quotient coaction are the images of polynomial weighted components. In particular, component projection is independent of the chosen representative.

theorem coeff_coaction_mk (w : σ → ℤ) (H : MvPolynomial σ k) {n : ℤ}
    (hH : H.IsWeightedHomogeneous w n) (p : MvPolynomial σ k) (m : ℤ) :
    (coaction w H hH ((Ideal.Quotient.mkₐ k _ :
      MvPolynomial σ k →ₐ[k] QuotientRing H) p)).coeff m =
      (Ideal.Quotient.mkₐ k _ : MvPolynomial σ k →ₐ[k] QuotientRing H)
        (weightedHomogeneousComponent w m p) := by
…

Mentions: OAI.StableCoordinate.HomogeneousQuotientWeight.coaction, OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing

def OAI.StableCoordinate.HomogeneousQuotientWeight.component line 105
Source documentation
A well-defined linear projection to an integral weight in the quotient.
```
def component (w : σ → ℤ) (H : MvPolynomial σ k) {n : ℤ}
    (hH : H.IsWeightedHomogeneous w n) (m : ℤ) :
    QuotientRing H →ₗ[k] QuotientRing H :=
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing
theorem OAI.StableCoordinate.HomogeneousQuotientWeight.component_apply line 112
theorem OAI.StableCoordinate.HomogeneousQuotientWeight.component_mk line 117
def OAI.StableCoordinate.HomogeneousQuotientWeight.piece line 125
Source documentation
The image definition of a weight piece in a homogeneous principal quotient.
```
def piece (w : σ → ℤ) (H : MvPolynomial σ k) (m : ℤ) :
    Submodule k (QuotientRing H) :=
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing
theorem OAI.StableCoordinate.HomogeneousQuotientWeight.component_mem_piece line 131
Source documentation
A projected component belongs to the corresponding image piece.
```
theorem component_mem_piece (w : σ → ℤ) (H : MvPolynomial σ k) {n : ℤ}
    (hH : H.IsWeightedHomogeneous w n) (m : ℤ) (q : QuotientRing H) :
    component w H hH m q ∈ piece w H m := by
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing, OAI.StableCoordinate.HomogeneousQuotientWeight.component, OAI.StableCoordinate.HomogeneousQuotientWeight.piece
theorem OAI.StableCoordinate.HomogeneousQuotientWeight.mem_piece_iff_coaction line 141
Source documentation
Elements of an image piece have the corresponding single-monomial coaction, and conversely the coaction identity detects the image piece.
```
theorem mem_piece_iff_coaction (w : σ → ℤ) (H : MvPolynomial σ k) {n : ℤ}
    (hH : H.IsWeightedHomogeneous w n) (m : ℤ) (q : QuotientRing H) :
    q ∈ piece w H m ↔ coaction w H hH q = AddMonoidAlgebra.single m q := by
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing, OAI.StableCoordinate.HomogeneousQuotientWeight.piece, OAI.StableCoordinate.HomogeneousQuotientWeight.coaction
theorem OAI.StableCoordinate.HomogeneousQuotientWeight.component_of_mem_piece line 156
Source documentation
The quotient projections are identity on their own piece and zero on all other pieces.
```
theorem component_of_mem_piece (w : σ → ℤ) (H : MvPolynomial σ k) {n : ℤ}
    (hH : H.IsWeightedHomogeneous w n) {m : ℤ} {q : QuotientRing H}
    (hq : q ∈ piece w H m) (r : ℤ) :
    component w H hH r q = if r = m then q else 0 := by
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing, OAI.StableCoordinate.HomogeneousQuotientWeight.piece, OAI.StableCoordinate.HomogeneousQuotientWeight.component

theorem OAI.StableCoordinate.HomogeneousQuotientWeight.polynomial_components_commute line 167

Source documentation

Any two polynomial weighted-component projections commute.

theorem polynomial_components_commute (w₁ w₂ : σ → ℤ) (m₁ m₂ : ℤ)
    (p : MvPolynomial σ k) :
    weightedHomogeneousComponent w₁ m₁ (weightedHomogeneousComponent w₂ m₂ p) =
      weightedHomogeneousComponent w₂ m₂ (weightedHomogeneousComponent w₁ m₁ p) := by
…

theorem OAI.StableCoordinate.HomogeneousQuotientWeight.components_commute line 179

Source documentation

Compatible integral gradings descend to compatible component projections on the actual same quotient.

theorem components_commute (w₁ w₂ : σ → ℤ) (H : MvPolynomial σ k) {n₁ n₂ : ℤ}
    (hH₁ : H.IsWeightedHomogeneous w₁ n₁) (hH₂ : H.IsWeightedHomogeneous w₂ n₂)
    (m₁ m₂ : ℤ) (q : QuotientRing H) :
    component w₁ H hH₁ m₁ (component w₂ H hH₂ m₂ q) =
      component w₂ H hH₂ m₂ (component w₁ H hH₁ m₁ q) := by
…

Mentions: OAI.StableCoordinate.HomogeneousQuotientWeight.QuotientRing, OAI.StableCoordinate.HomogeneousQuotientWeight.component