Theorems · Theorem · commutative algebra

Algebra.Presentation.relation_comp_localizationAway_inl

∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [inst_6 : IsScalarTower R S T]
  (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Presentation R S ι σ),
  P.σ (-1) = -1 →
    P.σ 0 = 0 →
      ∀ (r : Unit),
        ((Algebra.Presentation.localizationAway T g).comp P).relation (Sum.inl r) =
          (MvPolynomial.rename Sum.inr) (P.σ g) * MvPolynomial.X (Sum.inl ()) - 1

The composition of a presentation P with a localization away from an element has the form R[Xᵢ, Y]/(fⱼ, (P.σ g) Y - 1), if the chosen section of P preserves -1 and 0. Note: If S is non-trivial, we can ensure this by only modifying P.σ.

Defined in

Mathlib.RingTheory.Extension.Presentation.Basic

Cited by

0 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTowerIsLocalization.Away