Yamaguchi Lean 4 Library
FoxDifferential.Completed.DifferentialModule.Map.Limit
FoxDifferential/Completed/DifferentialModule/Map/Limit

FoxDifferential.Completed.DifferentialModule.Map.Limit

2 Theorem | 1 Definition

This module proves the separation lemmas used to read finite-support elements through suitable finite quotients. It chooses quotients that isolate a selected support point and then shows that the corresponding finite-stage coefficient is preserved.

Open this file on GitHub
import
Imported by

Declarations

Definition FoxDifferential.primePowerCompletedGroupAlgebraMap GitHub 
def primePowerCompletedGroupAlgebraMap
    (ψ : ContinuousMonoidHom G H) :
    PrimePowerCompletedGroupAlgebra ℓ G →+* PrimePowerCompletedGroupAlgebra ℓ H where
  toFun x := ⟨fun i =>
      primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
          (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x), by
    intro i j hij
    let hsource :
        (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) ≤
          (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) :=
      ⟨hij.1, completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hij.2⟩
    have hx := x.2
      (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
      (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2)
      hsource
    change
      primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hsource
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
            (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) x) =
        primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
          (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x at hx
    have hcompat := congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraMapStage_compatible
          (ℓ := ℓ) (G := G) (H := H) ψ hij))
      (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
        (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) x)
    rw [RingHom.comp_apply, RingHom.comp_apply] at hcompat
    rw [hx] at hcompat
    simpa [primePowerCompletedGroupAlgebraSystem] using hcompat⟩
  map_one' := by
    apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
    intro i
    simp only [primePowerCompletedGroupAlgebraMapStage, InverseSystems.InverseSystem.projection_apply,
  coe_one_primePowerCompletedGroupAlgebra, Pi.one_apply, MonoidAlgebra.mapDomainRingHom_apply,
  MonoidAlgebra.mapDomain_one]
  map_mul' := by
    intro x y
    apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
    intro i
    simp only [InverseSystems.InverseSystem.projection_apply, coe_mul_primePowerCompletedGroupAlgebra,
  Pi.mul_apply, map_mul]
  map_zero' := by
    apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
    intro i
    simp only [primePowerCompletedGroupAlgebraMapStage, InverseSystems.InverseSystem.projection_apply,
  coe_zero_primePowerCompletedGroupAlgebra, Pi.zero_apply, MonoidAlgebra.mapDomainRingHom_apply,
  Finsupp.mapDomain_zero]
  map_add' := by
    intro x y
    apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
    intro i
    simp only [InverseSystems.InverseSystem.projection_apply, coe_add_primePowerCompletedGroupAlgebra,
  Pi.add_apply, map_add]

Coefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjection_map GitHub 
theorem primePowerCompletedGroupAlgebraProjection_map
    (ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H)
    (x : PrimePowerCompletedGroupAlgebra ℓ G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
        (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ x) =
      primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
          (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x)

The finite-stage Fox-differential projection is computed by the prime-power completed group-algebra projection formula.

Show proof
Theorem FoxDifferential.continuous_primePowerCompletedGroupAlgebraMap GitHub 
theorem continuous_primePowerCompletedGroupAlgebraMap
    (ψ : ContinuousMonoidHom G H) :
    Continuous (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ)

The completed group-algebra map induced by a continuous homomorphism is continuous for the inverse-limit topologies.

Show proof