Theorems · Theorem · commutative algebra
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 →
∀ [Algebra.FinitePresentation R A] [Algebra.FinitePresentation R B], (RingHom.ker f.toRingHom).FGIf f : A →ₐ[R] B is a surjection between finitely-presented R-algebras, then the kernel of
f is finitely generated.
- Defined in
- Mathlib.RingTheory.FinitePresentation
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Semiringproof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- RingHomstatement · cited by 10,189
- Idealproof · cited by 4,748
- Bot.botproof · cited by 4,720
- AlgHomstatement and proof · cited by 3,236
- MvPolynomialproof · cited by 2,140
- RingHomClass.toRingHomproof · cited by 746
- Ideal.mapproof · cited by 692
- AlgHom.compproof · cited by 501
Cited by7
Results whose statement or proof uses this declaration.
- Module.FinitePresentation.of_finite_of_finitePresentationproof · cited by 2
- Algebra.Generators.exists_presentation_of_basis_cotangentproof · cited by 2
- Algebra.FinitePresentation.of_span_eq_top_target_auxproof · cited by 1
- Algebra.Generators.fg_ker_of_finitePresentationproof · cited by 1
- Algebra.FormallySmooth.of_formallySmooth_residueField_tensorproof · cited by 1
- Algebra.IsStandardEtale.of_surjectiveproof · cited by 1