ModuleLiesOverFractionRingExtension.lean
Nyll.SchemeTheory.RingTheory.GenericFiber.LiesOverFractionRingExtension
9 declarations indexed from sourceView source ↗ Module documentation
Fraction fields along a finite local extension
Let D / S be a finite extension of domains, and let q lie over p. This file fixes all canonical algebra structures between the two prime localizations and the fraction field of D. It also transports finite dimensionality to the literal fraction field of Sₚ.
Declarations
EtaleFundamentalGroups.finiteLiesOverLocalizationAlgebra
DocumentationThe canonical algebra from Sₚ to D_q when q lies over p.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uS uD
variable {S : Type uS} {D : Type uD}
variable [CommRing S] [IsDomain S]
variable [CommRing D] [IsDomain D]
variable [Algebra S D] [FaithfulSMul S D] [Module.Finite S D]
EtaleFundamentalGroups.finiteLiesOverLocalizationToFractionRingAlgebra
DocumentationThe canonical embedding of D_q into the literal fraction field of D.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uS uD
variable {S : Type uS} {D : Type uD}
variable [CommRing S] [IsDomain S]
variable [CommRing D] [IsDomain D]
variable [Algebra S D] [FaithfulSMul S D] [Module.Finite S D]
EtaleFundamentalGroups.finiteExtensionFractionRingAlgebra
DocumentationThe standard extension of fraction fields induced by S → D.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uS uD
variable {S : Type uS} {D : Type uD}
variable [CommRing S] [IsDomain S]
variable [CommRing D] [IsDomain D]
variable [Algebra S D] [FaithfulSMul S D] [Module.Finite S D]
EtaleFundamentalGroups.finiteExtensionAtPrimeToFractionRingAlgebra
DocumentationThe map Sₚ → Frac(D) factored through Frac(S).
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uS uD
variable {S : Type uS} {D : Type uD}
variable [CommRing S] [IsDomain S]
variable [CommRing D] [IsDomain D]
variable [Algebra S D] [FaithfulSMul S D] [Module.Finite S D]
EtaleFundamentalGroups.finiteExtensionAtPrimeFractionRingAlgebra
DocumentationThe literal fraction field of Sₚ acts on Frac(D) through the canonical identification Frac(Sₚ) ≃ Frac(S).
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uS uD
variable {S : Type uS} {D : Type uD}
variable [CommRing S] [IsDomain S]
variable [CommRing D] [IsDomain D]
variable [Algebra S D] [FaithfulSMul S D] [Module.Finite S D]
EtaleFundamentalGroups.finiteExtensionAtPrime_fractionRingTower
DocumentationThe maps Sₚ → Frac(S) → Frac(D) form the defining scalar tower.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uS uD
variable {S : Type uS} {D : Type uD}
variable [CommRing S] [IsDomain S]
variable [CommRing D] [IsDomain D]
variable [Algebra S D] [FaithfulSMul S D] [Module.Finite S D]
omit [Module.Finite S D] in
EtaleFundamentalGroups.finiteExtensionAtPrime_literalFractionRingTower
DocumentationThe direct map from Sₚ to Frac(D) extends through the literal fraction field of Sₚ.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uS uD
variable {S : Type uS} {D : Type uD}
variable [CommRing S] [IsDomain S]
variable [CommRing D] [IsDomain D]
variable [Algebra S D] [FaithfulSMul S D] [Module.Finite S D]
omit [Module.Finite S D] in
EtaleFundamentalGroups.finiteExtensionAtPrime_fractionRing_finiteDimensional
DocumentationFrac(D) is finite over the literal fraction field of Sₚ.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uS uD
variable {S : Type uS} {D : Type uD}
variable [CommRing S] [IsDomain S]
variable [CommRing D] [IsDomain D]
variable [Algebra S D] [FaithfulSMul S D] [Module.Finite S D]
EtaleFundamentalGroups.finiteLiesOverLocalization_fractionRingTower
DocumentationThe two canonical routes Sₚ → D_q → Frac(D) and Sₚ → Frac(S) → Frac(D) agree.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uS uD
variable {S : Type uS} {D : Type uD}
variable [CommRing S] [IsDomain S]
variable [CommRing D] [IsDomain D]
variable [Algebra S D] [FaithfulSMul S D] [Module.Finite S D]
omit [Module.Finite S D] in