HomogeneousQuotient.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Grading a quotient by a homogeneous ideal

The manuscript uses two integer gradings on a determinant hypersurface. This module constructs the grading on a quotient from the grading on the original algebra; homogeneity of the defining ideal is a proved input, not a new assumption on a headline theorem.

def OAI.StableCoordinate.HomogeneousQuotient.piece line 26
Source documentation
Images of homogeneous pieces in the actual ideal quotient.
```
def piece (i : ι) : Submodule k (A ⧸ I) :=
…
```
def OAI.StableCoordinate.HomogeneousQuotient.pieceMap line 30
Source documentation
The quotient map, restricted to one homogeneous piece.
```
def pieceMap (i : ι) : 𝒜 i →ₗ[k] piece 𝒜 I i :=
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.piece
theorem OAI.StableCoordinate.HomogeneousQuotient.coe_pieceMap line 37
def OAI.StableCoordinate.HomogeneousQuotient.decomposeBefore line 41
Source documentation
Decompose upstairs, then apply the quotient map to every component.
```
def decomposeBefore : A →ₗ[k] ⨁ i, piece 𝒜 I i :=
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.piece
theorem OAI.StableCoordinate.HomogeneousQuotient.decomposeBefore_apply line 45
theorem OAI.StableCoordinate.HomogeneousQuotient.ideal_le_ker_decomposeBefore line 54
Source documentation
Homogeneity is exactly what permits componentwise decomposition to descend.
```
theorem ideal_le_ker_decomposeBefore :
    I.restrictScalars k ≤ LinearMap.ker (decomposeBefore 𝒜 I) := by
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.decomposeBefore
def OAI.StableCoordinate.HomogeneousQuotient.decomposeQuotient line 64
Source documentation
The decomposition map on the quotient.
```
def decomposeQuotient : (A ⧸ I) →ₗ[k] ⨁ i, piece 𝒜 I i where
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.piece
theorem OAI.StableCoordinate.HomogeneousQuotient.decomposeQuotient_mk line 77
theorem OAI.StableCoordinate.HomogeneousQuotient.recompose_decomposeBefore line 82
Source documentation
Recomposition of the descended homogeneous pieces is the quotient map.
```
theorem recompose_decomposeBefore :
    (DirectSum.coeLinearMap (piece 𝒜 I)).comp (decomposeBefore 𝒜 I) =
      (Ideal.Quotient.mkₐ k I).toLinearMap := by
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.piece, OAI.StableCoordinate.HomogeneousQuotient.decomposeBefore
theorem OAI.StableCoordinate.HomogeneousQuotient.recompose_decomposeQuotient line 92
Source documentation
The descended decomposition has the expected left inverse.
```
theorem recompose_decomposeQuotient :
    (DirectSum.coeLinearMap (piece 𝒜 I)).comp (decomposeQuotient 𝒜 I hI) =
      LinearMap.id := by
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.piece, OAI.StableCoordinate.HomogeneousQuotient.decomposeQuotient
theorem OAI.StableCoordinate.HomogeneousQuotient.decomposeQuotient_recompose line 102
Source documentation
The descended decomposition has the expected right inverse.
```
theorem decomposeQuotient_recompose :
    (decomposeQuotient 𝒜 I hI).comp (DirectSum.coeLinearMap (piece 𝒜 I)) =
      LinearMap.id := by
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.decomposeQuotient, OAI.StableCoordinate.HomogeneousQuotient.piece
def OAI.StableCoordinate.HomogeneousQuotient.decomposition line 119
Source documentation
A quotient by a homogeneous ideal has a direct-sum decomposition.
```
def decomposition : DirectSum.Decomposition (piece 𝒜 I) :=
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.piece
instance OAI.StableCoordinate.HomogeneousQuotient.pieceGradedMonoid line 124
Source documentation
Multiplication of homogeneous representatives descends with its degree.
```
instance pieceGradedMonoid : SetLike.GradedMonoid (piece 𝒜 I) where
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.piece
def OAI.StableCoordinate.HomogeneousQuotient.gradedAlgebra line 136
Source documentation
The quotient algebra carries the induced grading, with no restriction on negative degrees or on the grading monoid.
```
def gradedAlgebra : GradedAlgebra (piece 𝒜 I) where
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.piece
theorem OAI.StableCoordinate.HomogeneousQuotient.proj_mk line 142
Source documentation
Homogeneous projections commute with the quotient map.
```
theorem proj_mk (i : ι) (a : A) :
    letI : GradedAlgebra (piece 𝒜 I) := gradedAlgebra 𝒜 I hI
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.piece, OAI.StableCoordinate.HomogeneousQuotient.gradedAlgebra
theorem OAI.StableCoordinate.HomogeneousQuotient.mk_mem_piece line 149
Source documentation
A homogeneous representative gives a homogeneous quotient element.
```
theorem mk_mem_piece {i : ι} {a : A} (ha : a ∈ 𝒜 i) :
    Ideal.Quotient.mk I a ∈ piece 𝒜 I i := ⟨a, ha, rfl⟩
…
```
Mentions: OAI.StableCoordinate.HomogeneousQuotient.piece