NYLL
Module

RingExtension.lean

Nyll.SchemeTheory.RingTheory.Localization.Fraction.RingExtension
6 declarations indexed from sourceView source ↗

Module documentation

A chosen field extension over the literal fraction ring

An application may use an arbitrary chosen fraction field K of a domain V, while a generic construction is formulated over the literal quotient type FractionRing V. This file fixes the canonical composite algebra on an extension L / K and transports finiteness and separability across the canonical fraction-field equivalence.

Imports2
  • Mathlib.FieldTheory.SeparableDegree
  • Mathlib.RingTheory.Localization.FractionRing
Imported by3

Declarations

abbrev

fractionRingToExtensionAlgebra

L33 ↗
EtaleFundamentalGroups.fractionRingToExtensionAlgebra
Documentation

The canonical algebra on L over the literal fraction ring of V, factored through the chosen fraction field K.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uV uK uL
variable {V : Type uV} {K : Type uK} {L : Type uL}
variable [CommRing V] [IsDomain V]
variable [Field K] [Algebra V K] [IsFractionRing V K]
variable [Field L] [Algebra K L]
Lean source · statement
abbrev fractionRingToExtensionAlgebra :
    Algebra (FractionRing V) L
def

fractionRingChosenFractionFieldAlgEquiv

L41 ↗
EtaleFundamentalGroups.fractionRingChosenFractionFieldAlgEquiv
Documentation

The canonical map from the literal fraction ring to a chosen fraction field is an algebra equivalence over the literal fraction ring itself.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uV uK uL
variable {V : Type uV} {K : Type uK} {L : Type uL}
variable [CommRing V] [IsDomain V]
variable [Field K] [Algebra V K] [IsFractionRing V K]
variable [Field L] [Algebra K L]
Lean source · full declaration
def fractionRingChosenFractionFieldAlgEquiv :
    letI : Algebra (FractionRing V) K := FractionRing.liftAlgebra V K
    FractionRing V ≃ₐ[FractionRing V] K := by
  letI : Algebra (FractionRing V) K := FractionRing.liftAlgebra V K
  refine AlgEquiv.ofRingEquiv
    (f := (FractionRing.algEquiv V K).toRingEquiv) fun x ↦ ?_
  change (FractionRing.algEquiv V K) x = algebraMap (FractionRing V) K x
  have h : (FractionRing.algEquiv V K).toRingEquiv.toRingHom =
      algebraMap (FractionRing V) K := by
    apply IsLocalization.ringHom_ext (nonZeroDivisors V)
    ext v
    change (FractionRing.algEquiv V K) (algebraMap V (FractionRing V) v) =
      algebraMap (FractionRing V) K (algebraMap V (FractionRing V) v)
    rw [(FractionRing.algEquiv V K).commutes]
    exact IsScalarTower.algebraMap_apply V (FractionRing V) K v
  exact DFunLike.congr_fun h x
theorem

fractionRingToChosenFractionFieldToExtension_isScalarTower

L61 ↗
EtaleFundamentalGroups.fractionRingToChosenFractionFieldToExtension_isScalarTower
Documentation

The literal fraction ring, chosen fraction field, and extension use a definitionally compatible scalar tower.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uV uK uL
variable {V : Type uV} {K : Type uK} {L : Type uL}
variable [CommRing V] [IsDomain V]
variable [Field K] [Algebra V K] [IsFractionRing V K]
variable [Field L] [Algebra K L]
omit [IsDomain V] in
Lean source · full declaration
theorem fractionRingToChosenFractionFieldToExtension_isScalarTower :
    letI : Algebra (FractionRing V) K := FractionRing.liftAlgebra V K
    letI : Algebra (FractionRing V) L :=
      fractionRingToExtensionAlgebra (V := V) (K := K) (L := L)
    IsScalarTower (FractionRing V) K L := by
  let : Algebra (FractionRing V) K := FractionRing.liftAlgebra V K
  let : Algebra (FractionRing V) L :=
    fractionRingToExtensionAlgebra (V := V) (K := K) (L := L)
  exact IsScalarTower.of_algebraMap_eq' rfl
theorem

fractionRingToExtension_isScalarTower

L76 ↗
EtaleFundamentalGroups.fractionRingToExtension_isScalarTower
Documentation

The original base map and the composite map from the literal fraction ring are compatible.

Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uV uK uL
variable {V : Type uV} {K : Type uK} {L : Type uL}
variable [CommRing V] [IsDomain V]
variable [Field K] [Algebra V K] [IsFractionRing V K]
variable [Field L] [Algebra K L]
variable [Algebra V L] [IsScalarTower V K L]
omit [IsDomain V] in
Lean source · full declaration
theorem fractionRingToExtension_isScalarTower :
    letI : Algebra (FractionRing V) L :=
      fractionRingToExtensionAlgebra (V := V) (K := K) (L := L)
    IsScalarTower V (FractionRing V) L := by
  let : Algebra (FractionRing V) K := FractionRing.liftAlgebra V K
  let : IsScalarTower V (FractionRing V) K :=
    FractionRing.isScalarTower_liftAlgebra V K
  let : Algebra (FractionRing V) L :=
    fractionRingToExtensionAlgebra (V := V) (K := K) (L := L)
  let : IsScalarTower (FractionRing V) K L :=
    fractionRingToChosenFractionFieldToExtension_isScalarTower
      (V := V) (K := K) (L := L)
  refine IsScalarTower.of_algebraMap_eq fun x ↦ ?_
  change algebraMap V L x =
    algebraMap K L
      (algebraMap (FractionRing V) K
        (algebraMap V (FractionRing V) x))
  rw [← IsScalarTower.algebraMap_apply V (FractionRing V) K,
    ← IsScalarTower.algebraMap_apply V K L]
theorem

fractionRingToExtension_finiteDimensional

L101 ↗
EtaleFundamentalGroups.fractionRingToExtension_finiteDimensional
Documentation

Finite dimensionality over a chosen fraction field transports to the literal fraction ring.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uV uK uL
variable {V : Type uV} {K : Type uK} {L : Type uL}
variable [CommRing V] [IsDomain V]
variable [Field K] [Algebra V K] [IsFractionRing V K]
variable [Field L] [Algebra K L]
variable [Algebra V L] [IsScalarTower V K L]
variable [FiniteDimensional K L]
omit [Algebra V L] [IsScalarTower V K L] in
Lean source · full declaration
theorem fractionRingToExtension_finiteDimensional :
    letI : Algebra (FractionRing V) L :=
      fractionRingToExtensionAlgebra (V := V) (K := K) (L := L)
    FiniteDimensional (FractionRing V) L := by
  let : Algebra (FractionRing V) K := FractionRing.liftAlgebra V K
  let : Algebra (FractionRing V) L :=
    fractionRingToExtensionAlgebra (V := V) (K := K) (L := L)
  let : IsScalarTower (FractionRing V) K L :=
    fractionRingToChosenFractionFieldToExtension_isScalarTower
      (V := V) (K := K) (L := L)
  let e : FractionRing V ≃ₐ[FractionRing V] K :=
    fractionRingChosenFractionFieldAlgEquiv (V := V) (K := K)
  let : Module.Finite (FractionRing V) K :=
    Module.Finite.of_surjective e.toLinearMap e.surjective
  exact Module.Finite.trans K L
theorem

fractionRingToExtension_isSeparable

L122 ↗
EtaleFundamentalGroups.fractionRingToExtension_isSeparable
Documentation

Separability over a chosen fraction field transports to the literal fraction ring.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uV uK uL
variable {V : Type uV} {K : Type uK} {L : Type uL}
variable [CommRing V] [IsDomain V]
variable [Field K] [Algebra V K] [IsFractionRing V K]
variable [Field L] [Algebra K L]
variable [Algebra V L] [IsScalarTower V K L]
variable [FiniteDimensional K L]
variable [Algebra.IsSeparable K L]
omit [Algebra V L] [IsScalarTower V K L] [FiniteDimensional K L] in
Lean source · full declaration
theorem fractionRingToExtension_isSeparable :
    letI : Algebra (FractionRing V) L :=
      fractionRingToExtensionAlgebra (V := V) (K := K) (L := L)
    Algebra.IsSeparable (FractionRing V) L := by
  let : Algebra (FractionRing V) K := FractionRing.liftAlgebra V K
  let : Algebra (FractionRing V) L :=
    fractionRingToExtensionAlgebra (V := V) (K := K) (L := L)
  let : IsScalarTower (FractionRing V) K L :=
    fractionRingToChosenFractionFieldToExtension_isScalarTower
      (V := V) (K := K) (L := L)
  let e : FractionRing V ≃ₐ[FractionRing V] K :=
    fractionRingChosenFractionFieldAlgEquiv (V := V) (K := K)
  let : Algebra.IsSeparable (FractionRing V) K :=
    AlgEquiv.Algebra.isSeparable e
  exact Algebra.IsSeparable.trans (FractionRing V) K L

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