Module

Residue_norm_eq_norm_residue_of_retraction.lean

Nyll.AlgebraicCurves.Differentials.Residues.Residue_norm_eq_norm_residue_of_retraction

32 declarations indexed from sourceView source ↗

Module documentation

Residue norm eq norm residue of retraction

Imports2

Imported by2

theorem

valuation_algebraMap_eq_one

L36 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.valuation_algebraMap_eq_one

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section RationalPlace
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
  (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
include hKA in

Lean source · statement

theorem valuation_algebraMap_eq_one {k : K} (hk : k ≠ 0) :
    A.valuation (algebraMap K E k) = 1

theorem

valuation_algebraMap_le_one

L46 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.valuation_algebraMap_le_one

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section RationalPlace
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
  (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
include hKA in

Lean source · statement

theorem valuation_algebraMap_le_one (k : K) : A.valuation (algebraMap K E k) ≤ 1

theorem

const_unique

L49 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.const_unique

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section RationalPlace
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
  (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
include hKA in

Lean source · statement

theorem const_unique {a : E} {k k' : K}
    (hk : A.valuation (a - algebraMap K E k) < 1) (hk' : A.valuation (a - algebraMap K E k') < 1) :
    k = k'

def

sigmaFun

L64 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.sigmaFun

Documentation

The base-field representative of an element of A modulo its valuation maximal ideal.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section RationalPlace
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
  (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)

Lean source · statement

def sigmaFun (a : A) : K

theorem

sigmaFun_spec

L66 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.sigmaFun_spec

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section RationalPlace
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
  (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)

Lean source · statement

theorem sigmaFun_spec (a : A) :
    A.valuation ((a : E) - algebraMap K E (sigmaFun A hArat a)) < 1

theorem

sigmaFun_eq_iff

L70 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.sigmaFun_eq_iff

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section RationalPlace
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
  (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
include hKA in

Lean source · statement

theorem sigmaFun_eq_iff (a : A) (k : K) :
    sigmaFun A hArat a = k ↔ A.valuation ((a : E) - algebraMap K E k) < 1

def

sigma

L75 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.sigma

Documentation

The residue homomorphism from A to the base field supplied by rationality.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section RationalPlace
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
  (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)

Lean source · full declaration

def sigma : A →+* K where
  toFun := sigmaFun A hArat
  map_one' := by
    rw [sigmaFun_eq_iff A hKA hArat]
    simp
  map_mul' a b := by
    rw [sigmaFun_eq_iff A hKA hArat]
    have ha := sigmaFun_spec A hArat a
    have hb := sigmaFun_spec A hArat b
    set k := sigmaFun A hArat a
    set k' := sigmaFun A hArat b
    have hid : ((a * b : A) : E) - algebraMap K E (k * k') =
        (a : E) * ((b : E) - algebraMap K E k') + algebraMap K E k' * ((a : E) - algebraMap K E k)
          := by
      simp only [MulMemClass.coe_mul, map_mul]; ring
    rw [hid]
    refine lt_of_le_of_lt (Valuation.map_add _ _ _) (max_lt ?_ ?_)
    · rw [map_mul]
      exact (mul_le_mul_left (A.valuation_le_one a) _).trans_lt (by rwa [one_mul])
    · rw [map_mul]
      exact (mul_le_mul_left (valuation_algebraMap_le_one A hKA k') _).trans_lt
        (by rwa [one_mul])
  map_zero' := by
    rw [sigmaFun_eq_iff A hKA hArat]
    simp
  map_add' a b := by
    rw [sigmaFun_eq_iff A hKA hArat]
    have ha := sigmaFun_spec A hArat a
    have hb := sigmaFun_spec A hArat b
    set k := sigmaFun A hArat a
    set k' := sigmaFun A hArat b
    have hid : ((a + b : A) : E) - algebraMap K E (k + k') =
        ((a : E) - algebraMap K E k) + ((b : E) - algebraMap K E k') := by
      simp only [AddMemClass.coe_add, map_add]; ring
    rw [hid]
    exact lt_of_le_of_lt (Valuation.map_add _ _ _) (max_lt ha hb)

theorem

sigma_spec

L112 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.sigma_spec

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section RationalPlace
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
  (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)

Lean source · statement

theorem sigma_spec (a : A) :
    A.valuation ((a : E) - algebraMap K E (sigma A hKA hArat a)) < 1

theorem

sigma_eq_iff

L116 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.sigma_eq_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section RationalPlace
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
  (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)

Lean source · statement

theorem sigma_eq_iff (a : A) (k : K) :
    sigma A hKA hArat a = k ↔ A.valuation ((a : E) - algebraMap K E k) < 1

theorem

linearIndependent_pow_of_transcendental'

L123 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.linearIndependent_pow_of_transcendental'

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
open Polynomial in

Lean source · full declaration

theorem linearIndependent_pow_of_transcendental' {R S : Type*} [CommRing R] [Ring S] [Algebra R S]
    {x : S} (hx : Transcendental R x) : LinearIndependent R fun k : ℕ => x ^ k := by
  rw [linearIndependent_iff]
  intro l hl
  set p : R[X] := l.sum fun n a => Polynomial.monomial n a with hp
  have hcoeff : ∀ n, p.coeff n = l n := fun n => by
    rw [hp, Finsupp.sum, Polynomial.finsetSum_coeff]
    simp only [Polynomial.coeff_monomial]
    rw [Finset.sum_ite_eq']
    split_ifs with h
    · rfl
    · exact (Finsupp.notMem_support_iff.mp h).symm
  have h1 : aeval x p = Finsupp.linearCombination R (fun k : ℕ => x ^ k) l := by
    rw [hp, Finsupp.sum, map_sum, Finsupp.linearCombination_apply, Finsupp.sum]
    refine Finset.sum_congr rfl fun k _ => ?_
    rw [aeval_monomial, Algebra.smul_def]
  have h2 := (transcendental_iff.mp hx) p (h1.trans hl)
  ext n
  rw [← hcoeff, h2, Polynomial.coeff_zero, Finsupp.zero_apply]

theorem

transcendental_ratFunc_X

L143 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.transcendental_ratFunc_X

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue

Lean source · statement

theorem transcendental_ratFunc_X (K : Type*) [Field K] :
    Transcendental K (RatFunc.X : RatFunc K)

theorem

isUnit_iff_inv_mem

L150 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.isUnit_iff_inv_mem

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue

Lean source · statement

theorem isUnit_iff_inv_mem {L : Type*} [Field L] (O : ValuationSubring L) (z : O) (hz : (z : L) ≠
  0) :
    IsUnit z ↔ (z : L)⁻¹ ∈ O

theorem

map_eq_zero_of_not_isUnit

L164 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.map_eq_zero_of_not_isUnit

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue

Lean source · statement

theorem map_eq_zero_of_not_isUnit {L R : Type*} [Field L] [Semiring R] (O : ValuationSubring L)
    (ρ : O →+* R) (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O) {z : O} (hz : ¬ IsUnit z) :
    ρ z = 0

theorem

isUnit_of_map_ne_zero

L170 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.isUnit_of_map_ne_zero

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue

Lean source · statement

theorem isUnit_of_map_ne_zero {L R : Type*} [Field L] [Semiring R] (O : ValuationSubring L)
    (ρ : O →+* R) (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O) {z : O} (hz : ρ z ≠ 0) :
    IsUnit z

theorem

algebraMap_polynomial_map

L183 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.algebraMap_polynomial_map

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section TwoTowers
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]

Lean source · statement

theorem algebraMap_polynomial_map
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
    (p : K[X]) :
    algebraMap (RatFunc E) FE (algebraMap E[X] (RatFunc E) (p.map (algebraMap K E))) =
      algebraMap F FE (algebraMap (RatFunc K) F (algebraMap K[X] (RatFunc K) p))

theorem

exists_algebraMap_eq

L206 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.exists_algebraMap_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section TwoTowers
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]

Lean source · statement

theorem exists_algebraMap_eq
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
    (l : RatFunc K) :
    ∃ m : RatFunc E, algebraMap (RatFunc E) FE m = algebraMap F FE (algebraMap (RatFunc K) F l)

theorem

algebraMap_ratFunc_polynomial

L217 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.algebraMap_ratFunc_polynomial

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section TwoTowers
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]

Lean source · statement

theorem algebraMap_ratFunc_polynomial (p : E[X]) :
    algebraMap (RatFunc E) FE (algebraMap E[X] (RatFunc E) p) =
      Polynomial.aeval (algebraMap (RatFunc E) FE RatFunc.X) p

theorem

exists_basis_algebraMap

L224 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.exists_basis_algebraMap

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section TwoTowers
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]
variable [IsAlgClosed K] [CharZero K]

Lean source · statement

theorem exists_basis_algebraMap
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
    {ι : Type*} [Finite ι] (b : Module.Basis ι (RatFunc K) F) :
    ∃ β : Module.Basis ι (RatFunc E) FE, ∀ i, β i = algebraMap F FE (b i)

theorem

algebraMap_mem

L329 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.algebraMap_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
include hρ in

Lean source · statement

theorem algebraMap_mem (f : F) : algebraMap F FE f ∈ O

theorem

rho_algebraMap

L333 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.rho_algebraMap

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
include hρ in

Lean source · statement

theorem rho_algebraMap (f : F) (h : algebraMap F FE f ∈ O) : ρ ⟨algebraMap F FE f, h⟩ = f

def

constEmb

L338 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.constEmb

Documentation

The inclusion of the base valuation ring into the extending valuation ring.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)

Lean source · full declaration

def constEmb : A →+* O where
  toFun a := ⟨algebraMap E FE a, (hO a).mpr a.2⟩
  map_one' := Subtype.ext (by simp)
  map_mul' a b := Subtype.ext (by simp)
  map_zero' := Subtype.ext (by simp)
  map_add' a b := Subtype.ext (by simp)

theorem

coe_constEmb

L345 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.coe_constEmb

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)

Lean source · statement

theorem coe_constEmb (a : A) : ((constEmb A O hO a : O) : FE) = algebraMap E FE a

theorem

rho_constEmb

L348 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.rho_constEmb

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
include hKA hker hρ in

Lean source · statement

theorem rho_constEmb (a : A) :
    ρ (constEmb A O hO a) = algebraMap K F (sigma A hKA hArat a)

theorem

X_mem

L387 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.X_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
variable [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
omit [Algebra K F] [Algebra E FE] [Algebra K E] [Algebra K FE] [IsScalarTower K E FE]
  [IsScalarTower K F FE] [IsScalarTower K (RatFunc K) F] [IsScalarTower E (RatFunc E) FE] in
include hX hρ in

Lean source · statement

theorem X_mem : algebraMap (RatFunc E) FE RatFunc.X ∈ O

def

polyEmb

L391 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.polyEmb

Documentation

The polynomial evaluation homomorphism into the extending valuation ring.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
variable [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))

Lean source · statement

def polyEmb : A[X] →+* O

theorem

coe_polyEmb

L395 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.coe_polyEmb

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
variable [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
omit [Algebra K F] [Algebra K E] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
  [IsScalarTower K (RatFunc K) F] in

Lean source · statement

theorem coe_polyEmb (p₀ : A[X]) :
    ((polyEmb A O ρ hO hρ hX p₀ : O) : FE) =
      algebraMap (RatFunc E) FE (algebraMap E[X] (RatFunc E) (p₀.map (algebraMap A E)))

theorem

rho_polyEmb

L413 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.rho_polyEmb

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
variable [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
omit [IsScalarTower E (RatFunc E) FE] in
include hKA hArat hker in

Lean source · statement

theorem rho_polyEmb (p₀ : A[X]) :
    ρ (polyEmb A O ρ hO hρ hX p₀) =
      algebraMap (RatFunc K) F (algebraMap K[X] (RatFunc K) (p₀.map (sigma A hKA hArat)))

theorem

coeff_C_inv_mul_mem

L433 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.coeff_C_inv_mul_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
variable [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))

Lean source · statement

theorem coeff_C_inv_mul_mem (f : E[X]) (c₀ : E)
    (hmax : ∀ c ∈ f.coeffs, A.valuation c ≤ A.valuation c₀) (n : ℕ) :
    (Polynomial.C c₀⁻¹ * f).coeff n ∈ A

theorem

exists_rho_eq_algebraMap

L442 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.exists_rho_eq_algebraMap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
variable [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
include hKA hArat hO hker hρ hX in

Lean source · statement

theorem exists_rho_eq_algebraMap (m : RatFunc E) (hm : algebraMap (RatFunc E) FE m ∈ O) :
    ∃ l : RatFunc K, ρ ⟨algebraMap (RatFunc E) FE m, hm⟩ = algebraMap (RatFunc K) F l

theorem

algebraMap_coord_mem

L541 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.algebraMap_coord_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
variable [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
include hKA hArat hO hker hρ hX in

Lean source · statement

theorem algebraMap_coord_mem {ι : Type*} [Fintype ι] (b : ι → F)
    (hb : LinearIndependent (RatFunc K) b) (c : ι → RatFunc E)
    (hc : (∑ i, c i • algebraMap F FE (b i)) ∈ O) (i : ι) :
    algebraMap (RatFunc E) FE (c i) ∈ O

theorem

residue_norm_eq_norm_residue

L599 ↗

AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction.DeuringNormResidue.residue_norm_eq_norm_residue

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
namespace DeuringNormResidue
section Reduction
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
variable [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
include hKA hArat hO hker hρ hX in

Lean source · statement

theorem residue_norm_eq_norm_residue [IsAlgClosed K] [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    [FiniteDimensional (RatFunc K) F] [FiniteDimensional (RatFunc E) FE]
    (g : O) :
    ∃ h : algebraMap (RatFunc E) FE (Algebra.norm (RatFunc E) (g : FE)) ∈ O,
      ρ ⟨_, h⟩ = algebraMap (RatFunc K) F (Algebra.norm (RatFunc K) (ρ g))

theorem

residue_norm_eq_norm_residue_of_retraction

L673 ↗

AlgebraicCurve.residue_norm_eq_norm_residue_of_retraction

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.Residue_norm_eq_norm_residue_of_retraction
open AlgebraicCurve
open scoped Polynomial
open DeuringNormResidue in

Lean source · statement

theorem _root_.AlgebraicCurve.residue_norm_eq_norm_residue_of_retraction
    (K F E FE : Type*) [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    [IsAlgClosed K] [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE] [FiniteDimensional (RatFunc E) FE]
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
    (A : ValuationSubring E)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
    (g : O) (_hg : ρ g ≠ 0) :
    ∃ h : algebraMap (RatFunc E) FE (Algebra.norm (RatFunc E) (g : FE)) ∈ O,
      ρ ⟨_, h⟩ = algebraMap (RatFunc K) F (Algebra.norm (RatFunc K) (ρ g))

Module documentation

Residue norm eq norm residue of retraction

Declarations