Essentially of finite type algebras

Main results

• Algebra.EssFiniteType: The class of essentially of finite type algebras. An R-algebra is essentially of finite type if it is the localization of an algebra of finite type.
• Algebra.EssFiniteType.algHom_ext: The algebra homomorphisms out from an algebra essentially of finite type is determined by its values on a finite set.

class Algebra.EssFiniteType (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : Prop

An R-algebra is essentially of finite type if it is the localization of an algebra of finite type. See essFiniteType_iff_exists_subalgebra.

For field extensions, this is equivalent to being finitely generated as a field. See IntermediateField.fg_top_iff.

• cond : ∃ (s : Finset S), IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑s)) S) (IsUnit.submonoid S)) S

noncomputable def Algebra.EssFiniteType.finset (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [h : EssFiniteType R S] : Finset S

Let S be an R-algebra essentially of finite type, this is a choice of a finset s ⊆ S such that S is the localization of R[s].

Equations

• Algebra.EssFiniteType.finset R S = ⋯.choose

@[reducible, inline]

noncomputable abbrev Algebra.EssFiniteType.subalgebra (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [EssFiniteType R S] : Subalgebra R S

A choice of a subalgebra of finite type in an essentially of finite type algebra, such that its localization is the whole ring.

Equations

• Algebra.EssFiniteType.subalgebra R S = Algebra.adjoin R ↑(Algebra.EssFiniteType.finset R S)

theorem Algebra.EssFiniteType.adjoin_mem_finset (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [EssFiniteType R S] : adjoin R {x : ↥(subalgebra R S) | ↑x ∈ finset R S} = ⊤

instance Algebra.instFiniteTypeSubtypeMemSubalgebraSubalgebra (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [EssFiniteType R S] : FiniteType R ↥(EssFiniteType.subalgebra R S)

noncomputable def Algebra.EssFiniteType.submonoid (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [EssFiniteType R S] : Submonoid ↥(subalgebra R S)

A submonoid of EssFiniteType.subalgebra R S, whose localization is the whole algebra S.

Equations

• Algebra.EssFiniteType.submonoid R S = Submonoid.comap (algebraMap (↥(Algebra.EssFiniteType.subalgebra R S)) S) (IsUnit.submonoid S)

instance Algebra.EssFiniteType.isLocalization (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [h : EssFiniteType R S] : IsLocalization (submonoid R S) S

theorem Algebra.essFiniteType_cond_iff (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (σ : Finset S) : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S ↔ ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

theorem Algebra.essFiniteType_iff (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : EssFiniteType R S ↔ ∃ (σ : Finset S), ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

instance Algebra.EssFiniteType.of_finiteType (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] : EssFiniteType R S

theorem Algebra.EssFiniteType.of_isLocalization {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] : EssFiniteType R S

theorem Algebra.EssFiniteType.of_id (R : Type u_1) [CommRing R] : EssFiniteType R R

theorem Algebra.EssFiniteType.aux (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (σ : Subalgebra R S) (hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ) (τ : Set T) (t : T) (ht : t ∈ adjoin S τ) : ∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

theorem Algebra.EssFiniteType.comp (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [h₁ : EssFiniteType R S] [h₂ : EssFiniteType S T] : EssFiniteType R T

theorem Algebra.essFiniteType_iff_exists_subalgebra (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : EssFiniteType R S ↔ ∃ (S₀ : Subalgebra R S) (M : Submonoid ↥S₀), FiniteType R ↥S₀ ∧ IsLocalization M S

instance Algebra.EssFiniteType.baseChange (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [h : EssFiniteType R S] : EssFiniteType T (TensorProduct R T S)

theorem Algebra.EssFiniteType.of_comp (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [h : EssFiniteType R T] : EssFiniteType S T

theorem Algebra.EssFiniteType.comp_iff (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [EssFiniteType R S] : EssFiniteType R T ↔ EssFiniteType S T

instance Algebra.instEssFiniteTypeQuotientIdeal (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [EssFiniteType R S] (I : Ideal S) : EssFiniteType R (S ⧸ I)

instance Algebra.instEssFiniteTypeLocalization (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [EssFiniteType R S] (M : Submonoid S) : EssFiniteType R (Localization M)

theorem Algebra.EssFiniteType.of_surjective {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (f : S →ₐ[R] T) (hf : Function.Surjective ⇑f) [EssFiniteType R S] : EssFiniteType R T

theorem Algebra.EssFiniteType.iff_of_algEquiv {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (f : S ≃ₐ[R] T) : EssFiniteType R S ↔ EssFiniteType R T

theorem Algebra.EssFiniteType.algHom_ext {R : Type u_1} {S : Type u_2} (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [EssFiniteType R S] (f g : S →ₐ[R] T) (H : ∀ s ∈ finset R S, f s = g s) : f = g

def RingHom.EssFiniteType {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) : Prop

A ring hom is essentially of finite type if it is the composition of a localization map and a ring hom of finite type. See Algebra.EssFiniteType.

Equations

• f.EssFiniteType = Algebra.EssFiniteType R S

noncomputable def RingHom.EssFiniteType.finset {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.EssFiniteType) : Finset S

A choice of "essential generators" for a ring hom essentially of finite type. See Algebra.EssFiniteType.ext.

Equations

• hf.finset = Algebra.EssFiniteType.finset R S

theorem RingHom.FiniteType.essFiniteType {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.FiniteType) : f.EssFiniteType

theorem RingHom.EssFiniteType.ext {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} (hf : f.EssFiniteType) {g₁ g₂ : S →+* T} (h₁ : g₁.comp f = g₂.comp f) (h₂ : ∀ x ∈ hf.finset, g₁ x = g₂ x) : g₁ = g₂