Module

Kernel.lean

Nyll.ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Kernel

30 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — \(\mathbb{Z}_C\) coefficients — augmentation ideal — kernel

The principal declarations in this module are:

groupAlgebraMapDomainKernelAugmentationIdeal

The ideal in \(R[A]\) generated by \([k]-1\) for \(k \in \ker f\).

groupAlgebraMapDomainTargetSection

A chosen linear section of the group-algebra map induced by a surjective group homomorphism.

groupAlgebraMapDomainKernelAugmentationGenerator_mem

A kernel augmentation generator lies in the group-algebra kernel-augmentation ideal.

groupAlgebra_mapDomainRingHom_smul

The domain group-algebra map is compatible with scalar multiplication.

Imports3

Imported by2

def

groupAlgebraMapDomainKernelAugmentationIdeal

L41 ↗

FoxDifferential.groupAlgebraMapDomainKernelAugmentationIdeal

Documentation

The ideal in \(R[A]\) generated by \([k]-1\) for \(k \in \ker f\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section GroupAlgebraMapKernel
variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]

Lean source · statement

def groupAlgebraMapDomainKernelAugmentationIdeal (f : A →* B) :
    Ideal (MonoidAlgebra R A)

theorem

groupAlgebraMapDomainKernelAugmentationGenerator_mem

L46 ↗

FoxDifferential.groupAlgebraMapDomainKernelAugmentationGenerator_mem

Documentation

A kernel augmentation generator lies in the group-algebra kernel-augmentation ideal.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section GroupAlgebraMapKernel
variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]

Lean source · statement

theorem groupAlgebraMapDomainKernelAugmentationGenerator_mem
    (f : A →* B) (k : f.ker) :
    MonoidAlgebra.of R A k.1 - 1 ∈
      groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f

theorem

groupAlgebra_mapDomainRingHom_smul

L53 ↗

FoxDifferential.groupAlgebra_mapDomainRingHom_smul

Documentation

The domain group-algebra map is compatible with scalar multiplication.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section GroupAlgebraMapKernel
variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]

Lean source · statement

theorem groupAlgebra_mapDomainRingHom_smul
    (f : A →* B) (r : R) (x : MonoidAlgebra R A) :
    MonoidAlgebra.mapDomainRingHom R f (r • x) =
      r • MonoidAlgebra.mapDomainRingHom R f x

def

groupAlgebraMapDomainTargetSection

L62 ↗

FoxDifferential.groupAlgebraMapDomainTargetSection

Documentation

A chosen linear section of the group-algebra map induced by a surjective group homomorphism.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section GroupAlgebraMapKernel
variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]

Lean source · statement

def groupAlgebraMapDomainTargetSection
    (f : A →* B) (hf : Function.Surjective f) :
    MonoidAlgebra R B →ₗ[R] MonoidAlgebra R A

theorem

groupAlgebraMapDomainTargetSection_of

L74 ↗

FoxDifferential.groupAlgebraMapDomainTargetSection_of

Documentation

The domain-target section sends a group element to the corresponding group-algebra basis element.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section GroupAlgebraMapKernel
variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]

Lean source · statement

theorem groupAlgebraMapDomainTargetSection_of
    (f : A →* B) (hf : Function.Surjective f) (b : B) :
    groupAlgebraMapDomainTargetSection (R := R) f hf
        (MonoidAlgebra.of R B b) =
      MonoidAlgebra.of R A (Function.surjInv hf b)

theorem

groupAlgebraMapDomain_targetSection

L88 ↗

FoxDifferential.groupAlgebraMapDomain_targetSection

Documentation

The chosen group-algebra section is a right inverse to the map induced by \(f\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section GroupAlgebraMapKernel
variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]

Lean source · statement

theorem groupAlgebraMapDomain_targetSection
    (f : A →* B) (hf : Function.Surjective f) (y : MonoidAlgebra R B) :
    MonoidAlgebra.mapDomainRingHom R f
        (groupAlgebraMapDomainTargetSection (R := R) f hf y) = y

theorem

groupAlgebraMapDomain_sourceBasis_sub_targetSection_mem_kernelAugmentationIdeal

L118 ↗

FoxDifferential.groupAlgebraMapDomain_sourceBasis_sub_targetSection_mem_kernelAugmentationIdeal

Documentation

A source basis element minus the chosen lift of its target image lies in the kernel augmentation ideal.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section GroupAlgebraMapKernel
variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]

Lean source · statement

theorem groupAlgebraMapDomain_sourceBasis_sub_targetSection_mem_kernelAugmentationIdeal
    (f : A →* B) (hf : Function.Surjective f) (a : A) :
    MonoidAlgebra.of R A a -
      groupAlgebraMapDomainTargetSection (R := R) f hf
        (MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R A a)) ∈
      groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f

theorem

groupAlgebraMapDomain_sub_targetSection_map_mem_kernelAugmentationIdeal

L160 ↗

FoxDifferential.groupAlgebraMapDomain_sub_targetSection_map_mem_kernelAugmentationIdeal

Documentation

Every group-algebra element differs from the chosen lift of its target image by an element of the kernel augmentation ideal.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section GroupAlgebraMapKernel
variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]

Lean source · statement

theorem groupAlgebraMapDomain_sub_targetSection_map_mem_kernelAugmentationIdeal
    (f : A →* B) (hf : Function.Surjective f) (x : MonoidAlgebra R A) :
    x - groupAlgebraMapDomainTargetSection (R := R) f hf
        (MonoidAlgebra.mapDomainRingHom R f x) ∈
      groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f

theorem

groupAlgebraMapDomainRingHom_ker_eq_kernelAugmentationIdeal_of_surjective

L203 ↗

FoxDifferential.groupAlgebraMapDomainRingHom_ker_eq_kernelAugmentationIdeal_of_surjective

Documentation

For a surjective group map, the kernel of R[A] \(\to\) R[B] is generated by the augmentation generators attached to kernel f.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section GroupAlgebraMapKernel
variable {R : Type v} {A : Type u} {B : Type w} [CommRing R] [Group A] [Group B]

Lean source · statement

theorem groupAlgebraMapDomainRingHom_ker_eq_kernelAugmentationIdeal_of_surjective
    (f : A →* B) (hf : Function.Surjective f) :
    RingHom.ker (MonoidAlgebra.mapDomainRingHom R f) =
      groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f

def

zcCompletedGroupAlgebraKernelAugmentationIdealMul

L239 ↗

FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationIdealMul

Documentation

The algebraic ideal in \(\mathbb{Z}_C\llbracket G\rrbracket\) generated by completed augmentation generators coming from the kernel of \(\psi\).

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcCompletedGroupAlgebraKernelAugmentationIdealMul
    (psi : ContinuousMonoidHom G H) :
    Ideal (ZCCompletedGroupAlgebra C G)

theorem

zcGroupLike_sub_one_mem_kernelAugmentationIdealMul

L248 ↗

FoxDifferential.zcGroupLike_sub_one_mem_kernelAugmentationIdealMul

Documentation

A kernel augmentation generator lies in the algebraic kernel-augmentation ideal.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in

Lean source · statement

theorem zcGroupLike_sub_one_mem_kernelAugmentationIdealMul
    (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi) :
    zcGroupLike C G n.1 - 1 ∈
      zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi

theorem

zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_standardAugmentationIdeal

L256 ↗

FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_standardAugmentationIdeal

Documentation

The kernel-augmentation ideal is contained in the standard source augmentation ideal.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_standardAugmentationIdeal
    (psi : ContinuousMonoidHom G H) :
    zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi ≤
      zcCompletedGroupAlgebraStandardAugmentationIdeal C G

theorem

zcGroupLike_sub_mem_kernelAugmentationIdealMul_of_map_eq

L269 ↗

FoxDifferential.zcGroupLike_sub_mem_kernelAugmentationIdealMul_of_map_eq

Documentation

Source group-like elements with the same target differ by an element of the algebraic kernel-augmentation ideal.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in

Lean source · statement

theorem zcGroupLike_sub_mem_kernelAugmentationIdealMul_of_map_eq
    (psi : ContinuousMonoidHom G H) {g₁ g₂ : G} (h : psi g₁ = psi g₂) :
    zcGroupLike C G g₁ - zcGroupLike C G g₂ ∈
      zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi

theorem

zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map

L295 ↗

FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map

Documentation

The algebraic kernel-augmentation ideal maps to zero under the completed target map.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
    (psi : ContinuousMonoidHom G H) :
    zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi ≤
      RingHom.ker (zcCompletedGroupAlgebraMap C hC psi)

theorem

isClosed_zcCompletedGroupAlgebraMap_ker

L310 ↗

FoxDifferential.isClosed_zcCompletedGroupAlgebraMap_ker

Documentation

The kernel of the completed target map is closed in the inverse-limit topology.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem isClosed_zcCompletedGroupAlgebraMap_ker
    (psi : ContinuousMonoidHom G H) :
    IsClosed
      ((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
        Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G))

theorem

closure_zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map

L321 ↗

FoxDifferential.closure_zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map

Documentation

The closure of the algebraic kernel-augmentation ideal is contained in the completed kernel.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem closure_zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
    (psi : ContinuousMonoidHom G H) :
    closure
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :
          Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) ≤
      ((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
        Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G))

theorem

zcCompletedGAMapStageRelationAugmentationGenerator_mem_proj_kernelAugmentationIdealMul

L339 ↗

FoxDifferential.zcCompletedGAMapStageRelationAugmentationGenerator_mem_proj_kernelAugmentationIdealMul

Documentation

A finite target-stage relation-augmentation generator is the projection of an algebraic kernel-augmentation generator in \(\mathbb{Z}_C\llbracket G\rrbracket\).

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGAMapStageRelationAugmentationGenerator_mem_proj_kernelAugmentationIdealMul
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (i : ZCCompletedGroupAlgebraIndex C H)
    (q :
      (completedGroupAlgebraComapQuotientMapInClass
        (G := G) (H := H) C hC psi i.2).ker) :
    ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
      zcCompletedGroupAlgebraProjection C G
          (i.1, completedGroupAlgebraComapIndexInClass
            (G := G) (H := H) C hC psi i.2) y =
        zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC psi i q

theorem

zcCompletedGAMapStageRelationAugmentationIdeal_mem_proj_kernelAugmentationIdealMul

L398 ↗

FoxDifferential.zcCompletedGAMapStageRelationAugmentationIdeal_mem_proj_kernelAugmentationIdealMul

Documentation

Every element of a finite target-stage relation-augmentation ideal is the projection of an element of the algebraic completed kernel-augmentation ideal.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGAMapStageRelationAugmentationIdeal_mem_proj_kernelAugmentationIdealMul
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (i : ZCCompletedGroupAlgebraIndex C H)
    (x : zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC psi i) :
    ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
      zcCompletedGroupAlgebraProjection C G
          (i.1, completedGroupAlgebraComapIndexInClass
            (G := G) (H := H) C hC psi i.2) y =
        (x :
          ZCCompletedGroupAlgebraStage C G
            (i.1, completedGroupAlgebraComapIndexInClass
              (G := G) (H := H) C hC psi i.2))

theorem

zcCompletedGAMapDomainKernelAugmentationIdeal_mem_proj_kernelAugmentationIdealMul

L450 ↗

FoxDifferential.zcCompletedGAMapDomainKernelAugmentationIdeal_mem_proj_kernelAugmentationIdealMul

Documentation

A finite source-stage ideal generated by kernel classes of a quotient map is the projection of the algebraic completed kernel-augmentation ideal, provided every finite kernel class has a representative in the actual kernel of \(\psi\).

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedGAMapDomainKernelAugmentationIdeal_mem_proj_kernelAugmentationIdealMul
    (psi : ContinuousMonoidHom G H)
    (i : ZCCompletedGroupAlgebraIndex C G)
    {Q : Type u} [Group Q]
    (qmap : CompletedGroupAlgebraQuotientInClass G C i.2 →* Q)
    (hkerLift :
      ∀ q : qmap.ker,
        ∃ n : ProfiniteKernelSubgroup psi,
          QuotientGroup.mk'
              ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1 =
            q.1)
    (x : ZCCompletedGroupAlgebraStage C G i)
    (hx :
      x ∈ groupAlgebraMapDomainKernelAugmentationIdeal
        (R := ModNCompletedCoeff i.1.modulus) qmap) :
    ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
      zcCompletedGroupAlgebraProjection C G i y =
        x

def

zcCompletedGroupAlgebraOpenImageIndexInClass

L514 ↗

FoxDifferential.zcCompletedGroupAlgebraOpenImageIndexInClass

Documentation

The target quotient obtained by pushing a source quotient forward along an open surjective map.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcCompletedGroupAlgebraOpenImageIndexInClass
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    CompletedGroupAlgebraIndexInClass H C

def

zcCompletedGroupAlgebraOpenImageTargetIndex

L525 ↗

FoxDifferential.zcCompletedGroupAlgebraOpenImageTargetIndex

Documentation

The two-parameter target stage whose group quotient is the open image of a source stage.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcCompletedGroupAlgebraOpenImageTargetIndex
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    ZCCompletedGroupAlgebraIndex C H

theorem

zcCompletedGroupAlgebraOpenImage_comapIndex_le

L535 ↗

FoxDifferential.zcCompletedGroupAlgebraOpenImage_comapIndex_le

Documentation

The comap of the open image quotient is coarser than the original source quotient.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedGroupAlgebraOpenImage_comapIndex_le
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
        (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i) ≤
      i.2

def

zcCompletedGroupAlgebraOpenImageQuotientMap

L555 ↗

FoxDifferential.zcCompletedGroupAlgebraOpenImageQuotientMap

Documentation

The source-stage quotient map \(G/U \to H/\psi(U)\) attached to an open surjective map.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcCompletedGroupAlgebraOpenImageQuotientMap
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    CompletedGroupAlgebraQuotientInClass G C i.2 →*
      CompletedGroupAlgebraQuotientInClass H C
        (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)

theorem

zcCompletedGroupAlgebraOpenImageQuotientMap_mk

L578 ↗

FoxDifferential.zcCompletedGroupAlgebraOpenImageQuotientMap_mk

Documentation

The open-image quotient map sends a group-like class to its corresponding finite-stage quotient representative.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGroupAlgebraOpenImageQuotientMap_mk
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) (g : G) :
    zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i
        (QuotientGroup.mk'
          ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) g) =
      QuotientGroup.mk'
        ((((OrderDual.ofDual
          (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
            OpenNormalSubgroup H) : Subgroup H)) (psi g)

theorem

zcCompletedGroupAlgebraOpenImageQuotientMap_surjective

L605 ↗

FoxDifferential.zcCompletedGroupAlgebraOpenImageQuotientMap_surjective

Documentation

The source-stage quotient map to the open image quotient is surjective.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGroupAlgebraOpenImageQuotientMap_surjective
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    Function.Surjective
      (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)

theorem

zcCompletedGroupAlgebraOpenImageQuotientMap_kernel_lift

L627 ↗

FoxDifferential.zcCompletedGroupAlgebraOpenImageQuotientMap_kernel_lift

Documentation

Kernel classes of the source-stage quotient map lift to actual elements in the kernel of \(\psi\).

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGroupAlgebraOpenImageQuotientMap_kernel_lift
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    ∀ q : (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i).ker,
      ∃ n : ProfiniteKernelSubgroup psi,
        QuotientGroup.mk'
            ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1 =
          q.1

theorem

zcCompletedGroupAlgebraOpenImageQuotientMap_stage_eq

L668 ↗

FoxDifferential.zcCompletedGroupAlgebraOpenImageQuotientMap_stage_eq

Documentation

The source-stage quotient map is the finite-stage map obtained by first transitioning to the comap of the open image and then applying the completed target-map stage.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

theorem zcCompletedGroupAlgebraOpenImageQuotientMap_stage_eq
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
        (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i) =
      (zcCompletedGroupAlgebraMapStage C hC psi
          (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i)).comp
      (zcCompletedGroupAlgebraTransition C G
          (show
            (i.1,
              completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
                (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)) ≤ i from
            ⟨le_rfl,
              zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i⟩)) := by
  erw [zcCompletedGroupAlgebraOpenImageQuotientMap]
  erw [MonoidAlgebra.mapDomainRingHom_comp]
  erw [zcCompletedGroupAlgebraMapStage]
  simp only [zcCompletedGroupAlgebraOpenImageTargetIndex]
  congr 1
  erw [zcCompletedGroupAlgebraTransition]
  erw [modNCompletedGroupAlgebraStageCoeffMapInClass_rfl]
  erw [RingHom.id_comp]
  rfl

theorem

zcCompletedGAProj_mem_openImage_kernelAugmentationIdeal_of_mem_ker

L698 ↗

FoxDifferential.zcCompletedGAProj_mem_openImage_kernelAugmentationIdeal_of_mem_ker

Documentation

A completed-kernel element projects at any source stage into the finite kernel-augmentation ideal for the source-stage quotient map to the open image.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGAProj_mem_openImage_kernelAugmentationIdeal_of_mem_ker
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (x : ZCCompletedGroupAlgebra C G)
    (hx : x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi)) :
    zcCompletedGroupAlgebraProjection C G i x ∈
      groupAlgebraMapDomainKernelAugmentationIdeal
        (R := ModNCompletedCoeff i.1.modulus)
        (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)

theorem

zcCompletedGAMap_sourceStageKernel_mem_proj_kernelAugmentationIdealMul_of_openMap_surj

L753 ↗

FoxDifferential.zcCompletedGAMap_sourceStageKernel_mem_proj_kernelAugmentationIdealMul_of_openMap_surj

Documentation

Any source-stage projection of a completed-kernel element is the projection of an element of the algebraic completed kernel-augmentation ideal.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGAMap_sourceStageKernel_mem_proj_kernelAugmentationIdealMul_of_openMap_surj
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (x : ZCCompletedGroupAlgebra C G)
    (hx : x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi)) :
    ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
      zcCompletedGroupAlgebraProjection C G i y =
        zcCompletedGroupAlgebraProjection C G i x

theorem

closure_zcCompletedGAKernelAugmentationIdealMul_eq_ker_map_of_openMap_surj

L776 ↗

FoxDifferential.closure_zcCompletedGAKernelAugmentationIdealMul_eq_ker_map_of_openMap_surj

Documentation

For an open surjective target map, the completed kernel is the closure of the algebraic kernel-augmentation ideal generated by \([n]-1\) for \(n \in \ker \psi\).

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v w
section KernelAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem closure_zcCompletedGAKernelAugmentationIdealMul_eq_ker_map_of_openMap_surj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    closure
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :
          Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) =
      ((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
        Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G))

Module documentation

Fox differential: completed — \(\mathbb{Z}_C\) coefficients — augmentation ideal — kernel

Declarations