NYLL
Module

FractionRing.lean

Nyll.SchemeTheory.RingTheory.GenericFiber.FractionRing
3 declarations indexed from sourceView source ↗

Module documentation

Fraction fields from generic-fibre equivalences

An equivalence between the generic fibre K ⊗[R] C and a field E canonically embeds C in E. When C is a domain, this embedding makes E a fraction field of C.

Imports2
  • Mathlib.RingTheory.Localization.BaseChange
  • Mathlib.RingTheory.Localization.FractionRing
Imported by3

Declarations

def

genericFiberRightAlgHom

L28 ↗
EtaleFundamentalGroups.genericFiberRightAlgHom
Documentation

The canonical map from the right-hand algebra into a field identified with its generic fibre.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uK uE
Lean source · statement
def genericFiberRightAlgHom
    {R : Type uR} {C : Type uC} {K : Type uK} {E : Type uE}
    [CommRing R] [CommRing C] [Algebra R C]
    [Field K] [Algebra R K]
    [Field E] [Algebra K E] [Algebra R E] [IsScalarTower R K E]
    (e : (K ⊗[R] C) ≃ₐ[K] E) :
    C →ₐ[R] E
theorem

genericFiberRightAlgHom_apply

L38 ↗
EtaleFundamentalGroups.genericFiberRightAlgHom_apply
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uK uE
Lean source · statement
theorem genericFiberRightAlgHom_apply
    {R : Type uR} {C : Type uC} {K : Type uK} {E : Type uE}
    [CommRing R] [CommRing C] [Algebra R C]
    [Field K] [Algebra R K]
    [Field E] [Algebra K E] [Algebra R E] [IsScalarTower R K E]
    (e : (K ⊗[R] C) ≃ₐ[K] E) (c : C) :
    genericFiberRightAlgHom e c = e (1 ⊗ₜ[R] c)
theorem

isFractionRing_of_genericFiberAlgEquiv

L53 ↗
EtaleFundamentalGroups.isFractionRing_of_genericFiberAlgEquiv
Documentation

A field identified with the generic fibre of a domain is a fraction field of that domain, for the canonical right-factor embedding.

No finiteness assumption is needed: the existence of the field-valued generic-fibre equivalence already forces the required localization to be a field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uK uE
Lean source · full declaration
theorem isFractionRing_of_genericFiberAlgEquiv
    {R : Type uR} {C : Type uC} {K : Type uK} {E : Type uE}
    [CommRing R] [CommRing C] [IsDomain C] [Algebra R C]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field E] [Algebra K E] [Algebra R E] [IsScalarTower R K E]
    (e : (K ⊗[R] C) ≃ₐ[K] E) :
    letI : Algebra C E :=
      (genericFiberRightAlgHom e).toRingHom.toAlgebra
    IsFractionRing C E := by
  let M : Submonoid C :=
    Algebra.algebraMapSubmonoid C (nonZeroDivisors R)
  let T := K ⊗[R] C
  let f : C →ₐ[R] E := genericFiberRightAlgHom e
  let : Algebra C E := f.toRingHom.toAlgebra
  have hRE : Function.Injective (algebraMap R E) := by
    rw [IsScalarTower.algebraMap_eq R K E]
    exact (algebraMap K E).injective.comp
      (FaithfulSMul.algebraMap_injective R K)
  let : IsDomain R := hRE.isDomain _
  have hRC : Function.Injective (algebraMap R C) := by
    intro x y hxy
    apply hRE
    calc
      algebraMap R E x = f (algebraMap R C x) := (f.commutes x).symm
      _ = f (algebraMap R C y) := by rw [hxy]
      _ = algebraMap R E y := f.commutes y
  have hM : M ≤ nonZeroDivisors C := by
    rintro _ ⟨r, hr, rfl⟩
    have hr0 : r ≠ 0 := mem_nonZeroDivisors_iff_ne_zero.mp hr
    rw [mem_nonZeroDivisors_iff_ne_zero]
    intro h
    exact hr0 (hRC (by simpa using h))
  let : Algebra C T := Algebra.TensorProduct.rightAlgebra
  let : IsLocalization M T :=
    IsLocalization.tensorRight (R := R) (S := C) (A := K)
      (nonZeroDivisors R)
  let eC : T ≃ₐ[C] E :=
    { e with
      commutes' := fun c ↦ rfl }
  let : IsLocalization M E :=
    IsLocalization.isLocalization_of_algEquiv M eC
  let : FaithfulSMul C E :=
    (faithfulSMul_iff_algebraMap_injective C E).mpr
      (IsLocalization.injective E hM)
  apply IsFractionRing.of_field
  intro z
  obtain ⟨⟨x, s⟩, hz⟩ := IsLocalization.surj M z
  refine ⟨x, s, (eq_div_iff ?_).2 ?_⟩
  · exact (IsLocalization.map_units E s).ne_zero
  · simpa using hz

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