structure GoodPotionIngredient {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] (𝒜 : ι → Submodule R₀ A) [DecidableEq ι] [GradedAlgebra 𝒜] extends HomogeneousSubmonoid 𝒜 : Type u

• carrier : Set A
• mul_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• homogeneous_gen : ∃ (s : Set A), self.toSubmonoid = Submonoid.closure s ∧ ∀ x ∈ s, SetLike.Homogeneous 𝒜 x
• relevant : self.IsRelevant
• fg : self.FG

theorem GoodPotionIngredient.toHomogeneousSubmonoid_inj {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] : Function.Injective GoodPotionIngredient.toHomogeneousSubmonoid

noncomputable instance GoodPotionIngredient.instMul {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] : Mul (GoodPotionIngredient 𝒜)

Equations

• GoodPotionIngredient.instMul = { mul := fun (x y : GoodPotionIngredient 𝒜) => { toHomogeneousSubmonoid := x.toHomogeneousSubmonoid * y.toHomogeneousSubmonoid, relevant := ⋯, fg := ⋯ } }

noncomputable instance GoodPotionIngredient.instSemigroup {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] : Semigroup (GoodPotionIngredient 𝒜)

Equations

• GoodPotionIngredient.instSemigroup = Semigroup.mk ⋯

@[simp]

theorem GoodPotionIngredient.mul_toHomogeneousSubmonoid {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (x y : GoodPotionIngredient 𝒜) : (x * y).toHomogeneousSubmonoid = x.toHomogeneousSubmonoid * y.toHomogeneousSubmonoid

noncomputable instance GoodPotionIngredient.instCommSemigroup {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] : CommSemigroup (GoodPotionIngredient 𝒜)

Equations

• GoodPotionIngredient.instCommSemigroup = CommSemigroup.mk ⋯

noncomputable def GoodPotionIngredient.map {ι R₀ A B : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] [CommRing B] [Algebra R₀ B] {ℬ : ι → Submodule R₀ B} [GradedAlgebra ℬ] (Φ : GradedRingHom 𝒜 ℬ) (x : GoodPotionIngredient 𝒜) : GoodPotionIngredient ℬ

Equations

• GoodPotionIngredient.map Φ x = { toHomogeneousSubmonoid := HomogeneousSubmonoid.map Φ x.toHomogeneousSubmonoid, relevant := ⋯, fg := ⋯ }

instance GoodPotionIngredient.isOpenImmersion {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (S T : GoodPotionIngredient 𝒜) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (S.potionToMul T.toHomogeneousSubmonoid)))

noncomputable instance GoodPotionIngredient.instAlgebraPotionHMul {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (S T : GoodPotionIngredient 𝒜) : Algebra S.Potion (S * T).Potion

Equations

• S.instAlgebraPotionHMul T = (S.potionToMul T.toHomogeneousSubmonoid).toAlgebra

noncomputable instance GoodPotionIngredient.instAlgebra₃ {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) : Algebra S.Potion (R * S * T).Potion

Equations

• R.instAlgebra₃ S T = ((HomogeneousSubmonoid.potionEquiv ⋯).toRingHom.comp (S.potionToMul (R.toHomogeneousSubmonoid * T.toHomogeneousSubmonoid))).toAlgebra

@[simp]

theorem GoodPotionIngredient.instAlgebra₃_algebraMap_eq {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) : algebraMap S.Potion (R * S * T).Potion = (HomogeneousSubmonoid.potionEquiv ⋯).toRingHom.comp (S.potionToMul (R.toHomogeneousSubmonoid * T.toHomogeneousSubmonoid))

noncomputable def GoodPotionIngredient.mixingAux₀ {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] {R S T : GoodPotionIngredient 𝒜} (R' : S.PotionGen R.toHomogeneousSubmonoid) (T' : S.PotionGen T.toHomogeneousSubmonoid) : TensorProduct S.Potion (S * T).Potion (S * R).Potion ≃ₐ[S.Potion] TensorProduct S.Potion (Localization T'.genSubmonoid) (Localization R'.genSubmonoid)

Equations

• GoodPotionIngredient.mixingAux₀ R' T' = Algebra.TensorProduct.congr (HomogeneousSubmonoid.localizationAlgEquivPotion T').symm (HomogeneousSubmonoid.localizationAlgEquivPotion R').symm

noncomputable def GoodPotionIngredient.mixingAux₁ {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] {R S T : GoodPotionIngredient 𝒜} (R' : S.PotionGen R.toHomogeneousSubmonoid) (T' : S.PotionGen T.toHomogeneousSubmonoid) : TensorProduct S.Potion (Localization T'.genSubmonoid) (Localization R'.genSubmonoid) ≃ₐ[S.Potion] Localization (T'.genSubmonoid * R'.genSubmonoid)

Equations

• GoodPotionIngredient.mixingAux₁ R' T' = (Localization.mulEquivTensor T'.genSubmonoid R'.genSubmonoid).symm

noncomputable def GoodPotionIngredient.mixingAux₂ {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] {R S T : GoodPotionIngredient 𝒜} (R' : S.PotionGen R.toHomogeneousSubmonoid) (T' : S.PotionGen T.toHomogeneousSubmonoid) : Localization (T'.genSubmonoid * R'.genSubmonoid) ≃ₐ[S.Potion] Localization (T'.disjUnion R').genSubmonoid

Equations

• GoodPotionIngredient.mixingAux₂ R' T' = Localization.equivEq ⋯

noncomputable def GoodPotionIngredient.mixingAux₃ {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] {R S T : GoodPotionIngredient 𝒜} (R' : S.PotionGen R.toHomogeneousSubmonoid) (T' : S.PotionGen T.toHomogeneousSubmonoid) : Localization (T'.disjUnion R').genSubmonoid ≃ₐ[S.Potion] (S * (T * R)).Potion

Equations

• GoodPotionIngredient.mixingAux₃ R' T' = HomogeneousSubmonoid.localizationAlgEquivPotion (T'.disjUnion R')

noncomputable def GoodPotionIngredient.mixingAux₄ {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) : (S * (T * R)).Potion ≃ₐ[S.Potion] (R * S * T).Potion

Equations

• R.mixingAux₄ S T = AlgEquiv.ofRingEquiv ⋯

noncomputable def GoodPotionIngredient.mixing {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] {R S T : GoodPotionIngredient 𝒜} (R' : S.PotionGen R.toHomogeneousSubmonoid) (T' : S.PotionGen T.toHomogeneousSubmonoid) : TensorProduct S.Potion (S * T).Potion (S * R).Potion ≃ₐ[S.Potion] (R * S * T).Potion

Equations

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

theorem GoodPotionIngredient.mixing_left {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) (R' : S.PotionGen R.toHomogeneousSubmonoid) (T' : S.PotionGen T.toHomogeneousSubmonoid) (x : (S * T).Potion) : (GoodPotionIngredient.mixing R' T') (x ⊗ₜ[S.Potion] 1) = (HomogeneousSubmonoid.potionEquiv ⋯) (((S * T).potionToMul R.toHomogeneousSubmonoid) x)

theorem GoodPotionIngredient.mixing_right {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) (R' : S.PotionGen R.toHomogeneousSubmonoid) (T' : S.PotionGen T.toHomogeneousSubmonoid) (x : (S * R).Potion) : (GoodPotionIngredient.mixing R' T') (1 ⊗ₜ[S.Potion] x) = (HomogeneousSubmonoid.potionEquiv ⋯) (((S * R).potionToMul T.toHomogeneousSubmonoid) x)

noncomputable def GoodPotionIngredient.t'Aux₀ {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) : TensorProduct S.Potion (S * T).Potion (S * R).Potion ≃+* (R * S * T).Potion

Equations

• R.t'Aux₀ S T = ↑(GoodPotionIngredient.mixing (HomogeneousSubmonoid.finitePotionGen ⋯ ⋯) (HomogeneousSubmonoid.finitePotionGen ⋯ ⋯))

@[simp]

theorem GoodPotionIngredient.t'Aux₀_SR {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) (x : (S * R).Potion) : (R.t'Aux₀ S T) (1 ⊗ₜ[S.Potion] x) = (HomogeneousSubmonoid.potionEquiv ⋯) (((S * R).potionToMul T.toHomogeneousSubmonoid) x)

noncomputable def GoodPotionIngredient.t'Aux₁ {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) : TensorProduct R.Potion (R * S).Potion (R * T).Potion ≃+* (R * S * T).Potion

Equations

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

@[simp]

theorem GoodPotionIngredient.t'Aux₁_RS {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) (x : (R * S).Potion) : (R.t'Aux₁ S T) (x ⊗ₜ[R.Potion] 1) = (HomogeneousSubmonoid.potionEquiv ⋯) (((R * S).potionToMul T.toHomogeneousSubmonoid) x)

noncomputable def GoodPotionIngredient.t' {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) : TensorProduct S.Potion (S * T).Potion (S * R).Potion ≃+* TensorProduct R.Potion (R * S).Potion (R * T).Potion

Equations

• R.t' S T = (R.t'Aux₀ S T).trans (R.t'Aux₁ S T).symm

@[simp]

theorem GoodPotionIngredient.t'_apply_SR {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) (x : (S * R).Potion) : (R.t' S T) (1 ⊗ₜ[S.Potion] x) = (HomogeneousSubmonoid.potionEquiv ⋯) x ⊗ₜ[R.Potion] 1

theorem GoodPotionIngredient.t'_cocycle {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) : (T.t' R S).trans ((S.t' T R).trans (R.t' S T)) = RingEquiv.refl (TensorProduct R.Potion (R * S).Potion (R * T).Potion)

theorem GoodPotionIngredient.t'_fac {ι R₀ A : Type u} [AddCommGroup ι] [CommRing R₀] [CommRing A] [Algebra R₀ A] {𝒜 : ι → Submodule R₀ A} [DecidableEq ι] [GradedAlgebra 𝒜] (R S T : GoodPotionIngredient 𝒜) : (R.t' S T).toRingHom.comp Algebra.TensorProduct.includeRight.toRingHom = Algebra.TensorProduct.includeLeftRingHom.comp (HomogeneousSubmonoid.potionEquiv ⋯).toRingHom