AlgHom.injective_of_finite_of_isFractionRing
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace AlgHom_injective_of_finite_of_isFractionRing
universe uLean source · statement
theorem _root_.AlgHom.injective_of_finite_of_isFractionRing {k A B K : Type u} [Field k]
[CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A]
[CommRing B] [IsDomain B] [Algebra k B] [Algebra.FiniteType k B]
[Field K] [Algebra k K] [Algebra A K] [IsFractionRing A K] [IsScalarTower k A K]
[Algebra B K] [IsFractionRing B K] [IsScalarTower k B K]
(φ : A →ₐ[k] B) (hφ : φ.toRingHom.Finite) : Function.Injective φ