ModuleIdealLocalizationValuationEquiv.lean
Nyll.SchemeTheory.RingTheory.Ramification.IdealLocalizationValuationEquiv
5 declarations indexed from sourceView source ↗ Module documentation
Prime localization and its valuation-ring model
Constructs the canonical ring equivalence between a Dedekind prime localization and its valuation-ring model in the fraction field. Computation lemmas identify its values on the original coefficients.
Declarations
TameAbhyankar.SGA1.idealLocalizationValuationAlgebra
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace TameAbhyankar.SGA1
universe u v
variable (B : Type u) (L : Type v) [CommRing B] [IsDedekindDomain B]
[Field L] [Algebra B L] [IsFractionRing B L]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
TameAbhyankar.SGA1.idealLocalizationValuation_isLocalization
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace TameAbhyankar.SGA1
universe u v
variable (B : Type u) (L : Type v) [CommRing B] [IsDedekindDomain B]
[Field L] [Algebra B L] [IsFractionRing B L]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
local instance idealLocalizationValuationAlgebra :
Algebra B (idealLocalizationValuationSubring B L Q hQ) := by
change Algebra B (idealLocalizationSubalgebra B L Q)
infer_instance
TameAbhyankar.SGA1.primeLocalizationEquivValuation
DocumentationThe canonical identity-on-coefficients equivalence from the literal prime localization to the already constructed native local valuation ring.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace TameAbhyankar.SGA1
universe u v
variable (B : Type u) (L : Type v) [CommRing B] [IsDedekindDomain B]
[Field L] [Algebra B L] [IsFractionRing B L]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
local instance idealLocalizationValuationAlgebra :
Algebra B (idealLocalizationValuationSubring B L Q hQ) := by
change Algebra B (idealLocalizationSubalgebra B L Q)
infer_instance
TameAbhyankar.SGA1.primeLocalizationEquivValuation_algebraMap
DocumentationThe constructed equivalence uses the actual original normalization coefficient map.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace TameAbhyankar.SGA1
universe u v
variable (B : Type u) (L : Type v) [CommRing B] [IsDedekindDomain B]
[Field L] [Algebra B L] [IsFractionRing B L]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
local instance idealLocalizationValuationAlgebra :
Algebra B (idealLocalizationValuationSubring B L Q hQ) := by
change Algebra B (idealLocalizationSubalgebra B L Q)
infer_instance
TameAbhyankar.SGA1.primeLocalizationEquivValuation_algebraMap_coe
DocumentationThe canonical equivalence followed by the actual field inclusion is the original B-coefficient map. Its interface opens no B-action on the target V.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace TameAbhyankar.SGA1
universe u v
variable (B : Type u) (L : Type v) [CommRing B] [IsDedekindDomain B]
[Field L] [Algebra B L] [IsFractionRing B L]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
local instance idealLocalizationValuationAlgebra :
Algebra B (idealLocalizationValuationSubring B L Q hQ) := by
change Algebra B (idealLocalizationSubalgebra B L Q)
infer_instance