NYLL
Module

DVRProductComponent.lean

Nyll.SchemeTheory.RingTheory.GenericFiber.DVRProductComponent
4 declarations indexed from sourceView source ↗

Module documentation

Chosen generic components of a product of DVRs

For a generic fibre of a product of DVRs, a maximal ideal whose contraction lies strictly below a specified coordinate maximal prime selects the fraction field of that same coordinate. The kernel identification is produced by the prime structure of the DVR factor, rather than supplied as an assumption.

Imports2
Imported by2

Declarations

def

genericFiberDVRProductComponentFractionRingEquiv

L36 ↗
EtaleFundamentalGroups.genericFiberDVRProductComponentFractionRingEquiv
Documentation

A chosen generic component lying strictly below the maximal prime of the i-th DVR factor is canonically the fraction field of that factor.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uK uι uA
variable {R : Type uR} {K : Type uK} {ι : Type uι}
variable (A : ι → Type uA)
variable [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K]
variable [∀ j, CommRing (A j)] [∀ j, IsDomain (A j)]
variable [∀ j, IsDiscreteValuationRing (A j)]
variable [∀ j, Algebra R (A j)]
Lean source · statement
def genericFiberDVRProductComponentFractionRingEquiv
    (i : ι) (m : Ideal (K ⊗[R] (∀ j, A j))) [m.IsMaximal]
    (hNP : genericFiberComponentBaseIdeal m ≤
      productCoordinatePrime A i)
    (hNne : genericFiberComponentBaseIdeal m ≠
      productCoordinatePrime A i) :
    ((K ⊗[R] (∀ j, A j)) ⧸ m) ≃+* FractionRing (A i)
theorem

genericFiberDVRProductComponentFractionRingEquiv_quotient_mk

L68 ↗
EtaleFundamentalGroups.genericFiberDVRProductComponentFractionRingEquiv_quotient_mk
Documentation

The coordinate identification sends the image of a tuple to the usual image of its selected coordinate in the fraction field.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uK uι uA
variable {R : Type uR} {K : Type uK} {ι : Type uι}
variable (A : ι → Type uA)
variable [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K]
variable [∀ j, CommRing (A j)] [∀ j, IsDomain (A j)]
variable [∀ j, IsDiscreteValuationRing (A j)]
variable [∀ j, Algebra R (A j)]
Lean source · statement
theorem genericFiberDVRProductComponentFractionRingEquiv_quotient_mk
    (i : ι) (m : Ideal (K ⊗[R] (∀ j, A j))) [m.IsMaximal]
    (hNP : genericFiberComponentBaseIdeal m ≤
      productCoordinatePrime A i)
    (hNne : genericFiberComponentBaseIdeal m ≠
      productCoordinatePrime A i)
    (x : ∀ j, A j) :
    genericFiberDVRProductComponentFractionRingEquiv A i m hNP hNne
        (genericFiberComponentQuotientRingHom m
          (Ideal.Quotient.mk (genericFiberComponentBaseIdeal m) x)) =
      algebraMap (A i) (FractionRing (A i)) (x i)
def

genericFiberDVRProductComponentFractionRingAlgEquiv

L108 ↗
EtaleFundamentalGroups.genericFiberDVRProductComponentFractionRingAlgEquiv
Documentation

The chosen coordinate identification is compatible with the original base ring. This algebra form is what normalization and ramification comparisons consume downstream.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uK uι uA
variable {R : Type uR} {K : Type uK} {ι : Type uι}
variable (A : ι → Type uA)
variable [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K]
variable [∀ j, CommRing (A j)] [∀ j, IsDomain (A j)]
variable [∀ j, IsDiscreteValuationRing (A j)]
variable [∀ j, Algebra R (A j)]
Lean source · statement
def genericFiberDVRProductComponentFractionRingAlgEquiv
    (i : ι) (m : Ideal (K ⊗[R] (∀ j, A j))) [m.IsMaximal]
    (hNP : genericFiberComponentBaseIdeal m ≤
      productCoordinatePrime A i)
    (hNne : genericFiberComponentBaseIdeal m ≠
      productCoordinatePrime A i) :
    ((K ⊗[R] (∀ j, A j)) ⧸ m) ≃ₐ[R] FractionRing (A i)
theorem

genericFiberDVRProductComponentFractionRingAlgEquiv_quotient_mk

L145 ↗
EtaleFundamentalGroups.genericFiberDVRProductComponentFractionRingAlgEquiv_quotient_mk
Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uK uι uA
variable {R : Type uR} {K : Type uK} {ι : Type uι}
variable (A : ι → Type uA)
variable [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K]
variable [∀ j, CommRing (A j)] [∀ j, IsDomain (A j)]
variable [∀ j, IsDiscreteValuationRing (A j)]
variable [∀ j, Algebra R (A j)]
Lean source · statement
theorem genericFiberDVRProductComponentFractionRingAlgEquiv_quotient_mk
    (i : ι) (m : Ideal (K ⊗[R] (∀ j, A j))) [m.IsMaximal]
    (hNP : genericFiberComponentBaseIdeal m ≤
      productCoordinatePrime A i)
    (hNne : genericFiberComponentBaseIdeal m ≠
      productCoordinatePrime A i)
    (x : ∀ j, A j) :
    genericFiberDVRProductComponentFractionRingAlgEquiv A i m hNP hNne
        (genericFiberComponentQuotientRingHom m
          (Ideal.Quotient.mk (genericFiberComponentBaseIdeal m) x)) =
      algebraMap (A i) (FractionRing (A i)) (x i)

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