NYLL
Module

ChosenComponentFractionRing.lean

Nyll.SchemeTheory.RingTheory.GenericFiber.ChosenComponentFractionRing
7 declarations indexed from sourceView source ↗

Module documentation

A chosen generic-fibre component as a fraction field

Let K be a fraction field of R, let U be an R-algebra, and let m be a maximal ideal of the generic fibre K ⊗[R] U. The quotient by m is canonically a fraction field of U modulo the contraction of m.

The construction keeps the specified ideal m: its map from the quotient of U is induced by the actual quotient map on the generic fibre. This is the bridge needed to compare a chosen generic component with a concrete domain factor of U once that contraction is identified with the kernel of the corresponding factor map.

Imports3
Imported by2

Declarations

def

genericFiberComponentBaseIdeal

L38 ↗
EtaleFundamentalGroups.genericFiberComponentBaseIdeal
Documentation

The contraction to U of a chosen ideal in the generic fibre.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uU uK
variable {R : Type uR} {U : Type uU} {K : Type uK}
variable [CommRing R] [CommRing U] [Algebra R U]
variable [Field K] [Algebra R K] [IsFractionRing R K]
Lean source · statement
def genericFiberComponentBaseIdeal
    (m : Ideal (K ⊗[R] U)) : Ideal U
def

genericFiberComponentQuotientRingHom

L45 ↗
EtaleFundamentalGroups.genericFiberComponentQuotientRingHom
Documentation

The canonical map from the quotient by the contracted ideal to the chosen generic-fibre quotient.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uU uK
variable {R : Type uR} {U : Type uU} {K : Type uK}
variable [CommRing R] [CommRing U] [Algebra R U]
variable [Field K] [Algebra R K] [IsFractionRing R K]
Lean source · statement
def genericFiberComponentQuotientRingHom
    (m : Ideal (K ⊗[R] U)) :
    (U ⧸ (genericFiberComponentBaseIdeal m)) →+* ((K ⊗[R] U) ⧸ m)
theorem

genericFiberComponentQuotientRingHom_mk

L54 ↗
EtaleFundamentalGroups.genericFiberComponentQuotientRingHom_mk
Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uU uK
variable {R : Type uR} {U : Type uU} {K : Type uK}
variable [CommRing R] [CommRing U] [Algebra R U]
variable [Field K] [Algebra R K] [IsFractionRing R K]
omit [IsFractionRing R K] in
Lean source · statement
theorem genericFiberComponentQuotientRingHom_mk
    (m : Ideal (K ⊗[R] U)) (x : U) :
    genericFiberComponentQuotientRingHom m
        (Ideal.Quotient.mk (genericFiberComponentBaseIdeal m) x) =
      Ideal.Quotient.mk m
        ((Algebra.TensorProduct.includeRight : U →ₐ[R] K ⊗[R] U) x)
theorem

genericFiberComponentQuotientRingHom_injective

L65 ↗
EtaleFundamentalGroups.genericFiberComponentQuotientRingHom_injective
Documentation

The canonical map from the contracted quotient is injective.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uU uK
variable {R : Type uR} {U : Type uU} {K : Type uK}
variable [CommRing R] [CommRing U] [Algebra R U]
variable [Field K] [Algebra R K] [IsFractionRing R K]
omit [IsFractionRing R K] in
Lean source · statement
theorem genericFiberComponentQuotientRingHom_injective
    (m : Ideal (K ⊗[R] U)) :
    Function.Injective (genericFiberComponentQuotientRingHom m)
theorem

genericFiberComponentQuotient_isFractionRing

L76 ↗
EtaleFundamentalGroups.genericFiberComponentQuotient_isFractionRing
Documentation

A field component selected by a maximal generic-fibre ideal is a fraction field of the quotient by its contraction to the original algebra.

This is produced directly from the localization presentation K ⊗[R] U: denominators are images of non-zero elements of R, and no such denominator can lie in the contraction of a proper ideal upstairs.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uU uK
variable {R : Type uR} {U : Type uU} {K : Type uK}
variable [CommRing R] [CommRing U] [Algebra R U]
variable [Field K] [Algebra R K] [IsFractionRing R K]
Lean source · full declaration
theorem genericFiberComponentQuotient_isFractionRing
    (m : Ideal (K ⊗[R] U)) [m.IsMaximal] :
    let N := genericFiberComponentBaseIdeal m
    let Ω := ((K ⊗[R] U) ⧸ m)
    letI : Algebra (U ⧸ N) Ω :=
      (genericFiberComponentQuotientRingHom m).toAlgebra
    IsFractionRing (U ⧸ N) Ω := by
  let G := K ⊗[R] U
  let N := genericFiberComponentBaseIdeal m
  let Ω := G ⧸ m
  let M : Submonoid U :=
    Algebra.algebraMapSubmonoid U (nonZeroDivisors R)
  let : Algebra U G := Algebra.TensorProduct.rightAlgebra
  let : IsLocalization M G :=
    IsLocalization.tensorRight (R := R) (S := U) (A := K)
      (nonZeroDivisors R)
  let : m.IsPrime :=
    Ideal.IsMaximal.isPrime (inferInstance : m.IsMaximal)
  let : N.IsPrime := (inferInstance : m.IsPrime).comap
    (Algebra.TensorProduct.includeRight : U →ₐ[R] G).toRingHom
  let : Field Ω := Ideal.Quotient.field m
  let : Algebra (U ⧸ N) Ω :=
    (genericFiberComponentQuotientRingHom m).toAlgebra
  let : FaithfulSMul (U ⧸ N) Ω :=
    (faithfulSMul_iff_algebraMap_injective (U ⧸ N) Ω).mpr
      (genericFiberComponentQuotientRingHom_injective m)
  have hdisjoint : Disjoint (M : Set U) (N : Set U) := by
    rw [Set.disjoint_left]
    intro x hxM hxN
    have hxIdeal : algebraMap U G x ∈ m := hxN
    exact (inferInstance : m.IsPrime).ne_top
      (Ideal.eq_top_of_isUnit_mem m hxIdeal
        (IsLocalization.map_units G ⟨x, hxM⟩))
  apply IsFractionRing.of_field
  intro z
  obtain ⟨t, rfl⟩ := Ideal.Quotient.mk_surjective z
  obtain ⟨⟨x, s⟩, ht⟩ := IsLocalization.surj M t
  refine ⟨Ideal.Quotient.mk N x, Ideal.Quotient.mk N s, ?_⟩
  refine (eq_div_iff ?_).2 ?_
  · apply (map_ne_zero_iff _
      (FaithfulSMul.algebraMap_injective (U ⧸ N) Ω)).2
    intro hs
    have hsN : (s : U) ∈ N := Ideal.Quotient.eq_zero_iff_mem.mp hs
    exact (Set.disjoint_left.mp hdisjoint) s.property hsN
  · change Ideal.Quotient.mk m t * algebraMap U Ω s =
      algebraMap U Ω x
    simpa using congrArg (Ideal.Quotient.mk m) ht
def

genericFiberComponentFractionRingEquiv

L126 ↗
EtaleFundamentalGroups.genericFiberComponentFractionRingEquiv
Documentation

The canonical identification of a chosen generic-fibre component with the fraction ring of the quotient by its contracted prime.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uU uK
variable {R : Type uR} {U : Type uU} {K : Type uK}
variable [CommRing R] [CommRing U] [Algebra R U]
variable [Field K] [Algebra R K] [IsFractionRing R K]
Lean source · statement
def genericFiberComponentFractionRingEquiv
    (m : Ideal (K ⊗[R] U)) [m.IsMaximal] :
    ((K ⊗[R] U) ⧸ m) ≃+*
      FractionRing (U ⧸ genericFiberComponentBaseIdeal m)
theorem

genericFiberComponentFractionRingEquiv_quotient_mk

L145 ↗
EtaleFundamentalGroups.genericFiberComponentFractionRingEquiv_quotient_mk
Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uU uK
variable {R : Type uR} {U : Type uU} {K : Type uK}
variable [CommRing R] [CommRing U] [Algebra R U]
variable [Field K] [Algebra R K] [IsFractionRing R K]
Lean source · statement
theorem genericFiberComponentFractionRingEquiv_quotient_mk
    (m : Ideal (K ⊗[R] U)) [m.IsMaximal] (x : U) :
    genericFiberComponentFractionRingEquiv m
        (genericFiberComponentQuotientRingHom m
          (Ideal.Quotient.mk (genericFiberComponentBaseIdeal m) x)) =
      algebraMap (U ⧸ genericFiberComponentBaseIdeal m)
        (FractionRing (U ⧸ genericFiberComponentBaseIdeal m))
        (Ideal.Quotient.mk (genericFiberComponentBaseIdeal m) x)

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