NYLL
Module

IntegralExtensionAlgebra.lean

Nyll.SchemeTheory.RingTheory.AdicCompletion.IntegralExtensionAlgebra
3 declarations indexed from sourceView source ↗

Module documentation

Algebra compatibility of the integral-extension completion decomposition

The Chinese-remainder decomposition of a completed finite integral extension is compatible with the canonical maps from the extension ring.

Imports1
Imported by1

Declarations

def

adicCompletionIntegralExtensionAlgEquivPi

L29 ↗
EtaleFundamentalGroups.adicCompletionIntegralExtensionAlgEquivPi
Documentation

The decomposition of the completion of a finite integral extension as a product of prime-power completions, as an equivalence of B-algebras.

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 · full declaration
def adicCompletionIntegralExtensionAlgEquivPi
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥) :
    AdicCompletion (p.map (algebraMap A B)) B ≃ₐ[B]
      ∀ Q : p.primesOver B,
        AdicCompletion (Q.1 ^ Q.1.ramificationIdx A) B where
  toRingEquiv := adicCompletionIntegralExtensionEquivPi p hp
  commutes' x := by
    apply funext
    intro Q
    simp only [Pi.algebraMap_apply, AdicCompletion.algebraMap_apply,
      Algebra.algebraMap_self, RingHom.id_apply]
    change adicCompletionIntegralExtensionEquivPi p hp
        (AdicCompletion.of (p.map (algebraMap A B)) B x) Q =
      AdicCompletion.of (Q.1 ^ Q.1.ramificationIdx A) B x
    exact adicCompletionIntegralExtensionEquivPi_of p hp x Q
theorem

adicCompletionIntegralExtensionAlgEquivPi_of_apply

L48 ↗
EtaleFundamentalGroups.adicCompletionIntegralExtensionAlgEquivPi_of_apply
Documentation

Primewise computation of the algebra equivalence on the canonical image of an element of B.

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 adicCompletionIntegralExtensionAlgEquivPi_of_apply
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥) (x : B)
    (Q : p.primesOver B) :
    adicCompletionIntegralExtensionAlgEquivPi p hp
        (AdicCompletion.of (p.map (algebraMap A B)) B x) Q =
      AdicCompletion.of (Q.1 ^ Q.1.ramificationIdx A) B x
theorem

adicCompletionIntegralExtensionAlgEquivPi_algebraMap_apply

L58 ↗
EtaleFundamentalGroups.adicCompletionIntegralExtensionAlgEquivPi_algebraMap_apply
Documentation

Bundled algebra-map form of the primewise compatibility calculation.

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 adicCompletionIntegralExtensionAlgEquivPi_algebraMap_apply
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥) (x : B)
    (Q : p.primesOver B) :
    adicCompletionIntegralExtensionAlgEquivPi p hp
        (algebraMap B (AdicCompletion (p.map (algebraMap A B)) B) x) Q =
      algebraMap B (AdicCompletion (Q.1 ^ Q.1.ramificationIdx A) B) x

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.