NYLL
Module

IsLocalRing_hensel_lift_unique.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_hensel_lift_unique
19 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring hensel lift unique

Imports5
Imported by2

Declarations

theorem

kw_ffgc_ramificationIndex_eq_one_of_comap_surjective

L47 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_ramificationIndex_eq_one_of_comap_surjective
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Bridge
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
theorem kw_ffgc_ramificationIndex_eq_one_of_comap_surjective
    (hsurj : Function.Surjective (kw_ffgc_adicCompletionComap F W)) :
    W.ramificationIndex F = 1
theorem

kw_ffgc_hensel_lift_unique_port

L76 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.kw_ffgc_hensel_lift_unique_port
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
section HenselUniqueness
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem kw_ffgc_hensel_lift_unique_port {f : Polynomial R} {a b : R}
    (ha : f.IsRoot a) (hb : f.IsRoot b) (hmem : b - a ∈ maximalIdeal R)
    (hunit : IsUnit (f.derivative.eval a)) : a = b
theorem

kw_ffgc_adicCompletionComapIntegers_mem_maximalIdeal

L106 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_adicCompletionComapIntegers_mem_maximalIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section IntegerComap
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
theorem kw_ffgc_adicCompletionComapIntegers_mem_maximalIdeal
    {x : (W.restrict F).adicCompletionIntegers}
    (hx : x ∈ maximalIdeal (W.restrict F).adicCompletionIntegers) :
    kw_ffgc_adicCompletionComapIntegers F W x ∈ maximalIdeal W.adicCompletionIntegers
instance

kw_ffgc_isLocalHom_adicCompletionComapIntegers

L122 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_isLocalHom_adicCompletionComapIntegers
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section IntegerComap
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · full declaration
instance kw_ffgc_isLocalHom_adicCompletionComapIntegers :
    IsLocalHom (kw_ffgc_adicCompletionComapIntegers F W) where
  map_nonunit x hx := by
    by_contra hnu
    exact (IsLocalRing.notMem_maximalIdeal.mpr hx)
      (kw_ffgc_adicCompletionComapIntegers_mem_maximalIdeal F W
        ((IsLocalRing.mem_maximalIdeal x).mpr hnu))
instance

kw_ffgc_isIntegrallyClosed_adicCompletionIntegers

L159 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_isIntegrallyClosed_adicCompletionIntegers
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section CompletionAlgebra
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
instance kw_ffgc_isIntegrallyClosed_adicCompletionIntegers :
    IsIntegrallyClosed (W.restrict F).adicCompletionIntegers
theorem

kw_ffgc_adicCompletionComapIntegers_injective

L165 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_adicCompletionComapIntegers_injective
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section CompletionAlgebra
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
theorem kw_ffgc_adicCompletionComapIntegers_injective :
    Function.Injective (kw_ffgc_adicCompletionComapIntegers F W)
instance

kw_ffgc_isTorsionFree_adicCompletionComapIntegers

L171 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_isTorsionFree_adicCompletionComapIntegers
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section CompletionAlgebra
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
instance kw_ffgc_isTorsionFree_adicCompletionComapIntegers :
    Module.IsTorsionFree (W.restrict F).adicCompletionIntegers W.adicCompletionIntegers
theorem

kw_ffgc_valued_coe_irreducible_adicCompletionIntegers

L184 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_valued_coe_irreducible_adicCompletionIntegers
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section IrreducibleValuation
open WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)
Lean source · statement
theorem kw_ffgc_valued_coe_irreducible_adicCompletionIntegers
    {π : V.adicCompletionIntegers} (hπ : Irreducible π) :
    Valued.v (π : V.adicCompletion) = exp (-1 : ℤ)
theorem

kw_ffgc_norm_adicCompletion_eq

L234 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_norm_adicCompletion_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section SpectralSetup
open scoped Valued NNReal WithZero
open WithZeroMulInt Valuation.IsRankOneDiscrete
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)
Lean source · full declaration
theorem kw_ffgc_norm_adicCompletion_eq (x : V.adicCompletion) :
    letI := kw_ffgc_rankOne_adicCompletion V
    ‖x‖ = (WithZeroMulInt.toNNReal (two_ne_zero) (Valued.v x) : ℝ) := by
  let := kw_ffgc_rankOne_adicCompletion V
  have h := valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective
    (V.heightOneSpectrum.valuedAdicCompletion_surjective F) x
  simp only [Valued.toNormedField.norm_def, Valuation.RankOne.hom]
  rw [← h]; rfl
theorem

kw_ffgc_absoluteValue_extends

L255 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_absoluteValue_extends
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section AbsoluteValue
open scoped Valued NNReal WithZero
open WithZeroMulInt Valuation.IsRankOneDiscrete
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · full declaration
theorem kw_ffgc_absoluteValue_extends (c : (W.restrict F).adicCompletion) :
    letI := kw_ffgc_rankOne_adicCompletion (W.restrict F)
    kw_ffgc_absoluteValue F W
      (algebraMap (W.restrict F).adicCompletion W.adicCompletion c) = ‖c‖ := by
  let := kw_ffgc_rankOne_adicCompletion (W.restrict F)
  let := kw_ffgc_rankOne_adicCompletion W
  have hr : (0 : ℝ) < (W.ramificationIndex F : ℝ) :=
    Nat.cast_pos.mpr (W.ramificationIndex_pos (F := F))
  change ‖algebraMap (W.restrict F).adicCompletion W.adicCompletion c‖
      ^ ((W.ramificationIndex F : ℝ))⁻¹ = ‖c‖
  rw [kw_ffgc_norm_adicCompletion_eq W, kw_ffgc_norm_adicCompletion_eq (W.restrict F),
    kw_ffgc_algebraMap_adicCompletionComap_eq, kw_ffgc_valued_adicCompletionComap,
    map_pow, NNReal.coe_pow, ← Real.rpow_natCast, ← Real.rpow_mul (NNReal.coe_nonneg _),
    mul_inv_cancel₀ hr.ne', Real.rpow_one]
theorem

kw_ffgc_isIntegral_adicCompletionIntegers_of_algebraic

L280 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_isIntegral_adicCompletionIntegers_of_algebraic
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section IntegralClosure
open scoped Valued NNReal WithZero
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
theorem kw_ffgc_isIntegral_adicCompletionIntegers_of_algebraic
    [Algebra.IsAlgebraic (W.restrict F).adicCompletion W.adicCompletion]
    (x : W.adicCompletionIntegers) :
    IsIntegral (W.restrict F).adicCompletionIntegers x
theorem

kw_ffgc_isIntegralClosure_adicCompletionIntegers

L324 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_isIntegralClosure_adicCompletionIntegers
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section IntegralClosure
open scoped Valued NNReal WithZero
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · full declaration
theorem kw_ffgc_isIntegralClosure_adicCompletionIntegers
    [Algebra.IsAlgebraic (W.restrict F).adicCompletion W.adicCompletion] :
    IsIntegralClosure W.adicCompletionIntegers (W.restrict F).adicCompletionIntegers
      W.adicCompletion where
  algebraMap_injective := Subtype.val_injective
  isIntegral_iff {x} := by
    constructor
    · intro hx
      have hxW : IsIntegral W.adicCompletionIntegers x := hx.tower_top
      have : IsIntegrallyClosed W.adicCompletionIntegers :=
        Valuation.Integers.isIntegrallyClosed
          (HeightOneSpectrum.adicCompletionIntegers.integers
            (K := F') (v := W.heightOneSpectrum))
      exact IsIntegrallyClosed.isIntegral_iff.mp hxW
    · rintro ⟨y, rfl⟩
      exact (kw_ffgc_isIntegral_adicCompletionIntegers_of_algebraic F W y).map
        (IsScalarTower.toAlgHom (W.restrict F).adicCompletionIntegers
          W.adicCompletionIntegers W.adicCompletion)
theorem

kw_ffgc_isClosed_intermediateField_of_finiteDimensional

L353 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_isClosed_intermediateField_of_finiteDimensional
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ClosedAdjoin
open scoped Valued NNReal WithZero
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
theorem kw_ffgc_isClosed_intermediateField_of_finiteDimensional
    (E : IntermediateField (W.restrict F).adicCompletion W.adicCompletion)
    [FiniteDimensional (W.restrict F).adicCompletion E] :
    IsClosed (E : Set W.adicCompletion)
theorem

kw_ffgc_adjoin_adicCompletion_eq_top_of_denseSubset

L362 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_adjoin_adicCompletion_eq_top_of_denseSubset
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ClosedAdjoin
open scoped Valued NNReal WithZero
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
theorem kw_ffgc_adjoin_adicCompletion_eq_top_of_denseSubset {ζ : W.adicCompletion}
    (hint : IsIntegral (W.restrict F).adicCompletion ζ)
    (hsubset : ∀ x : F', algebraMap F' W.adicCompletion x
      ∈ IntermediateField.adjoin (W.restrict F).adicCompletion {ζ}) :
    Algebra.adjoin (W.restrict F).adicCompletion {ζ} = ⊤
instance

kw_ffgc_faithfulSMul_adicCompletionComapIntegers

L389 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_faithfulSMul_adicCompletionComapIntegers
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Bridge
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
instance kw_ffgc_faithfulSMul_adicCompletionComapIntegers :
    FaithfulSMul (W.restrict F).adicCompletionIntegers W.adicCompletionIntegers
theorem

kw_ffgc_finrank_adicCompletion_le

L417 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_finrank_adicCompletion_le
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section FiniteDimensional
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
theorem kw_ffgc_finrank_adicCompletion_le [FiniteDimensional F F'] :
    Module.finrank (W.restrict F).adicCompletion W.adicCompletion ≤ Module.finrank F F'
theorem

kw_ffgc_completionTraceF'_apply

L443 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_completionTraceF'_apply
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section CompletionTrace
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
theorem kw_ffgc_completionTraceF'_apply [FiniteDimensional F F'] (g : F') :
    kw_ffgc_completionTraceF' F W g
      = Algebra.trace (W.restrict F).adicCompletion W.adicCompletion
          (algebraMap F' W.adicCompletion g)
theorem

kw_ffgc_completionTrace_mem_integers

L448 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique.AlgebraicCurve.Place.kw_ffgc_completionTrace_mem_integers
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section CompletionTrace
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
theorem kw_ffgc_completionTrace_mem_integers [FiniteDimensional F F']
    [Algebra.IsSeparable (W.restrict F).adicCompletion W.adicCompletion]
    (x : W.adicCompletion) (hx : x ∈ W.adicCompletionIntegers) :
    kw_ffgc_completionTrace F W x ∈ (W.restrict F).adicCompletionIntegers
theorem

hensel_lift_unique

L470 ↗
IsLocalRing.hensel_lift_unique
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_hensel_lift_unique
open Polynomial IsLocalRing
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open _root_.AlgebraicCurve AlgebraicCurve _root_.AlgebraicCurve.Place AlgebraicCurve.Place
  IsLocalRing WithZero in
Lean source · statement
theorem _root_.IsLocalRing.hensel_lift_unique {R : Type*} [CommRing R] [IsLocalRing R] {f :
  Polynomial R} {a b : R}
    (ha : f.IsRoot a) (hb : f.IsRoot b) (hmem : b - a ∈ IsLocalRing.maximalIdeal R)
    (hunit : IsUnit (f.derivative.eval a)) : a = b

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.