Module

IntegralExtensionLocalFactors.lean

Nyll.EtaleFundamentalGroups.Completions.Adic.IntegralExtensionLocalFactors

5 declarations indexed from sourceView source ↗

Module documentation

Local factors of a completed integral extension

For a finite integral extension of a Dedekind domain, completion along the extension of a nonzero maximal ideal first splits over the primes above it. Power-adic cofinality removes the ramification exponent in each factor, and localization at that prime identifies the factor with the completion of the corresponding local ring.

Imports3

Imported by2

def

adicCompletionPrimePowerLocalFactorAlgEquiv

L35 ↗

EtaleFundamentalGroups.adicCompletionPrimePowerLocalFactorAlgEquiv

Documentation

The ramification-power completion at Q is canonically the completion of the local ring B_Q. Positivity of the ramification index follows from the primality of Q and finiteness of B over A.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB
variable {A : Type uA} [CommRing A] [IsDomain A]
variable {B : Type uB} [CommRing B] [IsDedekindDomain B]
variable [Algebra A B] [Algebra.IsIntegral A B]
variable [Module.IsTorsionFree A B] [Module.Finite A B]

Lean source · statement

def adicCompletionPrimePowerLocalFactorAlgEquiv
    (p : Ideal A) [p.IsMaximal] (Q : p.primesOver B) :
    AdicCompletion (Q.1 ^ Q.1.ramificationIdx A) B ≃ₐ[B]
      AdicCompletion
        (IsLocalRing.maximalIdeal (Localization.AtPrime Q.1))
        (Localization.AtPrime Q.1)

theorem

adicCompletionPrimePowerLocalFactorAlgEquiv_of

L47 ↗

EtaleFundamentalGroups.adicCompletionPrimePowerLocalFactorAlgEquiv_of

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB
variable {A : Type uA} [CommRing A] [IsDomain A]
variable {B : Type uB} [CommRing B] [IsDedekindDomain B]
variable [Algebra A B] [Algebra.IsIntegral A B]
variable [Module.IsTorsionFree A B] [Module.Finite A B]
omit [IsDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] in

Lean source · statement

theorem adicCompletionPrimePowerLocalFactorAlgEquiv_of
    (p : Ideal A) [p.IsMaximal] (Q : p.primesOver B) (x : B) :
    adicCompletionPrimePowerLocalFactorAlgEquiv p Q
        (AdicCompletion.of (Q.1 ^ Q.1.ramificationIdx A) B x) =
      algebraMap B
        (AdicCompletion
          (IsLocalRing.maximalIdeal (Localization.AtPrime Q.1))
          (Localization.AtPrime Q.1)) x

def

adicCompletionIntegralExtensionLocalFactorsRingEquiv

L59 ↗

EtaleFundamentalGroups.adicCompletionIntegralExtensionLocalFactorsRingEquiv

Documentation

Completion along the extended ideal is the product of the completed local rings at all primes above p.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB
variable {A : Type uA} [CommRing A] [IsDomain A]
variable {B : Type uB} [CommRing B] [IsDedekindDomain B]
variable [Algebra A B] [Algebra.IsIntegral A B]
variable [Module.IsTorsionFree A B] [Module.Finite A B]

Lean source · statement

def adicCompletionIntegralExtensionLocalFactorsRingEquiv
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥) :
    AdicCompletion (p.map (algebraMap A B)) B ≃+*
      ∀ Q : p.primesOver B,
        AdicCompletion
          (IsLocalRing.maximalIdeal (Localization.AtPrime Q.1))
          (Localization.AtPrime Q.1)

theorem

adicCompletionIntegralExtensionLocalFactorsRingEquiv_apply

L71 ↗

EtaleFundamentalGroups.adicCompletionIntegralExtensionLocalFactorsRingEquiv_apply

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB
variable {A : Type uA} [CommRing A] [IsDomain A]
variable {B : Type uB} [CommRing B] [IsDedekindDomain B]
variable [Algebra A B] [Algebra.IsIntegral A B]
variable [Module.IsTorsionFree A B] [Module.Finite A B]

Lean source · statement

theorem adicCompletionIntegralExtensionLocalFactorsRingEquiv_apply
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (x : AdicCompletion (p.map (algebraMap A B)) B)
    (Q : p.primesOver B) :
    adicCompletionIntegralExtensionLocalFactorsRingEquiv p hp x Q =
      adicCompletionPrimePowerLocalFactorAlgEquiv p Q
        (adicCompletionIntegralExtensionEquivPi p hp x Q)

theorem

adicCompletionIntegralExtensionLocalFactorsRingEquiv_of_apply

L83 ↗

EtaleFundamentalGroups.adicCompletionIntegralExtensionLocalFactorsRingEquiv_of_apply

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB
variable {A : Type uA} [CommRing A] [IsDomain A]
variable {B : Type uB} [CommRing B] [IsDedekindDomain B]
variable [Algebra A B] [Algebra.IsIntegral A B]
variable [Module.IsTorsionFree A B] [Module.Finite A B]

Lean source · statement

theorem adicCompletionIntegralExtensionLocalFactorsRingEquiv_of_apply
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥) (x : B)
    (Q : p.primesOver B) :
    adicCompletionIntegralExtensionLocalFactorsRingEquiv p hp
        (AdicCompletion.of (p.map (algebraMap A B)) B x) Q =
      algebraMap B
        (AdicCompletion
          (IsLocalRing.maximalIdeal (Localization.AtPrime Q.1))
          (Localization.AtPrime Q.1)) x

Module documentation

Local factors of a completed integral extension

Declarations

adicCompletionPrimePowerLocalFactorAlgEquiv

adicCompletionPrimePowerLocalFactorAlgEquiv_of

adicCompletionIntegralExtensionLocalFactorsRingEquiv

adicCompletionIntegralExtensionLocalFactorsRingEquiv_apply

adicCompletionIntegralExtensionLocalFactorsRingEquiv_of_apply