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.

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

theorem Algebra.EssFiniteType.cond {R : Type u_1} {S : Type u_2} : ∀ {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S} [self : Algebra.EssFiniteType R S], ∃ (s : Finset S), IsLocalization (Submonoid.comap (algebraMap (↥(Algebra.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 : Algebra.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] [Algebra.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] [Algebra.EssFiniteType R S] : Algebra.adjoin R {x : ↥(Algebra.EssFiniteType.subalgebra R S) | ↑x ∈ Algebra.EssFiniteType.finset R S} = ⊤

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

Equations

• ⋯ = ⋯

noncomputable def Algebra.EssFiniteType.submonoid (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] : Submonoid ↥(Algebra.EssFiniteType.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 : Algebra.EssFiniteType R S] : IsLocalization (Algebra.EssFiniteType.submonoid R S) S

Equations

• ⋯ = ⋯

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 (↥(Algebra.adjoin R ↑σ)) S) (IsUnit.submonoid S)) S ↔ ∀ (s : S), ∃ t ∈ Algebra.adjoin R ↑σ, IsUnit t ∧ s * t ∈ Algebra.adjoin R ↑σ

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

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

Equations

• ⋯ = ⋯

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] : Algebra.EssFiniteType R S

theorem Algebra.EssFiniteType.of_id (R : Type u_1) [CommRing R] : Algebra.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 ∈ Algebra.adjoin S τ) : ∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ Algebra.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₁ : Algebra.EssFiniteType R S] [h₂ : Algebra.EssFiniteType S T] : Algebra.EssFiniteType R T

theorem Algebra.essFiniteType_iff_exists_subalgebra (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : Algebra.EssFiniteType R S ↔ ∃ (S₀ : Subalgebra R S) (M : Submonoid ↥S₀), Algebra.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 : Algebra.EssFiniteType R S] : Algebra.EssFiniteType T (TensorProduct R T S)

Equations

• ⋯ = ⋯

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 : Algebra.EssFiniteType R T] : Algebra.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] [Algebra.EssFiniteType R S] : Algebra.EssFiniteType R T ↔ Algebra.EssFiniteType S 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] [Algebra.EssFiniteType R S] (f : S →ₐ[R] T) (g : S →ₐ[R] T) (H : ∀ s ∈ Algebra.EssFiniteType.finset R S, f s = g s) : f = g