ModuleLocalFactor.lean
Nyll.EtaleFundamentalGroups.FiniteEtale.ChosenPrime.LocalFactor
21 declarations indexed from sourceView source ↗ Module documentation
The non-Henselian local factor selected by Tag 00UJ
The idempotent furnished by Tag 00UJ cuts out a finite factor after an etale change of the base. Its chosen prime remains the unique prime over the pointed prime after inverting the idempotent. Consequently the prime localization of that factor is finite over the pointed base localization.
No Henselian hypothesis is used here. This is the part of the chosen-factor construction which precedes any root-cover or purity argument.
Declarations
EtaleFundamentalGroups.exists_localizationAtPrime_pi_factor_ringEquiv
DocumentationEvery prime-local ring of a finite product is canonically the prime-local ring of one actual coordinate. The coordinate and its prime are extracted from the given prime; neither is supplied as auxiliary data.
The computation on algebra maps records that this is the literal evaluation map. It is the local form of PrimeSpectrum.exists_comap_evalRingHom_eq needed when a generic tensor product is decomposed into its field components.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
section FiniteProductPrimeCoordinate
universe uI uA uBase
EtaleFundamentalGroups.exists_localizationAtPrime_pi_factor_algEquiv
DocumentationAlgebra-linear form of exists_localizationAtPrime_pi_factor_ringEquiv. The algebra structures on the product and the selected factor are the canonical coordinatewise ones.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
section FiniteProductPrimeCoordinate
universe uI uA uBase
EtaleFundamentalGroups.exists_integralClosure_artinianComponent_localizationAtPrime_algEquiv
DocumentationA prime-local factor of the normalization in a reduced Artinian algebra comes from one actual residue-field component of that algebra.
Both the component and the prime in its normalization are extracted from the given prime. This is the normalization-level coordinate producer used after smooth base change of the Tag 00UJ tensor product.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
section ArtinianNormalizationPrimeCoordinate
universe uB uG
EtaleFundamentalGroups.etaleChosenAwayPrime
DocumentationThe prime in the idempotent Away factor induced by the Tag 00UJ prime.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenAwayPrime_isPrime
DocumentationA Tag prime avoiding the chosen idempotent remains prime in the Away factor.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenAwayPrime_liesOver
DocumentationThe prime in the Away factor contracts to the original Tag prime.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenAway_primesOver_eq_singleton
DocumentationTag uniqueness before localization is exactly uniqueness of the prime over the pointed base prime in the idempotent Away factor.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.moduleFinite_etaleChosenAway_localizationAtPrime
DocumentationThe chosen prime-local factor is finite over the pointed localization. This is the non-Henselian finiteness step: the singleton fibre, rather than Hensel's lemma, is what makes localization preserve module finiteness.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenLocalFactorToIntegralClosureAlgHom
DocumentationThe canonical inclusion of the literal local factor into the integral closure of the pointed base in its total fraction ring. No domain claim is made here: identifying the total fraction ring with the actual selected field component is precisely the later generic-component comparison. The map itself and its integrality require only the Tag singleton fibre.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenLocalFactorToIntegralClosureAlgHom_injective
DocumentationThe canonical local-factor map to the normalization in its total fraction ring is injective.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenAwayLocalizationAtPrimeAlgEquiv
DocumentationLocalizing the idempotent factor at its chosen prime is canonically the same as localizing the original tensor product at the Tag prime.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenPointedTensorBaseChangeAlgHom
DocumentationBase change the Tag tensor product from the pointed etale neighborhood to the local ring at its chosen point.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenPointedTensorPrime
DocumentationThe actual Tag prime after base change to the pointed local base.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenPointedTensorPrime_isPrime
DocumentationThe actual Tag prime remains prime after pointed-base localization.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenPointedTensorPrime_comap
DocumentationThe pointed-base Tag prime contracts to the original Tag prime.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenAwayPointedBaseChangeLocalizationAlgEquiv
DocumentationThe Tag local factor is unchanged when the pointed etale neighborhood is localized at its chosen point. More precisely, both displayed local rings are the localization of the original tensor product at the complement of the same literal Tag prime.
This is the non-Henselian comparison: no cancellation of the pointed etale neighborhood with the original local base is used.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.etaleChosenAwayPointedBaseChangeLocalizationAtPrimeAlgEquiv
DocumentationThe pointed-base comparison is linear over the pointed local ring itself. The source algebra is the canonical one induced by the chain of lies-over primes.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
EtaleFundamentalGroups.smoothNormalizationBaseChangeAlgEquiv
DocumentationSmooth base change identifies the literal tensor product of a normalization with the relative integral closure in the base-changed ambient algebra. This is the production smooth comparison, retained as an equivalence so that the actual Tag prime can be localized without choosing a new component.
Source context 14 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
section SmoothNormalizationComparison
universe uK uL
variable {K : Type uK} {L : Type uL}
variable [Field K] [Field L]
variable [Algebra R K] [IsFractionRing R K]
variable [Algebra K L] [Algebra R L] [IsScalarTower R K L]
variable [Algebra.Smooth R C]
EtaleFundamentalGroups.pointedSmoothNormalizationBaseChangeAlgEquiv
DocumentationSmooth base change followed by localization at the pointed prime still preserves integral closure. The proof composes the production smooth comparison with the production localization comparison; it does not assume a new comparison equivalence.
Source context 14 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
section SmoothNormalizationComparison
universe uK uL
variable {K : Type uK} {L : Type uL}
variable [Field K] [Field L]
variable [Algebra R K] [IsFractionRing R K]
variable [Algebra K L] [Algebra R L] [IsScalarTower R K L]
variable [Algebra.Smooth R C]
EtaleFundamentalGroups.etaleChosenLocalFactorSmoothIntegralClosureAlgEquiv
DocumentationThe non-Henselian Tag local factor is the local ring at the transported prime of the smooth base-changed integral closure. In particular this comparison preserves the chosen prime; it does not reselect an abstract generic component.
Source context 14 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
section SmoothNormalizationComparison
universe uK uL
variable {K : Type uK} {L : Type uL}
variable [Field K] [Field L]
variable [Algebra R K] [IsFractionRing R K]
variable [Algebra K L] [Algebra R L] [IsScalarTower R K L]
variable [Algebra.Smooth R C]
EtaleFundamentalGroups.exists_etaleChosenLocalFactor_finiteGenericFiberComponent_algEquiv
DocumentationThe actual generic field component selected by the non-Henselian Tag local factor.
After localizing the pointed etale base at P, smooth base change identifies the Tag tensor product with the normalization in its generic algebra. That generic algebra is a reduced Artinian algebra over L; hence the transported Tag prime canonically selects one literal maximal-ideal quotient field and a prime in its normalization. The resulting local ring is the original Tag local factor, as an algebra over the pointed local base.
Source context 14 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uS
variable {R : Type uR} {C : Type uC} {S : Type uS}
variable [CommRing R] [CommRing C] [CommRing S]
variable [Algebra R C] [Algebra R S]
section SmoothNormalizationComparison
universe uK uL
variable {K : Type uK} {L : Type uL}
variable [Field K] [Field L]
variable [Algebra R K] [IsFractionRing R K]
variable [Algebra K L] [Algebra R L] [IsScalarTower R K L]
variable [Algebra.Smooth R C]