Module

ArithmeticConstantsTensor.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.ArithmeticConstantsTensor

3 declarations indexed from sourceView source ↗

Module documentation

Dominance after adjoining arithmetic constants

An integral subring of a geometrically integral function field remains disjoint from the integers of a number field. This proves injectivity of the actual multiplication map used in the arithmetic constants argument.

Imports6

Mathlib.NumberTheory.NumberField.Basic
Mathlib.FieldTheory.LinearDisjoint
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.Algebra.Algebra.Subalgebra.Basic

Imported by2

def

ringOfIntegersToNormalDomain

L31 ↗

EtaleFundamentalGroups.ringOfIntegersToNormalDomain

Documentation

Algebraic integers in a constant subfield lie in a normal domain with the given fraction field. The map is constructed by restricting to the range of the original inclusion into the fraction field.

Source context 3 commands

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

noncomputable section
open scoped TensorProduct NumberField
namespace EtaleFundamentalGroups

Lean source · statement

def ringOfIntegersToNormalDomain
    (A K L : Type) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    [Field K] [NumberField K] [Field L] [CharZero L]
    [Algebra A L] [IsFractionRing A L] (g : K →ₐ[ℚ] L) :
    𝓞 K →ₐ[ℤ] A

theorem

algebraMap_ringOfIntegersToNormalDomain

L47 ↗

EtaleFundamentalGroups.algebraMap_ringOfIntegersToNormalDomain

Documentation

The constructed map of integer rings has the prescribed value in the original fraction field.

Source context 3 commands

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

noncomputable section
open scoped TensorProduct NumberField
namespace EtaleFundamentalGroups

Lean source · statement

theorem algebraMap_ringOfIntegersToNormalDomain
    (A K L : Type) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    [Field K] [NumberField K] [Field L] [CharZero L]
    [Algebra A L] [IsFractionRing A L] (g : K →ₐ[ℚ] L) (z : 𝓞 K) :
    algebraMap A L (ringOfIntegersToNormalDomain A K L g z) = g (z : K)

theorem

arithmeticConstantsTensor_lift_injective

L62 ↗

EtaleFundamentalGroups.arithmeticConstantsTensor_lift_injective

Documentation

An integral constant extension embeds in a common overfield when the corresponding rational tensor product is a domain.

Source context 3 commands

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

noncomputable section
open scoped TensorProduct NumberField
namespace EtaleFundamentalGroups

Lean source · full declaration

theorem arithmeticConstantsTensor_lift_injective
    {B F K L : Type} [CommRing B] [Field F] [CharZero F]
    [Field K] [NumberField K] [Field L] [CharZero L]
    (i : B →ₐ[ℤ] F) (hi : Function.Injective i)
    (f : F →ₐ[ℚ] L) (g : K →ₐ[ℚ] L)
    [IsDomain (F ⊗[ℚ] K)] :
    Function.Injective (Algebra.TensorProduct.lift
      ((f.restrictScalars ℤ).comp i)
      ((g.restrictScalars ℤ).comp (IsScalarTower.toAlgHom ℤ (𝓞 K) K))
      (fun _ _ ↦ Commute.all _ _)) := by
  let j : 𝓞 K →ₐ[ℤ] K := IsScalarTower.toAlgHom ℤ (𝓞 K) K
  let m : B ⊗[ℤ] (𝓞 K) →ₐ[ℤ] F ⊗[ℤ] K :=
    Algebra.TensorProduct.map i j
  have hm : Function.Injective m := by
    exact TensorProduct.map_injective_of_flat_flat i.toLinearMap j.toLinearMap
      hi (FaithfulSMul.algebraMap_injective (𝓞 K) K)
  let e : F ⊗[ℚ] K ≃ₐ[ℚ] F ⊗[ℤ] K :=
    IsLocalization.algebraTensorEquiv (nonZeroDivisors ℤ) ℚ F K
  let h : F ⊗[ℚ] K →ₐ[ℚ] L :=
    Algebra.TensorProduct.lift f g (fun _ _ ↦ Commute.all _ _)
  have hfield : IsField (F ⊗[ℚ] K) :=
    Algebra.TensorProduct.isField_of_isAlgebraic ℚ F K (.inr inferInstance)
  let : Field (F ⊗[ℚ] K) := hfield.toField
  have hh : Function.Injective h := h.injective
  have heq : (h.restrictScalars ℤ).comp ((e.symm.restrictScalars ℤ).toAlgHom.comp m) =
      Algebra.TensorProduct.lift ((f.restrictScalars ℤ).comp i)
        ((g.restrictScalars ℤ).comp (IsScalarTower.toAlgHom ℤ (𝓞 K) K))
        (fun _ _ ↦ Commute.all _ _) := by
    ext b <;> rfl
  rw [← heq]
  exact hh.comp (e.symm.injective.comp hm)

Module documentation

Dominance after adjoining arithmetic constants

Declarations

ringOfIntegersToNormalDomain

algebraMap_ringOfIntegersToNormalDomain

arithmeticConstantsTensor_lift_injective