NYLL
Module

GenericComponent.lean

Nyll.EtaleFundamentalGroups.Completions.Chosen.GenericComponent
17 declarations indexed from sourceView source ↗

Module documentation

A completed generic component selected by a closed prime

Let C / R be a finite extension of domains, with R a DVR, and let Q be a maximal ideal of C above the closed point. For a faithfully flat local base change R → R' which preserves the closed point and residue field, the extension of Q to R' ⊗[R] C is a maximal ideal P; it contracts to exactly Q and has the same ramification index.

Flat going-down selects a generic prime below this specified P. After inverting the nonzero elements of R', it becomes a maximal ideal of the completed generic fibre. The resulting field component is therefore fixed once from Q, rather than being replaced by an unrelated tensor component.

Imports7
Imported by4

Declarations

abbrev

completedFiniteBaseChange

L46 ↗
EtaleFundamentalGroups.completedFiniteBaseChange
Documentation

The finite model after the completed base change.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
Lean source · statement
abbrev completedFiniteBaseChange
def

completedBaseChangeChosenPrime

L49 ↗
EtaleFundamentalGroups.completedBaseChangeChosenPrime
Documentation

The closed prime in the finite completed model selected by Q.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
Lean source · statement
def completedBaseChangeChosenPrime
    (Q : Ideal C) : Ideal (completedFiniteBaseChange
      (R := R) (R' := R') (C := C))
theorem

completedBaseChangeChosenPrime_isMaximal_liesOver

L60 ↗
EtaleFundamentalGroups.completedBaseChangeChosenPrime_isMaximal_liesOver
Documentation

Closed-point and residue-field preservation make the extension of Q a maximal ideal over the closed point of R'.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
omit [IsDomain R'] [IsDomain C] [Module.Finite R C]
  [FaithfulSMul R C] in
Lean source · full declaration
theorem completedBaseChangeChosenPrime_isMaximal_liesOver
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    let P := completedBaseChangeChosenPrime
      (R := R) (R' := R') Q
    P.IsMaximal ∧ P.LiesOver (IsLocalRing.maximalIdeal R') := by
  simpa [completedBaseChangeChosenPrime, completedFiniteBaseChange] using
    (tensorProduct_map_liesOver_maximalIdeal_of_residueFieldMap_bijective
      (R := R) (R' := R') Q hmax hres)
theorem

completedBaseChangeChosenPrime_comap_right

L78 ↗
EtaleFundamentalGroups.completedBaseChangeChosenPrime_comap_right
Documentation

The selected completed closed prime contracts to the specified Q.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
omit [IsDomain R] [IsDiscreteValuationRing R] [IsDomain R']
  [IsLocalRing R'] [IsLocalHom (algebraMap R R')] [IsDomain C]
  [Module.Finite R C] [FaithfulSMul R C] in
Lean source · full declaration
theorem completedBaseChangeChosenPrime_comap_right
    (Q : Ideal C) :
    let U := completedFiniteBaseChange (R := R) (R' := R') (C := C)
    letI : Algebra C U := Algebra.TensorProduct.rightAlgebra
    (completedBaseChangeChosenPrime (R := R) (R' := R') Q).comap
        (algebraMap C U) = Q := by
  let U := completedFiniteBaseChange (R := R) (R' := R') (C := C)
  let : Algebra C U := Algebra.TensorProduct.rightAlgebra
  let : Module.FaithfullyFlat C U :=
    Module.FaithfullyFlat.of_linearEquiv
      (R := C) (M := C ⊗[R] R')
      (Algebra.TensorProduct.commRight R C R').symm.toLinearEquiv
  simpa only [completedBaseChangeChosenPrime] using
    (Ideal.comap_map_eq_self_of_faithfullyFlat (B := U) Q)
theorem

completedBaseChangeChosenPrime_ramificationIdx_eq

L96 ↗
EtaleFundamentalGroups.completedBaseChangeChosenPrime_ramificationIdx_eq
Documentation

Ramification at the selected completed closed prime is exactly the ramification at the original Q.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
omit [IsDomain R'] in
Lean source · statement
theorem completedBaseChangeChosenPrime_ramificationIdx_eq
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    (completedBaseChangeChosenPrime (R := R) (R' := R') Q).ramificationIdx R' =
      Q.ramificationIdx R
theorem

exists_completedBaseChangeChosenGenericPrime

L126 ↗
EtaleFundamentalGroups.exists_completedBaseChangeChosenGenericPrime
Documentation

A generic prime of the finite base change lying below the closed prime selected by Q.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
Lean source · full declaration
theorem exists_completedBaseChangeChosenGenericPrime
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    let U := completedFiniteBaseChange (R := R) (R' := R') (C := C)
    let P := completedBaseChangeChosenPrime (R := R) (R' := R') Q
    ∃ N : Ideal U, N ≤ P ∧ N.IsPrime ∧ N.LiesOver (⊥ : Ideal R') := by
  let U := completedFiniteBaseChange (R := R) (R' := R') (C := C)
  let P := completedBaseChangeChosenPrime (R := R) (R' := R') Q
  let : Module.Flat R C := inferInstance
  let : Module.Flat R' U := Module.Flat.baseChange R R' C
  have hgeom := completedBaseChangeChosenPrime_isMaximal_liesOver
    (R := R) (R' := R') hmax hres Q
  let : P.IsPrime := hgeom.1.isPrime
  let : P.LiesOver (IsLocalRing.maximalIdeal R') := hgeom.2
  obtain ⟨N, hNP, hNprime, hNover⟩ :=
    Ideal.exists_ideal_le_liesOver_of_le
      (R := R') (S := U) (p := (⊥ : Ideal R'))
      (q := IsLocalRing.maximalIdeal R') P bot_le
  exact ⟨N, hNP, hNprime, hNover⟩
def

completedBaseChangeChosenGenericPrime

L152 ↗
EtaleFundamentalGroups.completedBaseChangeChosenGenericPrime
Documentation

The fixed generic prime below the completed closed point selected by Q.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
Lean source · statement
def completedBaseChangeChosenGenericPrime
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    Ideal (completedFiniteBaseChange (R := R) (R' := R') (C := C))
theorem

completedBaseChangeChosenGenericPrime_spec

L163 ↗
EtaleFundamentalGroups.completedBaseChangeChosenGenericPrime_spec
Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
Lean source · full declaration
theorem completedBaseChangeChosenGenericPrime_spec
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    let P := completedBaseChangeChosenPrime (R := R) (R' := R') Q
    let N := completedBaseChangeChosenGenericPrime
      (R := R) (R' := R') hmax hres Q
    N ≤ P ∧ N.IsPrime ∧ N.LiesOver (⊥ : Ideal R') :=
  Classical.choose_spec (exists_completedBaseChangeChosenGenericPrime
    (R := R) (R' := R') hmax hres Q)
abbrev

completedFiniteBaseChangeGenericFiber

L183 ↗
EtaleFundamentalGroups.completedFiniteBaseChangeGenericFiber
Documentation

The generic fibre of the finite completed model.

Source context 13 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
section GenericFibre
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
Lean source · statement
abbrev completedFiniteBaseChangeGenericFiber
def

completedBaseChangeChosenGenericIdeal

L188 ↗
EtaleFundamentalGroups.completedBaseChangeChosenGenericIdeal
Documentation

Extend the fixed generic prime below P to the completed generic fibre.

Source context 13 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
section GenericFibre
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
Lean source · statement
def completedBaseChangeChosenGenericIdeal
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    Ideal (completedFiniteBaseChangeGenericFiber
      (R := R) (R' := R') (C := C) (K' := K'))
theorem

completedBaseChangeChosenGenericPrime_disjoint

L204 ↗
EtaleFundamentalGroups.completedBaseChangeChosenGenericPrime_disjoint
Source context 13 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
section GenericFibre
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
Lean source · full declaration
theorem completedBaseChangeChosenGenericPrime_disjoint
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    let U := completedFiniteBaseChange (R := R) (R' := R') (C := C)
    Disjoint
      (Algebra.algebraMapSubmonoid U (nonZeroDivisors R') : Set U)
      (completedBaseChangeChosenGenericPrime
        (R := R) (R' := R') hmax hres Q : Set U) := by
  let U := completedFiniteBaseChange (R := R) (R' := R') (C := C)
  let N := completedBaseChangeChosenGenericPrime
    (R := R) (R' := R') hmax hres Q
  have hN := completedBaseChangeChosenGenericPrime_spec
    (R := R) (R' := R') hmax hres Q
  let : N.IsPrime := hN.2.1
  let : N.LiesOver (⊥ : Ideal R') := hN.2.2
  rw [Set.disjoint_left]
  intro x hxM hxN
  rcases hxM with ⟨r, hr, rfl⟩
  have hrN : r ∈ N.under R' := hxN
  have hr0 : r = 0 := by
    have : r ∈ (⊥ : Ideal R') := by
      rw [N.over_def (⊥ : Ideal R')]
      exact hrN
    simpa only [Ideal.mem_bot] using this
  exact (nonZeroDivisors.coe_ne_zero ⟨r, hr⟩) hr0
theorem

completedBaseChangeChosenGenericIdeal_isMaximal

L234 ↗
EtaleFundamentalGroups.completedBaseChangeChosenGenericIdeal_isMaximal
Source context 13 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
section GenericFibre
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
Lean source · statement
theorem completedBaseChangeChosenGenericIdeal_isMaximal
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    (completedBaseChangeChosenGenericIdeal
      (R := R) (R' := R') (K' := K') hmax hres Q).IsMaximal
theorem

completedBaseChangeChosenGenericIdeal_comap

L277 ↗
EtaleFundamentalGroups.completedBaseChangeChosenGenericIdeal_comap
Documentation

Contracting the completed generic ideal recovers the fixed generic prime below the Q-selected closed point.

Source context 13 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
section GenericFibre
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
Lean source · full declaration
theorem completedBaseChangeChosenGenericIdeal_comap
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    let U := completedFiniteBaseChange (R := R) (R' := R') (C := C)
    let G := completedFiniteBaseChangeGenericFiber
      (R := R) (R' := R') (C := C) (K' := K')
    letI : Algebra U G := Algebra.TensorProduct.rightAlgebra
    (completedBaseChangeChosenGenericIdeal
        (R := R) (R' := R') (K' := K') hmax hres Q).comap
        (algebraMap U G) =
      completedBaseChangeChosenGenericPrime
        (R := R) (R' := R') hmax hres Q := by
  let U := completedFiniteBaseChange (R := R) (R' := R') (C := C)
  let G := completedFiniteBaseChangeGenericFiber
    (R := R) (R' := R') (C := C) (K' := K')
  let N := completedBaseChangeChosenGenericPrime
    (R := R) (R' := R') hmax hres Q
  let : Algebra U G := Algebra.TensorProduct.rightAlgebra
  let : IsLocalization
      (Algebra.algebraMapSubmonoid U (nonZeroDivisors R')) G :=
    IsLocalization.tensorRight (R := R') (S := U) (A := K')
      (nonZeroDivisors R')
  have hN := completedBaseChangeChosenGenericPrime_spec
    (R := R) (R' := R') hmax hres Q
  exact IsLocalization.under_map_of_isPrime_disjoint
    (Algebra.algebraMapSubmonoid U (nonZeroDivisors R')) G
    hN.2.1
    (completedBaseChangeChosenGenericPrime_disjoint
      (R := R) (R' := R') hmax hres Q)
def

completedGenericFiberEquiv

L323 ↗
EtaleFundamentalGroups.completedGenericFiberEquiv
Documentation

Reassociate the completed generic fibre with the usual field tensor K' ⊗[K] L.

Source context 21 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
section GenericFibre
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
section OriginalGenericTensor
variable {K : Type uK} {L : Type uL}
variable [Field K] [Algebra R K] [IsFractionRing R K]
variable [Field L] [Algebra C L] [IsFractionRing C L]
variable [Algebra R L] [IsScalarTower R C L]
variable [Algebra K L] [IsScalarTower R K L]
variable [Algebra R K'] [IsScalarTower R R' K']
variable [Algebra K K'] [IsScalarTower R K K']
Lean source · statement
def completedGenericFiberEquiv :
    completedFiniteBaseChangeGenericFiber
        (R := R) (R' := R') (C := C) (K' := K') ≃ₐ[K']
      (K' ⊗[K] L)
def

completedGenericTensorChosenIdeal

L342 ↗
EtaleFundamentalGroups.completedGenericTensorChosenIdeal
Documentation

The maximal ideal of K' ⊗[K] L obtained from the generic prime below the completed closed point selected by Q.

Source context 21 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
section GenericFibre
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
section OriginalGenericTensor
variable {K : Type uK} {L : Type uL}
variable [Field K] [Algebra R K] [IsFractionRing R K]
variable [Field L] [Algebra C L] [IsFractionRing C L]
variable [Algebra R L] [IsScalarTower R C L]
variable [Algebra K L] [IsScalarTower R K L]
variable [Algebra R K'] [IsScalarTower R R' K']
variable [Algebra K K'] [IsScalarTower R K K']
Lean source · statement
def completedGenericTensorChosenIdeal
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    Ideal (K' ⊗[K] L)
theorem

completedGenericTensorChosenIdeal_isMaximal

L356 ↗
EtaleFundamentalGroups.completedGenericTensorChosenIdeal_isMaximal
Source context 21 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
section GenericFibre
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
section OriginalGenericTensor
variable {K : Type uK} {L : Type uL}
variable [Field K] [Algebra R K] [IsFractionRing R K]
variable [Field L] [Algebra C L] [IsFractionRing C L]
variable [Algebra R L] [IsScalarTower R C L]
variable [Algebra K L] [IsScalarTower R K L]
variable [Algebra R K'] [IsScalarTower R R' K']
variable [Algebra K K'] [IsScalarTower R K K']
Lean source · statement
theorem completedGenericTensorChosenIdeal_isMaximal
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    (completedGenericTensorChosenIdeal
      (R := R) (R' := R') (K := K) (L := L) (K' := K')
      hmax hres Q).IsMaximal
theorem

completedGenericTensorChosenIdeal_comap

L376 ↗
EtaleFundamentalGroups.completedGenericTensorChosenIdeal_comap
Documentation

Under the canonical reassociation, the selected tensor component is exactly the generic ideal already fixed below the completed closed prime.

Source context 22 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uC uK uL uK'
variable {R : Type uR} {R' : Type uR'} {C : Type uC}
variable [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable [CommRing R'] [IsDomain R'] [IsLocalRing R'] [Algebra R R']
variable [IsLocalHom (algebraMap R R')] [Module.FaithfullyFlat R R']
variable [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
variable [FaithfulSMul R C]
section GenericFibre
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
section OriginalGenericTensor
variable {K : Type uK} {L : Type uL}
variable [Field K] [Algebra R K] [IsFractionRing R K]
variable [Field L] [Algebra C L] [IsFractionRing C L]
variable [Algebra R L] [IsScalarTower R C L]
variable [Algebra K L] [IsScalarTower R K L]
variable [Algebra R K'] [IsScalarTower R R' K']
variable [Algebra K K'] [IsScalarTower R K K']
omit [IsFractionRing R' K'] in
Lean source · full declaration
theorem completedGenericTensorChosenIdeal_comap
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R')))
    (Q : Ideal C) [Q.IsMaximal]
    [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    let e := completedGenericFiberEquiv
      (R := R) (R' := R') (C := C) (K := K) (L := L) (K' := K')
    let m := completedBaseChangeChosenGenericIdeal
      (R := R) (R' := R') (K' := K') hmax hres Q
    (completedGenericTensorChosenIdeal
        (R := R) (R' := R') (K := K) (L := L) (K' := K')
        hmax hres Q).comap e.toRingEquiv.toRingHom = m := by
  dsimp only [completedGenericTensorChosenIdeal]
  exact Ideal.comap_map_of_bijective
    (f := (completedGenericFiberEquiv
      (R := R) (R' := R') (C := C) (K := K) (L := L)
      (K' := K')).toRingEquiv.toRingHom)
    (completedGenericFiberEquiv
      (R := R) (R' := R') (C := C) (K := K) (L := L) (K' := K')).bijective

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