Module

FiltrationDrop.lean

Nyll.ProCGroups.ProP.Fox.FiltrationDrop

3 declarations indexed from sourceView source ↗

Module documentation

Filtration drop for continuous Fox operators

An additive Fox operator satisfying the right-Fox Leibniz rule lowers powers of the augmentation ideal. Continuity extends this algebraic result to closed powers, and hence makes the drop independent of representatives modulo the next source layer.

Imports1

Nyll.ProCGroups.ProP.Zassenhaus.AugmentationFiltration

Imported by2

theorem

mem_ideal_pow_of_foxOperator

L33 ↗

ClassFieldTower.ProP.mem_ideal_pow_of_foxOperator

Documentation

An additive Fox operator lowers ordinary powers of the augmentation ideal.

The product rule is written in the right-Fox convention used by the existing finite-stage PCG derivative. The proof has no topological hypotheses.

Source context 6 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
noncomputable section
universe u v w
variable {A : Type u} {B : Type v} {R : Type w}
variable [Ring A] [Ring B] [Ring R]

Lean source · statement

theorem mem_ideal_pow_of_foxOperator
    (epsilon : A →+* R) (phi : A →+* B) (coeff : R →+* B)
    (D : A →+ B) (J : Ideal B) [J.IsTwoSided]
    (hphi : ∀ x ∈ RingHom.ker epsilon, phi x ∈ J)
    (hleibniz : ∀ x y,
      D (x * y) = coeff (epsilon y) * D x + phi x * D y)
    (n : ℕ) {x : A} (hx : x ∈ RingHom.ker epsilon ^ (n + 1)) :
    D x ∈ J ^ n

theorem

mem_ideal_pow_closure_of_continuous_foxOperator

L60 ↗

ClassFieldTower.ProP.mem_ideal_pow_closure_of_continuous_foxOperator

Documentation

A continuous additive Fox operator lowers closed augmentation powers.

Source context 6 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
noncomputable section
universe u v w
variable {A : Type u} {B : Type v} {R : Type w}
variable [Ring A] [Ring B] [Ring R]

Lean source · statement

theorem mem_ideal_pow_closure_of_continuous_foxOperator
    [TopologicalSpace A] [IsTopologicalRing A]
    [TopologicalSpace B] [IsTopologicalRing B]
    (epsilon : A →+* R) (phi : A →+* B) (coeff : R →+* B)
    (D : A →+ B) (J : Ideal B) [J.IsTwoSided]
    (hphi : ∀ x ∈ RingHom.ker epsilon, phi x ∈ J)
    (hleibniz : ∀ x y,
      D (x * y) = coeff (epsilon y) * D x + phi x * D y)
    (hD : Continuous D) (n : ℕ) {x : A}
    (hx : x ∈ (RingHom.ker epsilon ^ (n + 1)).closure) :
    D x ∈ (J ^ n).closure

theorem

foxOperator_initialForm_congr

L86 ↗

ClassFieldTower.ProP.foxOperator_initialForm_congr

Documentation

The closed filtration drop is compatible with changing a representative by one deeper source layer. This is the exact congruence needed for the induced graded Fox/Jacobian map.

Source context 6 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
noncomputable section
universe u v w
variable {A : Type u} {B : Type v} {R : Type w}
variable [Ring A] [Ring B] [Ring R]

Lean source · statement

theorem foxOperator_initialForm_congr
    [TopologicalSpace A] [IsTopologicalRing A]
    [TopologicalSpace B] [IsTopologicalRing B]
    (epsilon : A →+* R) (phi : A →+* B) (coeff : R →+* B)
    (D : A →+ B) (J : Ideal B) [J.IsTwoSided]
    (hphi : ∀ x ∈ RingHom.ker epsilon, phi x ∈ J)
    (hleibniz : ∀ x y,
      D (x * y) = coeff (epsilon y) * D x + phi x * D y)
    (hD : Continuous D) (n : ℕ) {x y : A}
    (hxy : x - y ∈ (RingHom.ker epsilon ^ (n + 2)).closure) :
    D x - D y ∈ (J ^ (n + 1)).closure

Module documentation

Filtration drop for continuous Fox operators

Declarations

mem_ideal_pow_of_foxOperator

mem_ideal_pow_closure_of_continuous_foxOperator

foxOperator_initialForm_congr