Algebra.FinitePresentation is local #
In this file we show that being a finitely presented algebra is local.
Main results #
Algebra.FinitePresentation.of_span_eq_top_target: finite presentation is local on the (algebraic) target
theorem Algebra.FinitePresentation.of_span_eq_top_target_aux {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {A : Type u_3} [CommRing A] [Algebra R A] [FinitePresentation R A] (f : A →ₐ[R] S) (hf : Function.Surjective ⇑f) (t : Finset A) (ht : Ideal.span ↑t = ⊤) (H : ∀ (g : ↥t), FinitePresentation R (Localization.Away (f ↑g))) :
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.
theorem Algebra.FinitePresentation.of_span_eq_top_target {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (s : Set S) (hs : Ideal.span s = ⊤) (h : ∀ i ∈ s, FinitePresentation R (Localization.Away i)) :
Finite-presentation can be checked on a standard covering of the target.
theorem Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type u_3} (s : ι → S) (hs : Ideal.span (Set.range s) = ⊤) (T : ι → Type u_4) [(i : ι) → CommRing (T i)] [(i : ι) → Algebra R (T i)] [(i : ι) → Algebra S (T i)] [∀ (i : ι), IsScalarTower R S (T i)] [∀ (i : ι), IsLocalization.Away (s i) (T i)] [∀ (i : ι), FinitePresentation R (T i)] :
Finite-presentation can be checked on a standard covering of the target.
instance Algebra.FinitePresentation.pi {R : Type u_1} [CommRing R] {ι : Type u_3} [Finite ι] (S : ι → Type u_4) [(i : ι) → CommRing (S i)] [(i : ι) → Algebra R (S i)] [∀ (i : ι), FinitePresentation R (S i)] :
FinitePresentation R ((a : ι) → S a)