GroupRing.lean

def augmentationAlgHom : GroupRing H →ₐ[ℤ] ℤ

def augmentation : GroupRing H →+* ℤ

def augmentationIdeal : Ideal (GroupRing H)

def augmentationGeneratorIdeal : Ideal (GroupRing H)

theorem augmentation_of (h : H) :
    augmentation H (MonoidAlgebra.of ℤ H h) = 1

theorem augmentation_one :
    augmentation H (1 : GroupRing H) = 1

theorem mem_augmentationIdeal_iff {x : GroupRing H} :
    x ∈ augmentationIdeal H ↔ augmentation H x = 0

theorem groupRingBoundary_mem_augmentationIdeal
    {G : Type*} [Group G] (ψ : G →* H) (g : G) :
    groupRingBoundary ψ g ∈ augmentationIdeal H

theorem augmentationGenerator_mem_augmentationIdeal (h : H) :
    augmentationGenerator H h ∈ augmentationIdeal H

theorem augmentationGenerator_mem_augmentationGeneratorIdeal (h : H) :
    augmentationGenerator H h ∈ augmentationGeneratorIdeal H

theorem augmentationGeneratorIdeal_le_augmentationIdeal :
    augmentationGeneratorIdeal H ≤ augmentationIdeal H

theorem exists_mem_augmentationGeneratorIdeal_add (x : GroupRing H) :
    ∃ y ∈ augmentationGeneratorIdeal H, x = y + (augmentation H x : GroupRing H)

theorem augmentationIdeal_le_augmentationGeneratorIdeal :
    augmentationIdeal H ≤ augmentationGeneratorIdeal H

theorem augmentationGeneratorIdeal_eq_augmentationIdeal :
    augmentationGeneratorIdeal H = augmentationIdeal H

def augmentationBoundary (ψ : G →* H) (g : G) : augmentationIdeal H

def augmentationGeneratorSubtype (h : H) : augmentationIdeal H

theorem toGroupRing_mem_augmentationIdeal (ψ : G →* H) (x : DifferentialModule ψ) :
    toGroupRing ψ x ∈ augmentationIdeal H

def toAugmentationIdeal (ψ : G →* H) :
    DifferentialModule ψ →ₗ[GroupRing H] augmentationIdeal H

theorem toAugmentationIdeal_d (ψ : G →* H) (g : G) :
    toAugmentationIdeal (H := H) ψ (universalDifferential ψ g) =
      augmentationBoundary (H := H) ψ g

theorem subtype_comp_toAugmentationIdeal (ψ : G →* H) :
    (augmentationIdeal H).subtype.comp (toAugmentationIdeal (H := H) ψ) =
      toGroupRing ψ

theorem span_augmentationGeneratorSubtype_eq_top :
    Submodule.span (GroupRing H) (Set.range (augmentationGeneratorSubtype (H := H))) = ⊤

theorem toAugmentationIdeal_surjective (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Surjective (toAugmentationIdeal (H := H) ψ)

theorem toGroupRing_id_injective :
    Function.Injective (toGroupRing (MonoidHom.id H))

def augmentationIdealToIdentityDifferentialModule :
    augmentationIdeal H →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) where
  toFun x :=
    monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1
  map_add' x y := by
    change
      monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (x.1 + y.1) =
        monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1 +
          monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) y.1
    simp only [map_add]
  map_smul' r x := by
    change
      monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (r * x.1) =
        r • monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1
    apply identityCrossedDifferentialBoundary_injective (S := ℤ) (G := H)
    have hxaug :
        (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) x.1 = 0 :=
      (mem_augmentationIdeal_iff (H := H)).1 x.2
    have hrxaug :
        (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) (r * x.1) = 0 := by
      rw [map_mul, hxaug, mul_zero]
    calc
      identityCrossedDifferentialBoundary (S := ℤ) (G := H)
          (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (r * x.1)) =
        r * x.1 := by
          exact
            idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
              (S := ℤ) (G := H) hrxaug
      _ =
        r * identityCrossedDifferentialBoundary (S := ℤ) (G := H)
          (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) := by
          exact congrArg (fun z => r * z)
            (idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
              (S := ℤ) (G := H) hxaug).symm
      _ =
        identityCrossedDifferentialBoundary (S := ℤ) (G := H)
          (r • monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) := by
          exact
            (LinearMap.map_smul
              (identityCrossedDifferentialBoundary (S := ℤ) (G := H)) r
              (monoidAlgebraToIdentityCrossedDifferentialModule
                (S := ℤ) (G := H) x.1)).symm

theorem toAugmentationIdeal_augmentationIdealToIdentityDifferentialModule
    (x : augmentationIdeal H) :
    toAugmentationIdeal (H := H) (MonoidHom.id H)
        (augmentationIdealToIdentityDifferentialModule (H := H) x) = x

theorem augmentationIdealToIdentityDifferentialModule_toAugmentationIdeal
    (x : DifferentialModule (MonoidHom.id H)) :
    augmentationIdealToIdentityDifferentialModule (H := H)
        (toAugmentationIdeal (H := H) (MonoidHom.id H) x) = x

def identityDifferentialModuleEquivAugmentationIdeal :
    DifferentialModule (MonoidHom.id H) ≃ₗ[GroupRing H] augmentationIdeal H where
  toLinearMap := toAugmentationIdeal (H := H) (MonoidHom.id H)
  invFun := augmentationIdealToIdentityDifferentialModule (H := H)
  left_inv := augmentationIdealToIdentityDifferentialModule_toAugmentationIdeal (H := H)
  right_inv := toAugmentationIdeal_augmentationIdealToIdentityDifferentialModule (H := H)

theorem identityDifferentialModuleEquivAugmentationIdeal_toLinearMap :
    (identityDifferentialModuleEquivAugmentationIdeal (H := H)).toLinearMap =
      toAugmentationIdeal (H := H) (MonoidHom.id H)