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)