structure ReesAlgebra {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) : Type (max u_1 u_2)

• val : DirectSum (ι →₀ ℕ) fun (v : ι →₀ ℕ) => ↥(F ^ v)

theorem ReesAlgebra.ext {A : Type u_1} {inst✝ : CommSemiring A} {ι : Type u_2} {F : ι → Ideal A} {x y : ReesAlgebra F} (val : x.val = y.val) : x = y

noncomputable instance ReesAlgebra.instZero {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) : Zero (ReesAlgebra F)

Equations

• ReesAlgebra.instZero F = { zero := { val := 0 } }

theorem ReesAlgebra.zero_def {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) : 0 = { val := 0 }

noncomputable instance ReesAlgebra.instSMulNat {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) : SMul ℕ (ReesAlgebra F)

Equations

• ReesAlgebra.instSMulNat F = { smul := fun (n : ℕ) (x : ReesAlgebra F) => { val := n • x.val } }

theorem ReesAlgebra.nsmul_def {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) (n : ℕ) (x : ReesAlgebra F) : n • x = { val := n • x.val }

noncomputable instance ReesAlgebra.instAdd {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) : Add (ReesAlgebra F)

Equations

• ReesAlgebra.instAdd F = { add := fun (x y : ReesAlgebra F) => { val := x.val + y.val } }

theorem ReesAlgebra.add_def {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) {x y : ReesAlgebra F} : x + y = { val := x.val + y.val }

theorem ReesAlgebra.add_val {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) {x y : ReesAlgebra F} : (x + y).val = x.val + y.val

theorem ReesAlgebra.injective_val {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) : Function.Injective ReesAlgebra.val

noncomputable instance ReesAlgebra.instAddCommMonoid {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) : AddCommMonoid (ReesAlgebra F)

Equations

• ReesAlgebra.instAddCommMonoid F = Function.Injective.addCommMonoid ReesAlgebra.val ⋯ ⋯ ⋯ ⋯

noncomputable def ReesAlgebra.mul' {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : (DirectSum (ι →₀ ℕ) fun (v : ι →₀ ℕ) => ↥(F ^ v)) →+ (DirectSum (ι →₀ ℕ) fun (v : ι →₀ ℕ) => ↥(F ^ v)) →+ DirectSum (ι →₀ ℕ) fun (v : ι →₀ ℕ) => ↥(F ^ v)

Equations

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

@[simp]

theorem ReesAlgebra.mul'_of_of {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (v w : ι →₀ ℕ) (x : ↥(F ^ v)) (y : ↥(F ^ w)) : (ReesAlgebra.mul' ((DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) x)) ((DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) w) y) = (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) (v + w)) ⟨↑x * ↑y, ⋯⟩

noncomputable instance ReesAlgebra.instMul {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : Mul (ReesAlgebra F)

Equations

• ReesAlgebra.instMul = { mul := fun (x y : ReesAlgebra F) => { val := (ReesAlgebra.mul' x.val) y.val } }

theorem ReesAlgebra.mul_def {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (x y : ReesAlgebra F) : x * y = { val := (ReesAlgebra.mul' x.val) y.val }

theorem ReesAlgebra.mul_val {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (x y : ReesAlgebra F) : (x * y).val = (ReesAlgebra.mul' x.val) y.val

@[simp]

theorem ReesAlgebra.mul_of_of {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (v w : ι →₀ ℕ) (x : ↥(F ^ v)) (y : ↥(F ^ w)) : { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) x } * { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) w) y } = { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) (v + w)) ⟨↑x * ↑y, ⋯⟩ }

noncomputable instance ReesAlgebra.instOne {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : One (ReesAlgebra F)

Equations

• ReesAlgebra.instOne = { one := { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) 0) ⟨1, ⋯⟩ } }

theorem ReesAlgebra.one_def {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : 1 = { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) 0) ⟨1, ⋯⟩ }

theorem ReesAlgebra.one_val {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : ReesAlgebra.val 1 = (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) 0) ⟨1, ⋯⟩

instance ReesAlgebra.instLeftDistribClass {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : LeftDistribClass (ReesAlgebra F)

instance ReesAlgebra.instRightDistribClass {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : RightDistribClass (ReesAlgebra F)

theorem ReesAlgebra.induction_on {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (P : ReesAlgebra F → Prop) (H_zero : P 0) (H_basic : ∀ (v : ι →₀ ℕ) (x : ↥(F ^ v)), P { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) x }) (H_plus : ∀ (x y : ReesAlgebra F), P x → P y → P (x + y)) (x : ReesAlgebra F) : P x

noncomputable instance ReesAlgebra.instSemigroup {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : Semigroup (ReesAlgebra F)

Equations

• ReesAlgebra.instSemigroup = Semigroup.mk ⋯

noncomputable instance ReesAlgebra.instMulOneClass {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : MulOneClass (ReesAlgebra F)

Equations

• ReesAlgebra.instMulOneClass = MulOneClass.mk ⋯ ⋯

noncomputable instance ReesAlgebra.instMonoid {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : Monoid (ReesAlgebra F)

Equations

• ReesAlgebra.instMonoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

noncomputable instance ReesAlgebra.instCommMonoid {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : CommMonoid (ReesAlgebra F)

Equations

• ReesAlgebra.instCommMonoid = CommMonoid.mk ⋯

noncomputable instance ReesAlgebra.instMonoidWithZero {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : MonoidWithZero (ReesAlgebra F)

Equations

• ReesAlgebra.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯

noncomputable instance ReesAlgebra.instCommSemiring {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : CommSemiring (ReesAlgebra F)

Equations

• ReesAlgebra.instCommSemiring = CommSemiring.mk ⋯

noncomputable def ReesAlgebra.algebraMap' {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] : A →+* ReesAlgebra F

Equations

• ReesAlgebra.algebraMap' F = { toFun := fun (a : A) => { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) 0) ⟨a, ⋯⟩ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ReesAlgebra.algebraMap'_apply_val {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] (a : A) : ((ReesAlgebra.algebraMap' F) a).val = (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) 0) ⟨a, ⋯⟩

noncomputable instance ReesAlgebra.instAlgebra {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : Algebra A (ReesAlgebra F)

Equations

• ReesAlgebra.instAlgebra = (ReesAlgebra.algebraMap' F).toAlgebra

theorem ReesAlgebra.algebraMap_eq {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] : algebraMap A (ReesAlgebra F) = ReesAlgebra.algebraMap' F

theorem ReesAlgebra.algebraMap_apply_val {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (a : A) : ((algebraMap A (ReesAlgebra F)) a).val = (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) 0) ⟨a, ⋯⟩

theorem ReesAlgebra.algebraMap'_apply {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (a : A) : (ReesAlgebra.algebraMap' F) a = { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) 0) ⟨a, ⋯⟩ }

theorem ReesAlgebra.smul_of {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (a : A) (v : ι →₀ ℕ) (x : ↥(F ^ v)) : a • { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) x } = { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) (a • x) }

theorem ReesAlgebra.smul_of_val {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (a : A) (v : ι →₀ ℕ) (x : ↥(F ^ v)) : (a • { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) x }).val = (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) (a • x)

theorem ReesAlgebra.smul_val {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (a : A) (x : ReesAlgebra F) : (a • x).val = a • x.val

noncomputable def ReesAlgebra.single {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] (v : ι →₀ ℕ) : ↥(F ^ v) →ₗ[A] ReesAlgebra F

Equations

• ReesAlgebra.single F v = { toFun := fun (x : ↥(F ^ v)) => { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) x }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ReesAlgebra.single_apply_val {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] (v : ι →₀ ℕ) (x : ↥(F ^ v)) : ((ReesAlgebra.single F v) x).val = (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) x

theorem ReesAlgebra.single_def {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} [DecidableEq ι] (v : ι →₀ ℕ) (x : ↥(F ^ v)) : (ReesAlgebra.single F v) x = { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) x }

noncomputable instance ReesAlgebra.instNeg {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) : Neg (ReesAlgebra F)

Equations

• ReesAlgebra.instNeg F = { neg := fun (x : ReesAlgebra F) => { val := -x.val } }

theorem ReesAlgebra.neg_def {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) (x : ReesAlgebra F) : -x = { val := -x.val }

noncomputable instance ReesAlgebra.instSub {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) : Sub (ReesAlgebra F)

Equations

• ReesAlgebra.instSub F = { sub := fun (x y : ReesAlgebra F) => { val := x.val - y.val } }

theorem ReesAlgebra.sub_def {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) (x y : ReesAlgebra F) : x - y = { val := x.val - y.val }

noncomputable instance ReesAlgebra.instSMulInt {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) : SMul ℤ (ReesAlgebra F)

Equations

• ReesAlgebra.instSMulInt F = { smul := fun (n : ℤ) (x : ReesAlgebra F) => { val := n • x.val } }

theorem ReesAlgebra.zsmul_def {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) (n : ℤ) (x : ReesAlgebra F) : n • x = { val := n • x.val }

noncomputable instance ReesAlgebra.instAddCommGroup {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) : AddCommGroup (ReesAlgebra F)

Equations

• ReesAlgebra.instAddCommGroup F = AddCommGroup.mk ⋯

noncomputable instance ReesAlgebra.instCommRing {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] : CommRing (ReesAlgebra F)

Equations

• ReesAlgebra.instCommRing F = CommRing.mk ⋯

noncomputable def ReesAlgebra.grading {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] (v : ι →₀ ℕ) : Submodule A (ReesAlgebra F)

Equations

• ReesAlgebra.grading F v = LinearMap.range (ReesAlgebra.single F v)

instance ReesAlgebra.instGradedOneFinsuppNatSubmoduleGrading {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] : SetLike.GradedOne (ReesAlgebra.grading F)

instance ReesAlgebra.instGradedMulFinsuppNatSubmoduleGrading {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] : SetLike.GradedMul (ReesAlgebra.grading F)

instance ReesAlgebra.instGradedMonoidFinsuppNatSubmoduleGrading {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] : SetLike.GradedMonoid (ReesAlgebra.grading F)

noncomputable def ReesAlgebra.decomposeAux {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] : (DirectSum (ι →₀ ℕ) fun (v : ι →₀ ℕ) => ↥(F ^ v)) →ₗ[A] DirectSum (ι →₀ ℕ) fun (v : ι →₀ ℕ) => ↥(ReesAlgebra.grading F v)

Equations

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

noncomputable def ReesAlgebra.decompose {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] : ReesAlgebra F →ₗ[A] DirectSum (ι →₀ ℕ) fun (v : ι →₀ ℕ) => ↥(ReesAlgebra.grading F v)

Equations

• ReesAlgebra.decompose F = ReesAlgebra.decomposeAux F ∘ₗ { toFun := ReesAlgebra.val, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ReesAlgebra.decompose_single {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] (v : ι →₀ ℕ) (x : ↥(F ^ v)) : (ReesAlgebra.decompose F) ((ReesAlgebra.single F v) x) = (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(ReesAlgebra.grading F v)) v) ⟨(ReesAlgebra.single F v) x, ⋯⟩

@[simp]

theorem ReesAlgebra.decompose_val_of {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] (v : ι →₀ ℕ) (x : ↥(F ^ v)) : (ReesAlgebra.decompose F) { val := (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(F ^ v)) v) x } = (DirectSum.of (fun (v : ι →₀ ℕ) => ↥(ReesAlgebra.grading F v)) v) ⟨(ReesAlgebra.single F v) x, ⋯⟩

noncomputable instance ReesAlgebra.instGradedAlgebraFinsuppNatGrading {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] : GradedAlgebra (ReesAlgebra.grading F)

Equations

• ReesAlgebra.instGradedAlgebraFinsuppNatGrading F = GradedRing.mk

noncomputable instance ReesAlgebra.instGradedAlgebraFinsuppIntGradingOfInjectionNatGradingρNatToInt {A : Type u_1} [CommRing A] {ι : Type u_2} (F : ι → Ideal A) [DecidableEq ι] [(i : ι →₀ ℤ) → Decidable (i ∈ Set.range ⇑(ρNatToInt ι))] : GradedAlgebra (gradingOfInjection (ReesAlgebra.grading F) (ρNatToInt ι))

Equations

• ReesAlgebra.instGradedAlgebraFinsuppIntGradingOfInjectionNatGradingρNatToInt F = gradingOfInjection_isGradedAlgebra (ReesAlgebra.grading F) (ρNatToInt ι) ⋯