NYLL
Module

LocalRingFactor.lean

Nyll.SchemeTheory.Normalization.Products.LocalRingFactor
22 declarations indexed from sourceView source ↗

Module documentation

Extracting a local factor from a product by localization

For a family of local rings A, the inverse image of the maximal ideal of A i under evaluation at i is a maximal ideal of the product. Localization of the product at this ideal canonically recovers A i.

The construction does not require the index type to be finite; in particular, it applies to the finite products arising from Chinese-remainder decompositions.

Imports2
  • Mathlib.RingTheory.LocalRing.RingHom.Basic
  • Mathlib.RingTheory.Localization.AtPrime.Basic
Imported by4

Declarations

abbrev

productCoordinatePrime

L31 ↗
EtaleFundamentalGroups.productCoordinatePrime
Documentation

The prime of a product selected by the maximal ideal in coordinate i.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
abbrev productCoordinatePrime [∀ j, IsLocalRing (A j)] : Ideal (∀ j, A j)
instance

(anonymous instance)

L34 ↗
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
instance [∀ j, IsLocalRing (A j)] : (productCoordinatePrime A i).IsPrime
instance

(anonymous instance)

L38 ↗
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
instance [∀ j, IsLocalRing (A j)] : (productCoordinatePrime A i).IsMaximal
theorem

mem_productCoordinatePrime

L42 ↗
EtaleFundamentalGroups.mem_productCoordinatePrime
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
theorem mem_productCoordinatePrime [∀ j, IsLocalRing (A j)] (x : ∀ j, A j) :
    x ∈ productCoordinatePrime A i ↔ x i ∈ IsLocalRing.maximalIdeal (A i)
theorem

ker_productCoordinateEval

L48 ↗
EtaleFundamentalGroups.ker_productCoordinateEval
Documentation

The kernel of the coordinate map is generated by the complementary idempotent.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
theorem ker_productCoordinateEval [DecidableEq ι] :
    RingHom.ker (Pi.evalRingHom A i) =
      Ideal.span ({1 - Pi.single i 1} : Set (∀ j, A j))
instance

productCoordinateAlgebra

L55 ↗
EtaleFundamentalGroups.productCoordinateAlgebra
Documentation

The canonical algebra structure on a selected coordinate of a product.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
instance productCoordinateAlgebra : Algebra (∀ j, A j) (A i)
theorem

productCoordinate_algebraMap_apply

L59 ↗
EtaleFundamentalGroups.productCoordinate_algebraMap_apply
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
theorem productCoordinate_algebraMap_apply (x : ∀ j, A j) :
    algebraMap (∀ j, A j) (A i) x = x i
def

productAtPrimeToFactorAtPrimeRingEquiv

L63 ↗
EtaleFundamentalGroups.productAtPrimeToFactorAtPrimeRingEquiv
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
def productAtPrimeToFactorAtPrimeRingEquiv
    [∀ j, IsLocalRing (A j)] :
    Localization.AtPrime (productCoordinatePrime A i) ≃+*
      Localization.AtPrime (IsLocalRing.maximalIdeal (A i))
def

factorAtMaximalAlgEquiv

L72 ↗
EtaleFundamentalGroups.factorAtMaximalAlgEquiv
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
def factorAtMaximalAlgEquiv [∀ j, IsLocalRing (A j)] :
    A i ≃ₐ[A i] Localization.AtPrime (IsLocalRing.maximalIdeal (A i))
def

productCoordinateAtPrimeRingEquiv

L79 ↗
EtaleFundamentalGroups.productCoordinateAtPrimeRingEquiv
Documentation

Localization at the maximal ideal selected by coordinate i canonically recovers that local-ring factor.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
def productCoordinateAtPrimeRingEquiv [∀ j, IsLocalRing (A j)] :
    Localization.AtPrime (productCoordinatePrime A i) ≃+* A i
def

productCoordinateAtPrimeAlgEquiv

L86 ↗
EtaleFundamentalGroups.productCoordinateAtPrimeAlgEquiv
Documentation

The canonical equivalence with the selected factor, as an algebra over the whole product via coordinate evaluation.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
def productCoordinateAtPrimeAlgEquiv [∀ j, IsLocalRing (A j)] :
    Localization.AtPrime (productCoordinatePrime A i) ≃ₐ[(∀ j, A j)] A i
instance

productCoordinate_isLocalization

L98 ↗
EtaleFundamentalGroups.productCoordinate_isLocalization
Documentation

Coordinate evaluation exhibits the selected local factor itself as the localization of the product at the complement of productCoordinatePrime.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
instance productCoordinate_isLocalization [∀ j, IsLocalRing (A j)] :
    IsLocalization (productCoordinatePrime A i).primeCompl (A i)
theorem

productCoordinateAtPrimeAlgEquiv_algebraMap_apply

L105 ↗
EtaleFundamentalGroups.productCoordinateAtPrimeAlgEquiv_algebraMap_apply
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
theorem productCoordinateAtPrimeAlgEquiv_algebraMap_apply
    [∀ j, IsLocalRing (A j)] (x : ∀ j, A j) :
    productCoordinateAtPrimeAlgEquiv A i
        (algebraMap (∀ j, A j)
          (Localization.AtPrime (productCoordinatePrime A i)) x) = x i
theorem

productCoordinateAtPrimeRingEquiv_map_maximalIdeal

L113 ↗
EtaleFundamentalGroups.productCoordinateAtPrimeRingEquiv_map_maximalIdeal
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
Lean source · statement
theorem productCoordinateAtPrimeRingEquiv_map_maximalIdeal
    [∀ j, IsLocalRing (A j)] :
    (IsLocalRing.maximalIdeal
        (Localization.AtPrime (productCoordinatePrime A i))).map
        (productCoordinateAtPrimeRingEquiv A i) =
      IsLocalRing.maximalIdeal (A i)
abbrev

ringEquivProductCoordinatePrime

L128 ↗
EtaleFundamentalGroups.ringEquivProductCoordinatePrime
Documentation

The coordinate prime pulled back across a ring equivalence with a product.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
section RingEquivTransport
universe uU
variable {U : Type uU} [CommRing U]
Lean source · statement
abbrev ringEquivProductCoordinatePrime [∀ j, IsLocalRing (A j)]
    (e : U ≃+* (∀ j, A j)) : Ideal U
def

ringEquivProductCoordinateAlgebra

L135 ↗
EtaleFundamentalGroups.ringEquivProductCoordinateAlgebra
Documentation

The selected factor as an algebra over a ring identified with the whole product.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
section RingEquivTransport
universe uU
variable {U : Type uU} [CommRing U]
Lean source · statement
def ringEquivProductCoordinateAlgebra
    (e : U ≃+* (∀ j, A j)) : Algebra U (A i)
theorem

ringEquivProductCoordinate_algebraMap_apply

L140 ↗
EtaleFundamentalGroups.ringEquivProductCoordinate_algebraMap_apply
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
section RingEquivTransport
universe uU
variable {U : Type uU} [CommRing U]
Lean source · full declaration
theorem ringEquivProductCoordinate_algebraMap_apply
    (e : U ≃+* (∀ j, A j)) (x : U) :
    letI : Algebra U (A i) := ringEquivProductCoordinateAlgebra A i e
    algebraMap U (A i) x = e x i :=
  rfl
def

ringEquivProductCoordinateBaseAlgebra

L153 ↗
EtaleFundamentalGroups.ringEquivProductCoordinateBaseAlgebra
Documentation

The base-ring algebra on a selected coordinate obtained through the pulled-back product presentation.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
section RingEquivTransport
universe uU
variable {U : Type uU} [CommRing U]
universe uR
variable {R : Type uR} [CommRing R] [Algebra R U]
Lean source · statement
def ringEquivProductCoordinateBaseAlgebra
    (e : U ≃+* (∀ j, A j)) : Algebra R (A i)
theorem

ringEquivProductCoordinate_isScalarTower

L158 ↗
EtaleFundamentalGroups.ringEquivProductCoordinate_isScalarTower
Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
section RingEquivTransport
universe uU
variable {U : Type uU} [CommRing U]
universe uR
variable {R : Type uR} [CommRing R] [Algebra R U]
Lean source · full declaration
theorem ringEquivProductCoordinate_isScalarTower
    (e : U ≃+* (∀ j, A j)) :
    letI : Algebra U (A i) := ringEquivProductCoordinateAlgebra A i e
    letI : Algebra R (A i) :=
      ringEquivProductCoordinateBaseAlgebra (R := R) A i e
    IsScalarTower R U (A i) := by
  let : Algebra U (A i) := ringEquivProductCoordinateAlgebra A i e
  let : Algebra R (A i) :=
    ringEquivProductCoordinateBaseAlgebra (R := R) A i e
  exact IsScalarTower.of_algebraMap_eq fun _ => rfl
theorem

map_symm_primeCompl_eq

L169 ↗
EtaleFundamentalGroups.map_symm_primeCompl_eq
Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
section RingEquivTransport
universe uU
variable {U : Type uU} [CommRing U]
universe uR
variable {R : Type uR} [CommRing R] [Algebra R U]
Lean source · statement
theorem map_symm_primeCompl_eq
    [∀ j, IsLocalRing (A j)] (e : U ≃+* (∀ j, A j)) :
    Submonoid.map e.symm.toMonoidHom
        (productCoordinatePrime A i).primeCompl =
      (ringEquivProductCoordinatePrime A i e).primeCompl
theorem

ringEquivProductCoordinate_isLocalization

L187 ↗
EtaleFundamentalGroups.ringEquivProductCoordinate_isLocalization
Documentation

A local factor of a product remains the corresponding localization after pulling the product presentation back along a ring equivalence.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
section RingEquivTransport
universe uU
variable {U : Type uU} [CommRing U]
universe uR
variable {R : Type uR} [CommRing R] [Algebra R U]
Lean source · full declaration
theorem ringEquivProductCoordinate_isLocalization
    [∀ j, IsLocalRing (A j)] (e : U ≃+* (∀ j, A j)) :
    letI : Algebra U (A i) := ringEquivProductCoordinateAlgebra A i e
    IsLocalization (ringEquivProductCoordinatePrime A i e).primeCompl (A i) := by
  let : Algebra U (A i) := ringEquivProductCoordinateAlgebra A i e
  have hloc : IsLocalization
      (Submonoid.map e.symm.toMonoidHom
        (productCoordinatePrime A i).primeCompl) (A i) := by
    apply IsLocalization.of_surjective
      (productCoordinatePrime A i).primeCompl (A i)
      e.symm.toRingHom e.symm.surjective (RingHom.id (A i))
      Function.bijective_id.surjective
    · ext x
      change x i = e (e.symm x) i
      rw [e.apply_symm_apply]
    · intro x hx
      change x = 0 at hx
      subst x
      exact Ideal.zero_mem _
  rw [map_symm_primeCompl_eq A i e] at hloc
  exact hloc
theorem

ringEquivProductCoordinatePrime_map

L210 ↗
EtaleFundamentalGroups.ringEquivProductCoordinatePrime_map
Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA) [∀ j, CommRing (A j)]
variable (i : ι)
section RingEquivTransport
universe uU
variable {U : Type uU} [CommRing U]
universe uR
variable {R : Type uR} [CommRing R] [Algebra R U]
Lean source · full declaration
theorem ringEquivProductCoordinatePrime_map
    [∀ j, IsLocalRing (A j)] (e : U ≃+* (∀ j, A j)) :
    letI : Algebra U (A i) := ringEquivProductCoordinateAlgebra A i e
    (ringEquivProductCoordinatePrime A i e).map
        (algebraMap U (A i)) = IsLocalRing.maximalIdeal (A i) := by
  let : Algebra U (A i) := ringEquivProductCoordinateAlgebra A i e
  change Ideal.map ((Pi.evalRingHom A i).comp e.toRingHom)
      (Ideal.comap e.toRingHom
        (Ideal.comap (Pi.evalRingHom A i)
          (IsLocalRing.maximalIdeal (A i)))) =
    IsLocalRing.maximalIdeal (A i)
  rw [Ideal.comap_comap]
  have hf : Function.Surjective
      ((Pi.evalRingHom A i).comp e.toRingHom) := by
    intro y
    obtain ⟨x, hx⟩ := (Pi.evalRingHom A i).surjective y
    obtain ⟨z, rfl⟩ := e.surjective x
    exact ⟨z, hx⟩
  exact Ideal.map_comap_of_surjective _ hf _

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