Nyll.AlgebraicCurves.Valuations.IsAlgClosed_exists_valuationSubring_ringHom_retraction

theorem

exists_valuationSubring_ringHom_retraction

IsAlgClosed.exists_valuationSubring_ringHom_retraction

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.IsAlgClosed_exists_valuationSubring_ringHom_retraction

Lean source · statement

theorem _root_.IsAlgClosed.exists_valuationSubring_ringHom_retraction
    (K K' : Type*) [Field K] [IsAlgClosed K] [Field K'] [Algebra K K'] :
    ∃ (A : ValuationSubring K') (hK : ∀ c : K, algebraMap K K' c ∈ A) (σ : A →+* K),
      RingHom.ker σ = IsLocalRing.maximalIdeal A ∧
      ∀ c : K, σ ⟨algebraMap K K' c, hK c⟩ = c

IsAlgClosed_exists_valuationSubring_ringHom_retraction.lean

Module documentation

Is Alg Closed exists valuation Subring ring Hom retraction

exists_valuationSubring_ringHom_retraction

Module documentation

Is Alg Closed exists valuation Subring ring Hom retraction

Declarations

exists_valuationSubring_ringHom_retraction