IsLocalRing.mem_range_algebraMap_of_flat_of_isLocalHom
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_mem_range_algebraMap_of_flat_of_isLocalHom
universe u v u' v'Lean source · statement
theorem _root_.IsLocalRing.mem_range_algebraMap_of_flat_of_isLocalHom
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [IsDomain
R] [IsDomain S]
(f : R →+* S) (hf : f.Flat) [IsLocalHom f]
(K : Type u') (L : Type v') [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L]
[IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R K L]
(hcomm : ∀ r : R, algebraMap R L r = algebraMap S L (f r))
(x : K) (hx : algebraMap K L x ∈ (algebraMap S L).range) :
x ∈ (algebraMap R K).range