Algebra.FinitePresentation.equiv
theorem Algebra.FinitePresentation.equiv :
∀ {R : Type w₁} {A : Type w₂} {B : Type w₃} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
[inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra.FinitePresentation R A],
(A ≃ₐ[R] B) → Algebra.FinitePresentation R B
The theorem `Algebra.FinitePresentation.equiv` states that for all types `R`, `A`, and `B`, where `R` is a commutative ring, `A` and `B` are rings and `A` and `B` are algebras over `R`, if `A` is a finitely presented algebra, then `B` is also a finitely presented algebra, given there exists an algebra isomorphism from `A` to `B`. In other words, if we have an algebra that is the quotient of a polynomial ring in `n` variables by a finitely generated ideal (i.e., it's finitely presented), and if we have an isomorphism (equivalence) between this algebra and another, then the second algebra is also finitely presented.
More concisely: If `R` is a commutative ring, `A` and `B` are `R`-algebras with `A` finitely presented and there exists an algebra isomorphism from `A` to `B`, then `B` is also finitely presented.
|
Algebra.FinitePresentation.of_finiteType
theorem Algebra.FinitePresentation.of_finiteType :
∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
[inst_3 : IsNoetherianRing R], Algebra.FiniteType R A ↔ Algebra.FinitePresentation R A
The theorem states that for any commutative ring `R` and any ring `A` which is an `R`-algebra, if `R` is a Noetherian ring, then `A` is finitely generated as an `R`-algebra if and only if `A` is finitely presented as an `R`-algebra. Here, a Noetherian ring is a ring that satisfies the ascending chain condition on ideals, i.e., there does not exist an infinite strictly increasing sequence of ideals. An `R`-algebra `A` is finitely generated if there is a finite set of elements of `A` such that every element of `A` is a polynomial in these elements with coefficients in `R`. It is finitely presented if, in addition, the relations between these generators can be described by a finite set of polynomials.
More concisely: A commutative Noetherian ring `R`'s algebra `A` is finitely generated if and only if it is finitely presented.
|
Algebra.FinitePresentation.mvPolynomial_of_finitePresentation
theorem Algebra.FinitePresentation.mvPolynomial_of_finitePresentation :
∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
[inst_3 : Algebra.FinitePresentation R A] (ι : Type v) [inst_4 : Finite ι],
Algebra.FinitePresentation R (MvPolynomial ι A)
This theorem states that if `A` is a finitely presented `R`-algebra, then the multivariate polynomial `MvPolynomial (Fin n) A` with `n` variables and coefficients in `A`, is also finitely presented as an `R`-algebra. Here, `R` and `A` are commutative rings and `A` is an `R`-algebra. The theorem also requires `ι` to be a finite type, which suggests that the set of variables is finite. Essentially, the theorem ensures that the property of being finitely presented is preserved when we consider the ring of multivariate polynomials with coefficients in a finitely presented algebra.
More concisely: If `R` is a commutative ring, `A` is a finitely presented `R`-algebra, and `ι` is a finite type, then the multivariate polynomial algebra `MvPolynomial (Fin n) A` over `A` with `n` variables is also a finitely presented `R`-algebra.
|
Algebra.FinitePresentation.trans
theorem Algebra.FinitePresentation.trans :
∀ (R : Type w₁) (A : Type w₂) (B : Type w₃) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
[inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [inst_6 : IsScalarTower R A B]
[inst_7 : Algebra.FinitePresentation R A] [inst_8 : Algebra.FinitePresentation A B],
Algebra.FinitePresentation R B
This theorem states that if `A` is an `R`-algebra and `B` is an `A`-algebra, and both `A` and `B` are finitely presented, then `B` is also finitely presented as an `R`-algebra. Here, `R`, `A`, and `B` are types representing commutative rings, and an `R`-algebra is a ring that is also an `R`-module such that the multiplication in the ring is compatible with the `R`-module structure. 'Finitely presented' typically means that the structure can be expressed in terms of a finite number of generators and relations.
More concisely: If `A` is a finitely presented `R`-algebra and `B` is an `A`-algebra that is also finitely presented as an `A`-algebra, then `B` is a finitely presented `R`-algebra.
|
Algebra.FinitePresentation.ker_fg_of_mvPolynomial
theorem Algebra.FinitePresentation.ker_fg_of_mvPolynomial :
∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {n : ℕ}
(f : MvPolynomial (Fin n) R →ₐ[R] A),
Function.Surjective ⇑f → ∀ [inst_3 : Algebra.FinitePresentation R A], (RingHom.ker f.toRingHom).FG
This theorem, `Algebra.FinitePresentation.ker_fg_of_mvPolynomial`, states that for any commutative ring `R`, another commutative ring `A`, a number `n`, and a function `f` that is a homomorphism from the multivariate polynomial ring with `n` indeterminates over `R` to `A`, if `f` is surjective (meaning that every element of `A` is the image of some element in the multivariate polynomial ring under `f`), then if `A` is a finitely presented `R`-algebra, the kernel of the ring homomorphism `f` is finitely generated as an ideal of `R`. In other words, every element in the kernel can be written as a finite `R`-linear combination of some fixed set of elements in the kernel.
More concisely: If `R` is a commutative ring, `A` is a commutative and finitely presented `R`-algebra, and `f` is a surjective homomorphism from the multivariate polynomial ring over `R` to `A`, then the kernel of `f` is a finitely generated ideal of `R`.
|
Algebra.FinitePresentation.of_surjective
theorem Algebra.FinitePresentation.of_surjective :
∀ {R : Type w₁} {A : Type w₂} {B : Type w₃} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
[inst_3 : CommRing B] [inst_4 : Algebra R B] {f : A →ₐ[R] B},
Function.Surjective ⇑f →
(RingHom.ker f.toRingHom).FG → ∀ [inst_5 : Algebra.FinitePresentation R A], Algebra.FinitePresentation R B
The theorem `Algebra.FinitePresentation.of_surjective` states that if we have a surjective algebra homomorphism `f` from an algebra `A` over a commutative ring `R` to another algebra `B` over the same ring, and if the kernel of `f` is finitely generated, and `A` is a finitely presented algebra, then `B` is also a finitely presented algebra.
In other words, under these conditions, if `A` can be described by a finite number of generators and relations, then so can `B`. This theorem is a statement about preservation of a certain finiteness property under surjective algebra homomorphisms.
More concisely: If `f` is a surjective algebra homomorphism from the finitely presented algebra `A` over a commutative ring `R` to `B`, and the kernel of `f` is finitely generated, then `B` is also a finitely presented algebra.
|
Algebra.FinitePresentation.quotient
theorem Algebra.FinitePresentation.quotient :
∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I : Ideal A},
I.FG → ∀ [inst_3 : Algebra.FinitePresentation R A], Algebra.FinitePresentation R (A ⧸ I)
The theorem `Algebra.FinitePresentation.quotient` states that for any commutative ring `R` and any commutative ring `A` with an algebra structure over `R`, and any ideal `I` of `A`, if `I` is a finitely generated ideal and `A` is a finitely presented `R`-algebra, then the quotient ring `A/I` is also a finitely presented `R`-algebra. It says that the property of being finitely presented is preserved when taking quotients by finitely generated ideals.
More concisely: If `R` is a commutative ring, `A` is a commutative `R`-algebra that is finitely presented, and `I` is a finitely generated ideal of `A`, then `A/I` is also a finitely presented `R`-algebra.
|
Algebra.FinitePresentation.iff_quotient_mvPolynomial'
theorem Algebra.FinitePresentation.iff_quotient_mvPolynomial' :
∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
Algebra.FinitePresentation R A ↔ ∃ ι x f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
This theorem states that an algebra is finitely presented if and only if it can be represented as a quotient of a polynomial ring, where the variables of the polynomial ring are indexed by a finite type, and the quotient is defined by a finitely generated ideal. The proof involves finding an index set `ι`, a specific element `x`, and a function `f` such that the function `f` is surjective, meaning every element in the target set is the image of some element in the domain, and the kernel (the set of elements in the domain that map to the zero element in the target) of the function when considered as a ring homomorphism is a finitely-generated ideal.
More concisely: A commutative ring is finitely presented if and only if it is isomorphic to the quotient of a polynomial ring over a finite type by a finitely generated ideal.
|
Algebra.FinitePresentation.ker_fG_of_surjective
theorem Algebra.FinitePresentation.ker_fG_of_surjective :
∀ {R : Type w₁} {A : Type w₂} {B : Type w₃} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
[inst_3 : CommRing B] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
Function.Surjective ⇑f →
∀ [inst_5 : Algebra.FinitePresentation R A] [inst_6 : Algebra.FinitePresentation R B],
(RingHom.ker f.toRingHom).FG
The theorem `Algebra.FinitePresentation.ker_fG_of_surjective` states that if there is a surjective function `f` from a finitely presented `R`-algebra `A` to another finitely presented `R`-algebra `B`, then the kernel of `f` is a finitely generated ideal of `A`. Here, `f` is an algebra homomorphism, `R` is a commutative ring, and `A` and `B` are `R`-algebras. The function is surjective, meaning that for every element in `B`, there's an element in `A` such that `f` sends the element in `A` to the one in `B`. The kernel of `f` is the set of all elements in `A` that `f` sends to the zero element in `B`. This kernel is an ideal of `A`, and this theorem states that it is finitely generated, or equivalently, that it can be created by taking finite linear combinations of a finite set of generators.
More concisely: If `f` is a surjective homomorphism from the finitely presented `R`-algebra `A` to the finitely presented `R`-algebra `B`, then the kernel of `f` is a finitely generated ideal of `A`.
|