Module

Place_exists_sub_algebraMap_mem_maximalIdeal.lean

Nyll.AlgebraicCurves.Places.Place_exists_sub_algebraMap_mem_maximalIdeal

1 declaration indexed from sourceView source ↗

Module documentation

Place exists sub algebra Map mem maximal Ideal

Imports2

Nyll.AlgebraicCurves.Divisors.ClassGroup
Nyll.AlgebraicCurves.Places.Place_deg_eq_one_iff_surjective_algebraMap_residueField

Imported by2

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_degree_eq_sub_one_and_ell_eq_zero
Nyll.AlgebraicCurves.Places.All

theorem

exists_sub_algebraMap_mem_maximalIdeal

L27 ↗

AlgebraicCurve.Place.exists_sub_algebraMap_mem_maximalIdeal

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_sub_algebraMap_mem_maximalIdeal
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Place.exists_sub_algebraMap_mem_maximalIdeal {K F : Type*} [Field K]
  [Field F]
    [Algebra K F] (u : AlgebraicCurve.Place K F) (hdeg : u.deg = 1) (b : u.toValuationSubring) :
    ∃ c : K, b - algebraMap K u.toValuationSubring c
      ∈ IsLocalRing.maximalIdeal u.toValuationSubring

Module documentation

Place exists sub algebra Map mem maximal Ideal

Declarations

exists_sub_algebraMap_mem_maximalIdeal