# 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.

source
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 (↥(adjoin R ↑s)) S) (IsUnit.submonoid S)) S

Instances

source
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

Instances For

source
@[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)

Instances For

source
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} = ⊤
source
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)
source
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)

Instances For

source
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
source
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 ↑σ
source
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 ↑σ
source
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
source
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
source
theorem Algebra.EssFiniteType.of_id (R : Type u_1) [CommRing R] :
EssFiniteType R R
source
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 τ
source
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
source
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
source
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)
source
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
source
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
source
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)
source
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)
source
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
source
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

Instances For

source
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

Instances For

source
theorem RingHom.FiniteType.essFiniteType {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.FiniteType) :
f.EssFiniteType
source
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₂