Module

SubtypeLinear.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.SubtypeLinear

13 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — coefficient rings — prime-power augmentation ideal — subtype linear

The principal declarations in this module are:

primePowerCompletedGroupAlgebraAugmentationIdealAddEquivAddSubgroup

The inverse-limit augmentation ideal is additively equivalent to the additive kernel of the canonical prime-power augmentation.

primePowerCompletedGroupAlgebraAugmentationIdealLinearEquivAddSubgroup

The inverse-limit augmentation ideal is linearly equivalent to the additive kernel of the canonical prime-power augmentation.

primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_apply

The integral-linear inclusion of the prime-power augmentation ideal returns the underlying completed group-algebra element.

primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear_apply

The coefficient-linear inclusion of the prime-power augmentation ideal returns the underlying completed group-algebra element.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Augmentation

Imported by2

def

primePowerCompletedGroupAlgebraAugmentationIdealAddEquivAddSubgroup

L44 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealAddEquivAddSubgroup

Documentation

The inverse-limit augmentation ideal is additively equivalent to the additive kernel of the canonical prime-power augmentation.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

def primePowerCompletedGroupAlgebraAugmentationIdealAddEquivAddSubgroup :
    PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G ≃+
      primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G) where
  toFun x := by
    refine ⟨(ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
      (ℓ := ℓ) (G := G) x).1, ?_⟩
    exact (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
      (ℓ := ℓ) (G := G) x).2
  invFun x :=
    toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) <|
      ⟨x.1, by
        exact x.2⟩
  left_inv := by
    intro x
    exact toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of
      (ℓ := ℓ) (G := G) x
  right_inv := by
    intro x
    apply Subtype.ext
    let y : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) :=
      ⟨x.1, by
        exact x.2⟩
    exact congrArg Subtype.val
      (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to
        (ℓ := ℓ) (G := G) y)
  map_add' x y := by
    apply Subtype.ext
    apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
    intro i
    rfl

def

primePowerCompletedGroupAlgebraAugmentationIdealLinearEquivAddSubgroup

L79 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealLinearEquivAddSubgroup

Documentation

The inverse-limit augmentation ideal is linearly equivalent to the additive kernel of the canonical prime-power augmentation.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def primePowerCompletedGroupAlgebraAugmentationIdealLinearEquivAddSubgroup :
    PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G ≃ₗ[ℤ]
      primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)

def

primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear

L89 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear

Documentation

The canonical inclusion of the inverse-limit augmentation ideal into the prime-power completed group algebra.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear :
    PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G →ₗ[ℤ]
      PrimePowerCompletedGroupAlgebra ℓ G

theorem

primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_apply

L103 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_apply

Documentation

The integral-linear inclusion of the prime-power augmentation ideal returns the underlying completed group-algebra element.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_apply
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
        (ℓ := ℓ) (G := G) x =
      (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
        (ℓ := ℓ) (G := G) x).1

def

primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear

L115 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear

Documentation

The canonical inclusion of the inverse-limit augmentation ideal into the prime-power completed group algebra, viewed over the completed coefficient ring.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

def primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear :
    PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G →ₗ[PrimePowerCompletedCoeff ℓ G]
      PrimePowerCompletedGroupAlgebra ℓ G where
  toFun := fun x =>
    (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x).1
  map_add' := by
    intro x y
    apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
    intro i
    change (((primePowerCompletedGroupAlgebraAugmentationIdealProjection
        (ℓ := ℓ) (G := G) i x +
          primePowerCompletedGroupAlgebraAugmentationIdealProjection
            (ℓ := ℓ) (G := G) i y :
          primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) :
            PrimePowerCompletedGroupAlgebraStage ℓ G i)) =
      primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
        ((ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
          (ℓ := ℓ) (G := G) x).1 +
          (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
            (ℓ := ℓ) (G := G) y).1)
    rw [primePowerCompletedGroupAlgebraProjection_add,
      primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal,
      primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal]
    rfl
  map_smul' := by
    intro a x
    apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
    intro i
    change (((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        primePowerCompletedGroupAlgebraAugmentationIdealProjection
          (ℓ := ℓ) (G := G) i x :
          primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) :
            PrimePowerCompletedGroupAlgebraStage ℓ G i) =
      primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
        (a • (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
          (ℓ := ℓ) (G := G) x).1)
    rw [primePowerCompletedGroupAlgebraProjection_smul,
      primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal]
    rfl

theorem

primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear_apply

L161 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear_apply

Documentation

The coefficient-linear inclusion of the prime-power augmentation ideal returns the underlying completed group-algebra element.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear_apply
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
        (ℓ := ℓ) (G := G) x =
      (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
        (ℓ := ℓ) (G := G) x).1

theorem

primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_injective

L170 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_injective

Documentation

The canonical linear inclusion of the completed augmentation ideal is injective.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_injective :
    Function.Injective
      (primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
        (ℓ := ℓ) (G := G))

theorem

exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear

L186 ↗

FoxDifferential.exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear

Documentation

The linear inclusion of the prime-power completed augmentation ideal has image equal to the kernel of the prime-power augmentation.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear :
    Function.Exact
      (primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
        (ℓ := ℓ) (G := G))
      (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G))

theorem

primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_shortExact

L218 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_shortExact

Documentation

The canonical augmentation sequence with augmentation ideal as kernel is short exact: the inclusion is injective, its image is the kernel of augmentation, and the augmentation is surjective.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_shortExact :
    Function.Injective
        (primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
          (ℓ := ℓ) (G := G)) ∧
      Function.Exact
        (primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
          (ℓ := ℓ) (G := G))
        (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) ∧
      Function.Surjective
        (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G))

theorem

primePowerCompletedGroupAlgebraAugmentationCoeffLinear_surjective

L237 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationCoeffLinear_surjective

Documentation

The coefficient-linear form of the prime-power completed augmentation is surjective.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem primePowerCompletedGroupAlgebraAugmentationCoeffLinear_surjective :
    Function.Surjective
      (primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ℓ) (G := G))

theorem

primePowerCompletedGAAugmentationIdealToGACoeffLinear_inj

L249 ↗

FoxDifferential.primePowerCompletedGAAugmentationIdealToGACoeffLinear_inj

Documentation

The canonical linear inclusion of the completed augmentation ideal is injective.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem primePowerCompletedGAAugmentationIdealToGACoeffLinear_inj :
    Function.Injective
      (primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
        (ℓ := ℓ) (G := G))

theorem

exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear

L273 ↗

FoxDifferential.exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear

Documentation

The coefficient-linear inclusion of the prime-power completed augmentation ideal has image equal to the kernel of the coefficient-linear augmentation.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear :
    Function.Exact
      (primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
        (ℓ := ℓ) (G := G))
      (primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ℓ) (G := G))

theorem

primePowerCompletedGAAugmentationIdealToGACoeffLinear_shortExact

L291 ↗

FoxDifferential.primePowerCompletedGAAugmentationIdealToGACoeffLinear_shortExact

Documentation

The canonical augmentation sequence with augmentation ideal as kernel is short exact: the inclusion is injective, its image is the kernel of augmentation, and the augmentation is surjective.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem primePowerCompletedGAAugmentationIdealToGACoeffLinear_shortExact :
    Function.Injective
        (primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
          (ℓ := ℓ) (G := G)) ∧
      Function.Exact
        (primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
          (ℓ := ℓ) (G := G))
        (primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ℓ) (G := G)) ∧
      Function.Surjective
        (primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ℓ) (G := G))

Module documentation

Fox differential: completed — coefficient rings — prime-power augmentation ideal — subtype linear

Declarations