Module

RelNorm_eq_pow_of_isMaximal_of_isSeparable.lean

Nyll.AlgebraicCurves.FunctionFields.RelNorm_eq_pow_of_isMaximal_of_isSeparable

26 declarations indexed from sourceView source ↗

Module documentation

Rel Norm eq pow of is Maximal of is Separable

Imports3

Mathlib.RingTheory.Ideal.Norm.RelNorm
Mathlib.RingTheory.RamificationInertia.Inertia
Mathlib.FieldTheory.SeparableClosure

Imported by3

instance

(anonymous instance)

L37 ↗

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.

Lean source · statement

instance : Algebra (FractionRing R) (FractionRing S)

instance

(anonymous instance)

L46 ↗

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)

Lean source · statement

instance : Algebra S 𝔼

instance

(anonymous instance)

L48 ↗

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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)

L50 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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)

L51 ↗

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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)

L55 ↗

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance

Lean source · statement

instance : IsIntegralClosure 𝕋 S 𝔼

instance

(anonymous instance)

L57 ↗

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
local instance : IsIntegralClosure 𝕋 S 𝔼 := integralClosure.isIntegralClosure S 𝔼

Lean source · statement

instance : IsScalarTower R 𝕋 𝔼

instance

(anonymous instance)

L64 ↗

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 𝔼

theorem

isSeparable_normalClosure

L69 ↗

AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable.AlgebraicCurve.F10d.isSeparable_normalClosure

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]

Lean source · statement

theorem isSeparable_normalClosure : Algebra.IsSeparable 𝕂 𝔼

instance

(anonymous instance)

L77 ↗

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]

Lean source · statement

instance : Algebra.IsSeparable 𝕂 𝔼

instance

(anonymous instance)

L79 ↗

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S

Lean source · statement

instance : Algebra.IsSeparable 𝕃 𝔼

instance

(anonymous instance)

L83 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]

Lean source · statement

instance : FiniteDimensional 𝕃 𝔼

instance

(anonymous instance)

L84 ↗

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼

Lean source · statement

instance : IsFractionRing 𝕋 𝔼

instance

(anonymous instance)

L88 ↗

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := by
  change IsFractionRing (integralClosure S 𝔼) 𝔼
  exact integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼

Lean source · statement

instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃)

instance

(anonymous instance)

L91 ↗

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := by
  change IsFractionRing (integralClosure S 𝔼) 𝔼
  exact integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)

Lean source · statement

instance : Normal 𝕂 𝔼

instance

(anonymous instance)

L93 ↗

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := by
  change IsFractionRing (integralClosure S 𝔼) 𝔼
  exact integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
local instance : IsAlgClosure 𝕂 (AlgebraicClosure 𝕃) :=
  IsAlgClosure.ofAlgebraic 𝕂 𝕃 (AlgebraicClosure 𝕃)
local instance : Normal 𝕂 𝔼 := normalClosure.normal _ _ _

Lean source · statement

instance : IsGalois 𝕂 𝔼

instance

(anonymous instance)

L94 ↗

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := by
  change IsFractionRing (integralClosure S 𝔼) 𝔼
  exact integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
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)

L96 ↗

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := by
  change IsFractionRing (integralClosure S 𝔼) 𝔼
  exact integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
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)

L98 ↗

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := by
  change IsFractionRing (integralClosure S 𝔼) 𝔼
  exact integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
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)

L106 ↗

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := by
  change IsFractionRing (integralClosure S 𝔼) 𝔼
  exact integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
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)

L108 ↗

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := by
  change IsFractionRing (integralClosure S 𝔼) 𝔼
  exact integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
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)

L110 ↗

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := by
  change IsFractionRing (integralClosure S 𝔼) 𝔼
  exact integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
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

L113 ↗

AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable.AlgebraicCurve.F10d.relNorm_eq_pow_of_isMaximal_fractionRing

Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
section Closure
variable (R S : Type*) [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Algebra R S] [Module.IsTorsionFree R S]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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 𝕋 𝔼 := by
  change IsScalarTower S (integralClosure S 𝔼) 𝔼
  infer_instance
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 [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
local instance : Algebra.IsSeparable 𝕂 𝔼 := isSeparable_normalClosure R S
local instance : Algebra.IsSeparable 𝕃 𝔼 := Algebra.isSeparable_tower_top_of_isSeparable 𝕂 𝕃 𝔼
variable [Module.Finite R S]
local instance : FiniteDimensional 𝕃 𝔼 := Module.Finite.right 𝕂 𝕃 𝔼
local instance : IsFractionRing 𝕋 𝔼 := by
  change IsFractionRing (integralClosure S 𝔼) 𝔼
  exact integralClosure.isFractionRing_of_finite_extension 𝕃 𝔼
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}

Lean source · statement

theorem relNorm_eq_pow_of_isMaximal_fractionRing
    (P : Ideal S) (p : Ideal R) [P.LiesOver p] [P.IsMaximal] [p.IsMaximal] :
    Ideal.relNorm R P = p ^ P.inertiaDeg R

instance

(anonymous instance)

L134 ↗

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
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]

-- Register only the required fraction-field map, as in Ring.NormalClosure.

Lean source · statement

instance : Algebra (FractionRing R) (FractionRing S)

theorem

relNorm_eq_pow_of_isMaximal_of_isSeparable

L137 ↗

AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable.AlgebraicCurve.F10d.relNorm_eq_pow_of_isMaximal_of_isSeparable

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable
noncomputable section
namespace AlgebraicCurve
namespace F10d
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]

-- Register only the required fraction-field map, as in Ring.NormalClosure.
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

relNorm_eq_pow_of_isMaximal_of_isSeparable

L158 ↗

AlgebraicCurve.relNorm_eq_pow_of_isMaximal_of_isSeparable

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.RelNorm_eq_pow_of_isMaximal_of_isSeparable

Lean source · statement

theorem _root_.AlgebraicCurve.relNorm_eq_pow_of_isMaximal_of_isSeparable {R S : Type*} [CommRing
  R] [CommRing S]
    [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S]
      [Module.IsTorsionFree R S]
    (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

Module documentation

Rel Norm eq pow of is Maximal of is Separable

Declarations