Theorems · Theorem · commutative algebra

Algebra.FinitePresentation.of_span_eq_top_target_aux

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Type u_3}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] [Algebra.FinitePresentation R A] (f : A →ₐ[R] S),
  Function.Surjective ⇑f →
    ∀ (t : Finset A),
      Ideal.span ↑t = ⊤ →
        (∀ (g : ↥t), Algebra.FinitePresentation R (Localization.Away (f ↑g))) → Algebra.FinitePresentation R S

If S is an R-algebra with a surjection from a finitely-presented R-algebra A, such that localized at a spanning set { r } of elements of A, Sᵣ is finitely-presented, then S is finitely presented. This is almost finitePresentation_ofLocalizationSpanTarget. The difference is, that here the set t generates the unit ideal of A, while in the general version, it only generates a quotient of A.

Defined in

Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebra.FinitePresentation