NYLL
Module

HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.lean

Nyll.AlgebraicCurves.Divisors.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
53 declarations indexed from sourceView source ↗

Module documentation

Has Principal Divisors of finite Dimensional rat Func of is Separable

Imports10
Imported by1

Declarations

theorem

eq_ord_of_addHom_of_nonneg_iff

L47 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.eq_ord_of_addHom_of_nonneg_iff
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Uniqueness
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
Lean source · statement
theorem eq_ord_of_addHom_of_nonneg_iff (φ : F → ℤ)
    (hmul : ∀ x y, x ≠ 0 → y ≠ 0 → φ (x * y) = φ x + φ y)
    (hone : ∃ t, t ≠ 0 ∧ φ t = 1)
    (hiff : ∀ x, x ≠ 0 → (0 ≤ φ x ↔ x ∈ w.toValuationSubring))
    {x : F} (hx : x ≠ 0) : φ x = w.ord x
theorem

neg_log_valuation_fiberCenter_eq_ord

L124 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.neg_log_valuation_fiberCenter_eq_ord
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ValuationDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem neg_log_valuation_fiberCenter_eq_ord (hw : w.restrict F = v) {x : F'} (hx : x ≠ 0) :
    -log ((fiberCenter F' v hw).valuation F' x) = w.ord x
theorem

le_ord_iff_mem_pow_fiberCenter

L163 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.le_ord_iff_mem_pow_fiberCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ValuationDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem le_ord_iff_mem_pow_fiberCenter (hw : w.restrict F = v)
    {c : integralClosureAt F' v} (hc : c ≠ 0) (n : ℕ) :
    (n : ℤ) ≤ w.ord (algebraMap (integralClosureAt F' v) F' c) ↔
      c ∈ (fiberCenter F' v hw).asIdeal ^ n
theorem

ramificationIndex_eq_ramificationIdx_fiberCenter

L186 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.ramificationIndex_eq_ramificationIdx_fiberCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ValuationDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem ramificationIndex_eq_ramificationIdx_fiberCenter (hw : w.restrict F = v) :
    w.ramificationIndex F =
      (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
        (fiberCenter F' v hw).asIdeal
def

toValuationSubringOfRestrictEq

L218 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.toValuationSubringOfRestrictEq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def toValuationSubringOfRestrictEq (hw : w.restrict F = v) :
    integralClosureAt F' v →+* w.toValuationSubring
theorem

coe_toValuationSubringOfRestrictEq

L224 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.coe_toValuationSubringOfRestrictEq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem coe_toValuationSubringOfRestrictEq (hw : w.restrict F = v)
    (c : integralClosureAt F' v) :
    (toValuationSubringOfRestrictEq hw c : F')
      = algebraMap (integralClosureAt F' v) F' c
def

residueOfCenter

L229 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.residueOfCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def residueOfCenter (hw : w.restrict F = v) :
    integralClosureAt F' v →+* w.ResidueField
theorem

residueOfCenter_apply

L233 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.residueOfCenter_apply
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem residueOfCenter_apply (hw : w.restrict F = v) (c : integralClosureAt F' v) :
    residueOfCenter hw c = IsLocalRing.residue w.toValuationSubring
      (toValuationSubringOfRestrictEq hw c)
theorem

ker_residueOfCenter

L237 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.ker_residueOfCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem ker_residueOfCenter (hw : w.restrict F = v) :
    RingHom.ker (residueOfCenter hw) = (fiberCenter F' v hw).asIdeal
theorem

surjective_residueOfCenter

L243 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.surjective_residueOfCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem surjective_residueOfCenter (hw : w.restrict F = v) :
    Function.Surjective (residueOfCenter hw)
def

residueFieldEquivQuotientCenter

L305 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.residueFieldEquivQuotientCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def residueFieldEquivQuotientCenter (hw : w.restrict F = v) :
    integralClosureAt F' v ⧸ (fiberCenter F' v hw).asIdeal ≃+* w.ResidueField
theorem

residueFieldEquivQuotientCenter_mk

L310 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.residueFieldEquivQuotientCenter_mk
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem residueFieldEquivQuotientCenter_mk (hw : w.restrict F = v)
    (c : integralClosureAt F' v) :
    residueFieldEquivQuotientCenter hw (Ideal.Quotient.mk _ c) = residueOfCenter hw c
def

placeCongrEquiv

L319 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.placeCongrEquiv
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · full declaration
def placeCongrEquiv {u u' : Place K F} (h : u = u') :
    u.toValuationSubring ≃+* u'.toValuationSubring where
  toFun x := ⟨x.1, h ▸ x.2⟩
  invFun x := ⟨x.1, h.symm ▸ x.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
  map_add' _ _ := rfl
theorem

coe_placeCongrEquiv

L328 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.coe_placeCongrEquiv
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem coe_placeCongrEquiv {u u' : Place K F} (h : u = u') (x : u.toValuationSubring) :
    (placeCongrEquiv h x : F) = (x : F)
def

restrictResidueFieldEquiv

L331 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.restrictResidueFieldEquiv
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def restrictResidueFieldEquiv (hw : w.restrict F = v) :
    (w.restrict F).ResidueField ≃+* IsLocalRing.ResidueField v.toValuationSubring
theorem

restrictResidueFieldEquiv_residue

L335 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.restrictResidueFieldEquiv_residue
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem restrictResidueFieldEquiv_residue (hw : w.restrict F = v)
    (a : (w.restrict F).toValuationSubring) :
    restrictResidueFieldEquiv hw (IsLocalRing.residue _ a)
      = IsLocalRing.residue _ (placeCongrEquiv hw a)
theorem

inertiaDeg_eq_inertiaDeg_fiberCenter

L342 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.inertiaDeg_eq_inertiaDeg_fiberCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem inertiaDeg_eq_inertiaDeg_fiberCenter (hw : w.restrict F = v) :
    w.inertiaDeg F =
      (fiberCenter F' v hw).asIdeal.inertiaDeg v.toValuationSubring
theorem

aeval_mem

L385 ↗
AlgebraicCurve.Place.aeval_mem
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section SupportTransfer
open Polynomial
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F'] [Algebra F F']
  [FiniteDimensional F F']
variable (w : Place K F')
omit [FiniteDimensional F F'] in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.aeval_mem {Q : Polynomial F} {x : F'}
    (hcoeff : ∀ i, algebraMap F F' (Q.coeff i) ∈ w.toValuationSubring)
    (hx : x ∈ w.toValuationSubring) :
    Polynomial.aeval x Q ∈ w.toValuationSubring
theorem

exists_coeff_ord_ne_zero

L394 ↗
AlgebraicCurve.Place.exists_coeff_ord_ne_zero
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section SupportTransfer
open Polynomial
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F'] [Algebra F F']
  [FiniteDimensional F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_coeff_ord_ne_zero {f : F'} (hf : f ≠ 0) (hford :
  w.ord f ≠ 0) :
    ∃ i < (minpoly F f).natDegree, (minpoly F f).coeff i ≠ 0 ∧
      w.ord (algebraMap F F' ((minpoly F f).coeff i)) ≠ 0
instance

(anonymous instance)

L459 ↗
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
Lean source · statement
instance : Algebra (FractionRing R) (FractionRing S)
instance

(anonymous instance)

L468 ↗
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
Lean source · statement
instance : Algebra S 𝔼
instance

(anonymous instance)

L470 ↗
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
Lean source · statement
instance : IsScalarTower S 𝕃 𝔼
instance

(anonymous instance)

L472 ↗
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
instance : Algebra 𝕋 𝔼
instance

(anonymous instance)

L474 ↗
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
Lean source · statement
instance : IsScalarTower S 𝕋 𝔼
instance

(anonymous instance)

L476 ↗
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
Lean source · statement
instance : IsIntegralClosure 𝕋 S 𝔼
instance

(anonymous instance)

L478 ↗
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
Lean source · statement
instance : IsScalarTower R 𝕋 𝔼
instance

(anonymous instance)

L485 ↗
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
Lean source · statement
instance : FaithfulSMul S 𝔼
instance

(anonymous instance)

L490 ↗
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
Lean source · statement
instance : FiniteDimensional 𝕃 𝔼
instance

(anonymous instance)

L492 ↗
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
Lean source · statement
instance : IsFractionRing 𝕋 𝔼
theorem

isSeparable_normalClosure

L497 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.SeparableRelNorm.isSeparable_normalClosure
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
omit [Module.Finite R S] in
Lean source · statement
theorem isSeparable_normalClosure : Algebra.IsSeparable 𝕂 𝔼
instance

(anonymous instance)

L505 ↗
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
Lean source · statement
instance : Algebra.IsSeparable 𝕂 𝔼
instance

(anonymous instance)

L507 ↗
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
Lean source · statement
instance : Algebra.IsSeparable 𝕃 𝔼
instance

(anonymous instance)

L509 ↗
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
Lean source · statement
instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃)
instance

(anonymous instance)

L512 ↗
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)
Lean source · statement
instance : Normal 𝕂 𝔼
instance

(anonymous instance)

L514 ↗
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)
local instance : Normal 𝕂 𝔼 := normalClosure.normal _ _ _
Lean source · statement
instance : IsGalois 𝕂 𝔼
instance

(anonymous instance)

L516 ↗
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)
local instance : Normal 𝕂 𝔼 := normalClosure.normal _ _ _
local instance : IsGalois 𝕂 𝔼 := IsGalois.mk
Lean source · statement
instance : Algebra 𝕂 (FractionRing 𝕋)
instance

(anonymous instance)

L519 ↗
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)
local instance : Normal 𝕂 𝔼 := normalClosure.normal _ _ _
local instance : IsGalois 𝕂 𝔼 := IsGalois.mk
local instance : Algebra 𝕂 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra R (FractionRing 𝕋)
Lean source · statement
instance : Algebra 𝕃 (FractionRing 𝕋)
instance

(anonymous instance)

L522 ↗
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)
local instance : Normal 𝕂 𝔼 := normalClosure.normal _ _ _
local instance : IsGalois 𝕂 𝔼 := IsGalois.mk
local instance : Algebra 𝕂 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra R (FractionRing 𝕋)
local instance : Algebra 𝕃 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra S (FractionRing 𝕋)
Lean source · statement
instance : IsGalois 𝕂 (FractionRing 𝕋)
instance

(anonymous instance)

L530 ↗
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)
local instance : Normal 𝕂 𝔼 := normalClosure.normal _ _ _
local instance : IsGalois 𝕂 𝔼 := IsGalois.mk
local instance : Algebra 𝕂 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra R (FractionRing 𝕋)
local instance : Algebra 𝕃 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra S (FractionRing 𝕋)
local instance : IsGalois 𝕂 (FractionRing 𝕋) := by
  refine IsGalois.of_equiv_equiv (F := 𝕂) (E := 𝔼)
    (f := (FractionRing.algEquiv R 𝕂).symm.toRingEquiv)
    (g := (FractionRing.algEquiv 𝕋 𝔼).symm.toRingEquiv) ?_
  ext
  simpa using IsFractionRing.algEquiv_commutes (FractionRing.algEquiv R 𝕂).symm
    (FractionRing.algEquiv 𝕋 𝔼).symm _
Lean source · statement
instance : Module.Finite S 𝕋
instance

(anonymous instance)

L532 ↗
Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)
local instance : Normal 𝕂 𝔼 := normalClosure.normal _ _ _
local instance : IsGalois 𝕂 𝔼 := IsGalois.mk
local instance : Algebra 𝕂 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra R (FractionRing 𝕋)
local instance : Algebra 𝕃 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra S (FractionRing 𝕋)
local instance : IsGalois 𝕂 (FractionRing 𝕋) := by
  refine IsGalois.of_equiv_equiv (F := 𝕂) (E := 𝔼)
    (f := (FractionRing.algEquiv R 𝕂).symm.toRingEquiv)
    (g := (FractionRing.algEquiv 𝕋 𝔼).symm.toRingEquiv) ?_
  ext
  simpa using IsFractionRing.algEquiv_commutes (FractionRing.algEquiv R 𝕂).symm
    (FractionRing.algEquiv 𝕋 𝔼).symm _
local instance : Module.Finite S 𝕋 := IsIntegralClosure.finite S 𝕃 𝔼 𝕋
Lean source · statement
instance : Module.Finite R 𝕋
instance

(anonymous instance)

L534 ↗
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)
local instance : Normal 𝕂 𝔼 := normalClosure.normal _ _ _
local instance : IsGalois 𝕂 𝔼 := IsGalois.mk
local instance : Algebra 𝕂 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra R (FractionRing 𝕋)
local instance : Algebra 𝕃 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra S (FractionRing 𝕋)
local instance : IsGalois 𝕂 (FractionRing 𝕋) := by
  refine IsGalois.of_equiv_equiv (F := 𝕂) (E := 𝔼)
    (f := (FractionRing.algEquiv R 𝕂).symm.toRingEquiv)
    (g := (FractionRing.algEquiv 𝕋 𝔼).symm.toRingEquiv) ?_
  ext
  simpa using IsFractionRing.algEquiv_commutes (FractionRing.algEquiv R 𝕂).symm
    (FractionRing.algEquiv 𝕋 𝔼).symm _
local instance : Module.Finite S 𝕋 := IsIntegralClosure.finite S 𝕃 𝔼 𝕋
local instance : Module.Finite R 𝕋 := Module.Finite.trans S 𝕋
Lean source · statement
instance : IsDedekindDomain 𝕋
theorem

relNorm_eq_pow_of_isMaximal_fractionRing

L539 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.SeparableRelNorm.relNorm_eq_pow_of_isMaximal_fractionRing
Source context 34 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Closure
variable (R S : Type*) [CommRing R] [CommRing S]
  [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
local instance : Algebra S 𝔼 := ((algebraMap 𝕃 𝔼).comp (algebraMap S 𝕃)).toAlgebra
local instance : IsScalarTower S 𝕃 𝔼 := IsScalarTower.of_algebraMap_eq' rfl
local instance : Algebra 𝕋 𝔼 := inferInstanceAs (Algebra (integralClosure S 𝔼) 𝔼)
local instance : IsScalarTower S 𝕋 𝔼 := inferInstanceAs (IsScalarTower S (integralClosure S 𝔼) 𝔼)
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼
local instance : IsScalarTower R 𝕋 𝔼 :=
  IsScalarTower.of_algebraMap_eq fun r => Subtype.ext <| by
    change algebraMap R (AlgebraicClosure 𝕃) r
      = algebraMap 𝕃 (AlgebraicClosure 𝕃) (algebraMap S 𝕃 (algebraMap R S r))
    rw [IsScalarTower.algebraMap_apply R 𝕃 (AlgebraicClosure 𝕃), IsScalarTower.algebraMap_apply R S
      𝕃]
local instance : FaithfulSMul S 𝔼 := (faithfulSMul_iff_algebraMap_injective S 𝔼).mpr <|
      (FaithfulSMul.algebraMap_injective 𝕃 𝔼).comp (FaithfulSMul.algebraMap_injective S 𝕃)
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
variable [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)
local instance : Normal 𝕂 𝔼 := normalClosure.normal _ _ _
local instance : IsGalois 𝕂 𝔼 := IsGalois.mk
local instance : Algebra 𝕂 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra R (FractionRing 𝕋)
local instance : Algebra 𝕃 (FractionRing 𝕋) :=
  FractionRing.liftAlgebra S (FractionRing 𝕋)
local instance : IsGalois 𝕂 (FractionRing 𝕋) := by
  refine IsGalois.of_equiv_equiv (F := 𝕂) (E := 𝔼)
    (f := (FractionRing.algEquiv R 𝕂).symm.toRingEquiv)
    (g := (FractionRing.algEquiv 𝕋 𝔼).symm.toRingEquiv) ?_
  ext
  simpa using IsFractionRing.algEquiv_commutes (FractionRing.algEquiv R 𝕂).symm
    (FractionRing.algEquiv 𝕋 𝔼).symm _
local instance : Module.Finite S 𝕋 := IsIntegralClosure.finite S 𝕃 𝔼 𝕋
local instance : Module.Finite R 𝕋 := Module.Finite.trans S 𝕋
local instance : IsDedekindDomain 𝕋 := integralClosure.isDedekindDomain S 𝕃 𝔼
variable {R S}
omit [Algebra.IsSeparable (FractionRing R) (FractionRing S)] in
Lean source · statement
theorem relNorm_eq_pow_of_isMaximal_fractionRing
    (hsep : Algebra.IsSeparable (FractionRing R) (FractionRing S))
    (P : Ideal S) (p : Ideal R) [P.LiesOver p] [P.IsMaximal] [p.IsMaximal] :
    Ideal.relNorm R P = p ^ P.inertiaDeg R
instance

(anonymous instance)

L561 ↗
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Transport
variable {R S : Type*} [CommRing R] [CommRing S]
  [Algebra R S] [Module.IsTorsionFree R S] [Module.Finite R S]
  [IsDedekindDomain R] [IsDedekindDomain S]
Lean source · statement
instance : Algebra (FractionRing R) (FractionRing S)
theorem

relNorm_eq_pow_of_isMaximal_of_isSeparable

L564 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.SeparableRelNorm.relNorm_eq_pow_of_isMaximal_of_isSeparable
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SeparableRelNorm
section Transport
variable {R S : Type*} [CommRing R] [CommRing S]
  [Algebra R S] [Module.IsTorsionFree R S] [Module.Finite R S]
  [IsDedekindDomain R] [IsDedekindDomain S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
Lean source · statement
theorem relNorm_eq_pow_of_isMaximal_of_isSeparable (K L : Type*) [Field K] [Field L]
    [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L]
    [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] [Algebra.IsSeparable K L]
    (P : Ideal S) (p : Ideal R) [P.LiesOver p] [P.IsMaximal] [p.IsMaximal] :
    Ideal.relNorm R P = p ^ P.inertiaDeg R
theorem

ord_coe_eq_of_span_singleton_eq_pow_maximalIdeal

L596 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.ord_coe_eq_of_span_singleton_eq_pow_maximalIdeal
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section DVR
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem ord_coe_eq_of_span_singleton_eq_pow_maximalIdeal {r : v.toValuationSubring} {n : ℕ}
    (h : Ideal.span {r} = IsLocalRing.maximalIdeal v.toValuationSubring ^ n) :
    v.ord (r : F) = n
theorem

relNorm_fiberCenter

L627 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.relNorm_fiberCenter
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Place
open _root_.AlgebraicCurve.Place
section IdealNorm
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem relNorm_fiberCenter (hw : w.restrict F = v) :
    Ideal.relNorm v.toValuationSubring (fiberCenter F' v hw).asIdeal
      = IsLocalRing.maximalIdeal v.toValuationSubring ^ w.inertiaDeg F
theorem

count_normalizedFactors_span_singleton

L638 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.count_normalizedFactors_span_singleton
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Place
open _root_.AlgebraicCurve.Place
section IdealNorm
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem count_normalizedFactors_span_singleton
    (hw : w.restrict F = v) {c : integralClosureAt F' v} (hc : c ≠ 0) :
    (normalizedFactors (Ideal.span {c})).count (fiberCenter F' v hw).asIdeal
      = (w.ord (algebraMap (integralClosureAt F' v) F' c)).toNat
theorem

relNorm_span_singleton

L654 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.relNorm_span_singleton
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Place
open _root_.AlgebraicCurve.Place
section IdealNorm
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem relNorm_span_singleton {c : integralClosureAt F' v}
    (hc : c ≠ 0) :
    Ideal.relNorm v.toValuationSubring (Ideal.span {c})
      = IsLocalRing.maximalIdeal v.toValuationSubring
          ^ (∑ w ∈ v.fiberOver F',
              w.inertiaDeg F * (w.ord (algebraMap (integralClosureAt F' v) F' c)).toNat)
theorem

ord_norm_algebraMap_integralClosureAt

L737 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.ord_norm_algebraMap_integralClosureAt
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Place
open _root_.AlgebraicCurve.Place
section ElementNorm
variable (v : Place K F)
Lean source · statement
theorem ord_norm_algebraMap_integralClosureAt
    {c : integralClosureAt F' v} (hc : c ≠ 0) :
    v.ord (Algebra.norm F (algebraMap (integralClosureAt F' v) F' c))
      = ∑ w ∈ v.fiberOver F', (w.inertiaDeg F : ℤ)
          * w.ord (algebraMap (integralClosureAt F' v) F' c)
theorem

ord_norm_eq_sum_fiberOver

L752 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Place.ord_norm_eq_sum_fiberOver
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Place
open _root_.AlgebraicCurve.Place
section ElementNorm
variable (v : Place K F)
Lean source · statement
theorem ord_norm_eq_sum_fiberOver {f : F'} (hf : f ≠ 0) :
    v.ord (Algebra.norm F f) = ∑ w ∈ v.fiberOver F', (w.inertiaDeg F : ℤ) * w.ord f
theorem

pushforwardNormFormula_of_finiteDimensional

L786 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.Divisor.pushforwardNormFormula_of_finiteDimensional
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Divisor
open _root_.AlgebraicCurve.Divisor
Lean source · statement
theorem pushforwardNormFormula_of_finiteDimensional :
    Divisor.PushforwardNormFormula K F F'
theorem

finite_setOf_ord_ne_zero_of_finiteDimensional

L812 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable.AlgebraicCurve.finite_setOf_ord_ne_zero_of_finiteDimensional
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section T029
variable {K : Type*} [Field K] {F' : Type*} [Field F'] [Algebra K F']
  [Algebra (RatFunc K) F'] [IsScalarTower K (RatFunc K) F']
  [FiniteDimensional (RatFunc K) F'] [Algebra.IsSeparable (RatFunc K) F']
Lean source · statement
theorem finite_setOf_ord_ne_zero_of_finiteDimensional {f : F'} (hf : f ≠ 0) :
    {w : Place K F' | w.ord f ≠ 0}.Finite
theorem

hasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable

L836 ↗
AlgebraicCurve.hasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.hasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable (K :
  Type*) [Field K] (F' : Type*)
    [Field F'] [Algebra K F'] [Algebra (RatFunc K) F'] [IsScalarTower K (RatFunc K) F']
      [FiniteDimensional (RatFunc K) F']
    [Algebra.IsSeparable (RatFunc K) F'] :
    HasPrincipalDivisors K F'

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