ModuleNormalizationPrimeStalkFieldTower.lean
Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeStalkFieldTower
7 declarations indexed from sourceView source ↗ Module documentation
The actual original-field, stalk-fraction and ambient-field tower
The injective original stalk structure map induces its fraction-field map from the displayed original K. The computed extension equation proves that the actual ambient embedding composes to the original K-to-L map. Thus the canonical algebras attached to these two constructed maps form a genuine scalar tower. Fraction-field uniqueness also compares this map with the existing canonical FractionRing A map used by the normal-local pi1 sequence.
Declarations
EtaleFundamentalGroups.StrictHenselian.normalizationResiduePoint_isLocalHom
DocumentationThe actual normalization residue point is local over a local base, using contraction of the original maximal normalization prime.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
EtaleFundamentalGroups.StrictHenselian.normalizationStalkFractionBaseMap
DocumentationThe actual field map from the displayed original fraction field to the fraction field of the constructed geometric stalk.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
variable (A : Type u) (K : Type v) (L : Type u)
[CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
(Q : Ideal (integralClosure A L)) [Q.IsMaximal]
EtaleFundamentalGroups.StrictHenselian.normalizationStalkFractionBaseMap_algebraMap
DocumentationThe displayed fraction-field map extends the actual original stalk structure map on each coefficient of A.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
variable (A : Type u) (K : Type v) (L : Type u)
[CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
(Q : Ideal (integralClosure A L)) [Q.IsMaximal]
EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionToNormalizationField_comp_baseField
DocumentationThe two actual field maps compose to the original K-to-L coefficient map. This is proved on A and extended by fraction-field uniqueness.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
variable (A : Type u) (K : Type v) (L : Type u)
[CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
(Q : Ideal (integralClosure A L)) [Q.IsMaximal]
EtaleFundamentalGroups.StrictHenselian.normalizationStalkFractionField_isScalarTower
DocumentationThe algebras of the two actual maps form a scalar tower with the original K-action on L. No compatibility premise is introduced.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
variable (A : Type u) (K : Type v) (L : Type u)
[CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
(Q : Ideal (integralClosure A L)) [Q.IsMaximal]
EtaleFundamentalGroups.StrictHenselian.normalizationStalkFractionField_isSepClosure
DocumentationThe original separably closed Galois field is a separable closure of the actual stalk fraction field for its constructed ambient action.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
variable (A : Type u) (K : Type v) (L : Type u)
[CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
(Q : Ideal (integralClosure A L)) [Q.IsMaximal]
EtaleFundamentalGroups.StrictHenselian.normalizationStalkFractionBaseMap_eq_canonical
DocumentationThe displayed-field map is the existing canonical fraction-field map precomposed with the proved original fraction-field equivalence. This keeps an independent-universe K while allowing the canonical same-universe pi1 API.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
variable (A : Type u) (K : Type v) (L : Type u)
[CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
(Q : Ideal (integralClosure A L)) [Q.IsMaximal]