NYLL
Module

CompletionTraceSum_of_isSeparable.lean

Nyll.AlgebraicCurves.FunctionFields.CompletionTraceSum_of_isSeparable
44 declarations indexed from sourceView source ↗

Module documentation

CompletionTraceSum of isSeparable

A separable algebraic function-field extension satisfies the completed trace-sum identity, using semilocal completions and ramification and inertia degrees.

Imports4
Imported by3

Declarations

theorem

gapsw7_x3x_trace_pi

L35 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.gapsw7_x3x_trace_pi
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section ProductTrace
open scoped TensorProduct
Lean source · statement
theorem gapsw7_x3x_trace_pi (R : Type*) [CommRing R] {ι : Type*} [Fintype ι]
    (S : ι → Type*) [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)]
    [∀ i, Module.Free R (S i)] [∀ i, Module.Finite R (S i)]
    (x : ∀ i, S i) :
    Algebra.trace R (∀ i, S i) x = ∑ i, Algebra.trace R (S i) (x i)
theorem

gapsw7_x3x_trace_baseChange

L66 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.gapsw7_x3x_trace_baseChange
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section ProductTrace
open scoped TensorProduct
Lean source · statement
theorem gapsw7_x3x_trace_baseChange (R A B : Type*) [CommRing R] [CommRing A]
    [CommRing B] [Algebra R A] [Algebra R B] [Module.Free R B]
    [Module.Finite R B] (b : B) :
    Algebra.trace A (A ⊗[R] B) ((1 : A) ⊗ₜ[R] b)
      = algebraMap R A (Algebra.trace R B b)
theorem

gapsw7_x3x_trace_decomposition_of_prod_iso

L76 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.gapsw7_x3x_trace_decomposition_of_prod_iso
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section ProductTrace
open scoped TensorProduct
Lean source · statement
theorem gapsw7_x3x_trace_decomposition_of_prod_iso (R A B : Type*)
    [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [Module.Free R B] [Module.Finite R B] {ι : Type*} [Fintype ι]
    (S : ι → Type*) [∀ i, CommRing (S i)] [∀ i, Algebra A (S i)]
    [∀ i, Module.Free A (S i)] [∀ i, Module.Finite A (S i)]
    (e : (A ⊗[R] B) ≃ₐ[A] ∀ i, S i) (b : B) :
    algebraMap R A (Algebra.trace R B b)
      = ∑ i, Algebra.trace A (S i) (e ((1 : A) ⊗ₜ[R] b) i)
theorem

kw_ffgc_norm_adicCompletion_eq

L100 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kw_ffgc_norm_adicCompletion_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section SpectralSetup
open Polynomial IsLocalRing IsDedekindDomain
open AlgebraicCurve AlgebraicCurve.Place
open scoped AlgebraicCurve.Place 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

L122 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kw_ffgc_absoluteValue_extends
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section AbsoluteValueIntegralClosure
open Polynomial IsLocalRing IsDedekindDomain
open AlgebraicCurve AlgebraicCurve.Place
open scoped AlgebraicCurve.Place 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

L137 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kw_ffgc_isIntegral_adicCompletionIntegers_of_algebraic
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section AbsoluteValueIntegralClosure
open Polynomial IsLocalRing IsDedekindDomain
open AlgebraicCurve AlgebraicCurve.Place
open scoped AlgebraicCurve.Place 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 · 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

L181 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kw_ffgc_isIntegralClosure_adicCompletionIntegers
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section AbsoluteValueIntegralClosure
open Polynomial IsLocalRing IsDedekindDomain
open AlgebraicCurve AlgebraicCurve.Place
open scoped AlgebraicCurve.Place 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_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_adicCompletionComapIntegers_mem_maximalIdeal

L212 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kw_ffgc_adicCompletionComapIntegers_mem_maximalIdeal
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section IntegerComap
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
open AlgebraicCurve AlgebraicCurve.Place
open scoped AlgebraicCurve.Place
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

L228 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kw_ffgc_isLocalHom_adicCompletionComapIntegers
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section IntegerComap
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
open AlgebraicCurve AlgebraicCurve.Place
open scoped AlgebraicCurve.Place
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))
def

kw_ffgc_residueFieldEquivCompletionResidueField

L247 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kw_ffgc_residueFieldEquivCompletionResidueField
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section ResidueCompletion
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open AlgebraicCurve AlgebraicCurve.Place
open scoped AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)
Lean source · statement
def kw_ffgc_residueFieldEquivCompletionResidueField :
    V.ResidueField ≃+* IsLocalRing.ResidueField V.adicCompletionIntegers
theorem

kw_ffgc_residueFieldEquivCompletionResidueField_residue

L251 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kw_ffgc_residueFieldEquivCompletionResidueField_residue
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section ResidueCompletion
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open AlgebraicCurve AlgebraicCurve.Place
open scoped AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)
Lean source · statement
theorem kw_ffgc_residueFieldEquivCompletionResidueField_residue (a : V.toValuationSubring) :
    kw_ffgc_residueFieldEquivCompletionResidueField V
        (IsLocalRing.residue V.toValuationSubring a)
      = IsLocalRing.residue V.adicCompletionIntegers
          (algebraMap V.toValuationSubring V.adicCompletionIntegers a)
instance

kwF4R1V384a_instAlgebraFiberCompletion

L270 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_instAlgebraFiberCompletion
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section FiberAlgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
Lean source · statement
instance kwF4R1V384a_instAlgebraFiberCompletion (v : Place K E) (w' : v.fiber F) :
    Algebra v.adicCompletion w'.1.adicCompletion
instance

kwF4R1V384a_instIsScalarTowerFiberCompletion

L277 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_instIsScalarTowerFiberCompletion
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section FiberAlgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
Lean source · statement
instance kwF4R1V384a_instIsScalarTowerFiberCompletion (v : Place K E) (w' :
  v.fiber F) :
    IsScalarTower E v.adicCompletion w'.1.adicCompletion
instance

kwF4R1V384a_instFiniteDimensionalFiberCompletion

L288 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_instFiniteDimensionalFiberCompletion
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section FiberAlgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
Lean source · statement
instance kwF4R1V384a_instFiniteDimensionalFiberCompletion [FiniteDimensional E F]
    (v : Place K E) (w' : v.fiber F) :
    FiniteDimensional v.adicCompletion w'.1.adicCompletion
def

kwF4R1V384a_semilocalComponent

L304 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_semilocalComponent
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section SemilocalDiag
variable {K : Type*} (F : Type*) [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
Lean source · statement
def kwF4R1V384a_semilocalComponent (v : Place K E) (w' : v.fiber F) :
    v.adicCompletion ⊗[E] F →ₐ[v.adicCompletion] w'.1.adicCompletion
theorem

kwF4R1V384a_semilocalComponent_tmul

L311 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_semilocalComponent_tmul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section SemilocalDiag
variable {K : Type*} (F : Type*) [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
omit [HasPrincipalDivisors K E] in
Lean source · statement
theorem kwF4R1V384a_semilocalComponent_tmul (v : Place K E) (w' : v.fiber F)
    (c : v.adicCompletion) (g : F) :
    kwF4R1V384a_semilocalComponent F v w' (c ⊗ₜ[E] g)
      = algebraMap v.adicCompletion w'.1.adicCompletion c
          * algebraMap F w'.1.adicCompletion g
def

kwF4R1V384a_semilocalDiag

L320 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_semilocalDiag
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section SemilocalDiag
variable {K : Type*} (F : Type*) [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
Lean source · statement
def kwF4R1V384a_semilocalDiag (v : Place K E) :
    v.adicCompletion ⊗[E] F →ₐ[v.adicCompletion]
      ((w' : v.fiber F) → w'.1.adicCompletion)
theorem

kwF4R1V384a_semilocalDiag_apply

L329 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_semilocalDiag_apply
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section SemilocalDiag
variable {K : Type*} (F : Type*) [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
variable {F}
omit [HasPrincipalDivisors K E] in
Lean source · statement
theorem kwF4R1V384a_semilocalDiag_apply (v : Place K E) (x : v.adicCompletion ⊗[E] F)
    (w' : v.fiber F) :
    kwF4R1V384a_semilocalDiag F v x w' = kwF4R1V384a_semilocalComponent F v w' x
theorem

kwF4R1V384a_semilocalDiag_one_tmul

L334 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_semilocalDiag_one_tmul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section SemilocalDiag
variable {K : Type*} (F : Type*) [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
variable {F}
omit [HasPrincipalDivisors K E] in
Lean source · statement
theorem kwF4R1V384a_semilocalDiag_one_tmul (v : Place K E) (g : F) (w' : v.fiber F) :
    kwF4R1V384a_semilocalDiag F v ((1 : v.adicCompletion) ⊗ₜ[E] g) w'
      = algebraMap F w'.1.adicCompletion g
def

KwF4R1V384aCompletionSemilocalBij

L348 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.KwF4R1V384aCompletionSemilocalBij
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section Mint
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (E : Type*) [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
def KwF4R1V384aCompletionSemilocalBij : Prop
theorem

kwF4R1V384a_completionLinearCombination_surjective

L363 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_completionLinearCombination_surjective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section PerComponentSurjective
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
variable [FiniteDimensional E F]
omit [HasPrincipalDivisors K E] [HasPrincipalDivisors K F] [FiniteDimensional E F] in
Lean source · statement
theorem kwF4R1V384a_completionLinearCombination_surjective
    (w' : Place K F) {ι : Type*} [Fintype ι] (b : Module.Basis ι E F) :
    Function.Surjective (kw_ffgc_completionLinearCombination E w' b)
theorem

kwF4R1V384a_semilocalComponent_surjective

L376 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_semilocalComponent_surjective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section PerComponentSurjective
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
variable [FiniteDimensional E F]
omit [HasPrincipalDivisors K E] in
Lean source · statement
theorem kwF4R1V384a_semilocalComponent_surjective (v : Place K E) (w' : v.fiber F) :
    Function.Surjective (kwF4R1V384a_semilocalComponent F v w')
def

KwF4R1V384aDistinctKernels

L399 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.KwF4R1V384aDistinctKernels
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section SpecificMints
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (E : Type*) [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
def KwF4R1V384aDistinctKernels : Prop
def

KwF4R1V384aFinrankCompletionEF

L405 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.KwF4R1V384aFinrankCompletionEF
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section SpecificMints
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (E : Type*) [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
def KwF4R1V384aFinrankCompletionEF : Prop
instance

kwF4R1V384a_ker_semilocalComponent_isMaximal

L419 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_ker_semilocalComponent_isMaximal
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section BijEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
instance kwF4R1V384a_ker_semilocalComponent_isMaximal
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F] [FiniteDimensional E F]
    (v : Place K E) (w' : v.fiber F) :
    (RingHom.ker (kwF4R1V384a_semilocalComponent F v w').toRingHom).IsMaximal
theorem

kwF4R1V384a_semilocalDiag_surjective_of_distinctKernels

L426 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_semilocalDiag_surjective_of_distinctKernels
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section BijEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V384a_semilocalDiag_surjective_of_distinctKernels
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F] [FiniteDimensional E F]
    (hdist : KwF4R1V384aDistinctKernels K F E) (v : Place K E) :
    Function.Surjective (kwF4R1V384a_semilocalDiag F v)
instance

kwF4R1V384a_instModuleFiberCompletion

L452 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_instModuleFiberCompletion
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section BijEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
instance kwF4R1V384a_instModuleFiberCompletion
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
    (v : Place K E) (w' : v.fiber F) :
    Module v.adicCompletion w'.1.adicCompletion
theorem

kwF4R1V384a_completionSemilocalBij_of_distinctKernels_finrankEF

L458 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_completionSemilocalBij_of_distinctKernels_finrankEF
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section BijEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V384a_completionSemilocalBij_of_distinctKernels_finrankEF
    [Algebra.IsSeparable E F]
    (hdist : KwF4R1V384aDistinctKernels K F E)
    (hef : KwF4R1V384aFinrankCompletionEF K F E) :
    KwF4R1V384aCompletionSemilocalBij K F E
theorem

kwF4R1V384a_trace_algebraMap_eq_completionTraceAt

L511 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_trace_algebraMap_eq_completionTraceAt
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section SemilocalHeadline
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V384a_trace_algebraMap_eq_completionTraceAt
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F] [FiniteDimensional E F]
    (v : Place K E) (w' : v.fiber F) (g : F) :
    Algebra.trace v.adicCompletion w'.1.adicCompletion (algebraMap F w'.1.adicCompletion g)
      = AlgebraicCurve.kwHgfV352_completionTraceAt v w'.1 w'.2 g
theorem

kwF4R1V384a_completionTraceSum_of_semilocalBij

L521 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_completionTraceSum_of_semilocalBij
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section SemilocalHeadline
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V384a_completionTraceSum_of_semilocalBij
    (hbij : KwF4R1V384aCompletionSemilocalBij K F E) :
    AlgebraicCurve.KwHgfV352CompletionTraceSum K F E
theorem

kwF4R1V384a_completionTraceSum_of_distinctKernels_finrankEF

L539 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V384a_completionTraceSum_of_distinctKernels_finrankEF
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Semilocal
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct
section SemilocalHeadline
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V384a_completionTraceSum_of_distinctKernels_finrankEF
    [Algebra.IsSeparable E F]
    (hdist : KwF4R1V384aDistinctKernels K F E)
    (hef : KwF4R1V384aFinrankCompletionEF K F E) :
    AlgebraicCurve.KwHgfV352CompletionTraceSum K F E
theorem

kwF4R1V386a_isSeparable_algebraMap_fiberCompletion

L562 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_isSeparable_algebraMap_fiberCompletion
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section IsSeparableLift
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V386a_isSeparable_algebraMap_fiberCompletion
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
    [FiniteDimensional E F] [Algebra.IsSeparable E F]
    (v : Place K E) (w' : v.fiber F) (g : F) :
    IsSeparable v.adicCompletion (algebraMap F w'.1.adicCompletion g)
theorem

kwF4R1V386a_isSeparable_fiberCompletion

L578 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_isSeparable_fiberCompletion
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section IsSeparableLift
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V386a_isSeparable_fiberCompletion
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
    [FiniteDimensional E F] [Algebra.IsSeparable E F]
    (v : Place K E) (w' : v.fiber F) :
    Algebra.IsSeparable v.adicCompletion w'.1.adicCompletion
theorem

kwF4R1V386a_spectralNorm_eq_absoluteValue

L622 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_spectralNorm_eq_absoluteValue
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section DistinctKernels
open scoped Valued NNReal WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · full declaration
theorem kwF4R1V386a_spectralNorm_eq_absoluteValue [FiniteDimensional E F]
    (w' : Place K F) (y : w'.adicCompletion) :
    letI := kw_ffgc_rankOne_adicCompletion (w'.restrict E)
    letI : NontriviallyNormedField (w'.restrict E).adicCompletion :=
      Valued.toNontriviallyNormedField (w'.restrict E).adicCompletion ℤᵐ⁰
    spectralNorm (w'.restrict E).adicCompletion w'.adicCompletion y
      = kw_ffgc_absoluteValue E w' y := by
  let := kw_ffgc_rankOne_adicCompletion (w'.restrict E)
  let : NontriviallyNormedField (w'.restrict E).adicCompletion :=
    Valued.toNontriviallyNormedField (w'.restrict E).adicCompletion ℤᵐ⁰
  have : IsUltrametricDist (w'.restrict E).adicCompletion :=
    IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_norm
      (fun a b => Valuation.norm_add_le Valued.v a b)
  have : Algebra.IsAlgebraic (w'.restrict E).adicCompletion w'.adicCompletion :=
    Algebra.IsAlgebraic.of_finite _ _
  exact (spectralNorm_unique_field_norm_ext (f := kw_ffgc_absoluteValue E w')
    (kw_ffgc_absoluteValue_extends E w') y).symm
theorem

kwF4R1V386a_spectralNorm_eq_absoluteValue_fiber

L640 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_spectralNorm_eq_absoluteValue_fiber
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section DistinctKernels
open scoped Valued NNReal WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · full declaration
theorem kwF4R1V386a_spectralNorm_eq_absoluteValue_fiber
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F] [FiniteDimensional E F]
    (v : Place K E) (w' : v.fiber F) (y : w'.1.adicCompletion) :
    letI := kw_ffgc_rankOne_adicCompletion v
    letI : NontriviallyNormedField v.adicCompletion :=
      Valued.toNontriviallyNormedField v.adicCompletion ℤᵐ⁰
    spectralNorm v.adicCompletion w'.1.adicCompletion y
      = kw_ffgc_absoluteValue E w'.1 y := by
  rcases w' with ⟨w', hw'⟩
  have hv : w'.restrict E = v := Place.mem_fiber.mp hw'
  subst hv
  exact kwF4R1V386a_spectralNorm_eq_absoluteValue (K := K) (E := E) w' y
theorem

kwF4R1V386a_valuedAlgebraMap_le_one_iff

L653 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_valuedAlgebraMap_le_one_iff
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section DistinctKernels
open scoped Valued NNReal WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V386a_valuedAlgebraMap_le_one_iff (w' : Place K F) (g : F) :
    Valued.v (algebraMap F w'.adicCompletion g) ≤ 1 ↔ g ∈ w'.toValuationSubring
theorem

kwF4R1V386a_absoluteValue_algebraMap_le_one_iff

L658 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_absoluteValue_algebraMap_le_one_iff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section DistinctKernels
open scoped Valued NNReal WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
omit [Algebra K E] [IsScalarTower K E F] in
Lean source · statement
theorem kwF4R1V386a_absoluteValue_algebraMap_le_one_iff
    (w' : Place K F) (g : F) :
    kw_ffgc_absoluteValue E w' (algebraMap F w'.adicCompletion g) ≤ 1
      ↔ g ∈ w'.toValuationSubring
theorem

kwF4R1V386a_distinctKernels

L685 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_distinctKernels
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section DistinctKernels
open scoped Valued NNReal WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V386a_distinctKernels :
    KwF4R1V384aDistinctKernels K F E
theorem

kwF4R1V386a_ramificationIdx_completion_eq

L746 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_ramificationIdx_completion_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section FinrankCompletionEF
open IsLocalRing Valuation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V386a_ramificationIdx_completion_eq
    (w' : Place K F) :
    (maximalIdeal (w'.restrict E).adicCompletionIntegers).ramificationIdx'
      (maximalIdeal w'.adicCompletionIntegers) = w'.ramificationIndex E
theorem

kwF4R1V386a_integersToCompletion_commute

L786 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_integersToCompletion_commute
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section FinrankCompletionEF
open IsLocalRing Valuation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V386a_integersToCompletion_commute
    (w' : Place K F) (a : (w'.restrict E).toValuationSubring) :
    algebraMap (w'.restrict E).adicCompletionIntegers w'.adicCompletionIntegers
        (algebraMap (w'.restrict E).toValuationSubring
          (w'.restrict E).adicCompletionIntegers a)
      = algebraMap w'.toValuationSubring w'.adicCompletionIntegers
          (restrictInclusion E w' a)
theorem

kwF4R1V386a_inertiaDeg_completion_eq

L796 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_inertiaDeg_completion_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section FinrankCompletionEF
open IsLocalRing Valuation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V386a_inertiaDeg_completion_eq
    (w' : Place K F) :
    (maximalIdeal w'.adicCompletionIntegers).inertiaDeg
      (w'.restrict E).adicCompletionIntegers = w'.inertiaDeg E
theorem

kwF4R1V386a_finrankCompletionEF

L824 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_finrankCompletionEF
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section FinrankCompletionEF
open IsLocalRing Valuation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V386a_finrankCompletionEF [Algebra.IsSeparable E F] :
    KwF4R1V384aFinrankCompletionEF K F E
theorem

kwF4R1V386a_completionTraceSum_of_isSeparable

L911 ↗
AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable.kwF4R1V386a_completionTraceSum_of_isSeparable
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
noncomputable section
section Discharge
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain TensorProduct IsLocalRing
open scoped AlgebraicCurve.Place Valued NNReal WithZero
section DischargeHeadline
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V386a_completionTraceSum_of_isSeparable [Algebra.IsSeparable E F] :
    AlgebraicCurve.KwHgfV352CompletionTraceSum K F E
theorem

completionTraceSum_of_isSeparable

L922 ↗
AlgebraicCurve.completionTraceSum_of_isSeparable
Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.CompletionTraceSum_of_isSeparable
Lean source · statement
theorem _root_.AlgebraicCurve.completionTraceSum_of_isSeparable
    {K F E : Type*} [Field K] [Field F] [Algebra K F]
    [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
    [Algebra.IsSeparable E F] :
    AlgebraicCurve.KwHgfV352CompletionTraceSum K F E

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