Algebra.exists_monoidHom_algebraMap_eq_norm_of_isIntegrallyClosed
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.AlgebraExistsMonoidHomAlgebraMap
universe u v w w'Lean source · statement
theorem _root_.Algebra.exists_monoidHom_algebraMap_eq_norm_of_isIntegrallyClosed
{A : Type u} {B : Type v} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B]
[Algebra A B]
[Algebra.IsIntegral A B]
(K : Type w) (L : Type w') [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] :
∃ N : B →* A, ∀ b : B, algebraMap A K (N b) = Algebra.norm K (algebraMap B L b)