Abstract.lean

def groupAlgebraAugmentation
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    MonoidAlgebra R G →+* R

theorem groupAlgebraAugmentation_of
    (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
    groupAlgebraAugmentation R G (MonoidAlgebra.of R G g) = 1

theorem groupAlgebraAugmentation_single
    (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) (r : R) :
    groupAlgebraAugmentation R G (MonoidAlgebra.single g r) = r

theorem groupAlgebraAugmentation_algebraMap
    (R : Type u) (G : Type v) [CommRing R] [Group G] (r : R) :
    groupAlgebraAugmentation R G (algebraMap R (MonoidAlgebra R G) r) = r

theorem groupAlgebraAugmentation_surjective
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Function.Surjective (groupAlgebraAugmentation R G)

def groupAlgebraAugmentationLinearMap
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    MonoidAlgebra R G →ₗ[R] R where
  toFun := groupAlgebraAugmentation R G
  map_add' := by
    intro x y
    exact map_add (groupAlgebraAugmentation R G) x y
  map_smul' := by
    intro r x
    simp only [Algebra.smul_def, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
        RingHom.coe_id,
  Function.comp_apply, id_eq, map_mul, groupAlgebraAugmentation_single, RingHom.id_apply]

theorem groupAlgebraAugmentationLinearMap_apply
    (R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
    groupAlgebraAugmentationLinearMap R G x = groupAlgebraAugmentation R G x

theorem groupAlgebraAugmentationLinearMap_surjective
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Function.Surjective (groupAlgebraAugmentationLinearMap R G)

def groupAlgebraAugmentationIdeal
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Ideal (MonoidAlgebra R G)

def groupAlgebraAugmentationIdealSubmodule
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Submodule R (MonoidAlgebra R G)

theorem mem_groupAlgebraAugmentationIdeal_iff
    {R : Type u} {G : Type v} [CommRing R] [Group G] {x : MonoidAlgebra R G} :
    x ∈ groupAlgebraAugmentationIdeal R G ↔ groupAlgebraAugmentation R G x = 0

theorem mem_groupAlgebraAugmentationIdealSubmodule_iff
    {R : Type u} {G : Type v} [CommRing R] [Group G] {x : MonoidAlgebra R G} :
    x ∈ groupAlgebraAugmentationIdealSubmodule R G ↔ groupAlgebraAugmentation R G x = 0

theorem groupAlgebraAugmentationIdeal_subtype_injective
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Function.Injective
      (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G)) := by
  intro x y hxy
  exact Subtype.ext hxy

theorem exact_groupAlgebraAugmentationIdeal_subtype
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Function.Exact
      (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G))
      (groupAlgebraAugmentation R G) := by
  intro x
  constructor
  · intro hx
    exact ⟨⟨x, hx⟩, rfl⟩
  · rintro ⟨y, rfl⟩
    exact y.2

theorem groupAlgebraAugmentation_shortExact
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Function.Injective
        (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G)) ∧
      Function.Exact
        (fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G))
        (groupAlgebraAugmentation R G) ∧
      Function.Surjective (groupAlgebraAugmentation R G) := by
  exact ⟨groupAlgebraAugmentationIdeal_subtype_injective R G,
    exact_groupAlgebraAugmentationIdeal_subtype R G,
    groupAlgebraAugmentation_surjective R G⟩

def groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    groupAlgebraAugmentationIdealSubmodule R G →ₗ[R] MonoidAlgebra R G

theorem groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap_injective
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Function.Injective (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G)

theorem exact_groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Function.Exact
      (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G)
      (groupAlgebraAugmentationLinearMap R G)

theorem groupAlgebraAugmentationLinearMap_shortExact
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Function.Injective (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G) ∧
      Function.Exact
        (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G)
        (groupAlgebraAugmentationLinearMap R G) ∧
      Function.Surjective (groupAlgebraAugmentationLinearMap R G)

def groupAlgebraAugmentationGenerator
    (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
    MonoidAlgebra R G

def groupAlgebraAugmentationGeneratorIdeal
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Ideal (MonoidAlgebra R G)

theorem groupAlgebraAugmentationGenerator_mem_augmentationIdeal
    (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
    groupAlgebraAugmentationGenerator R G g ∈ groupAlgebraAugmentationIdeal R G

theorem groupAlgebraAugmentationGenerator_mem_generatorIdeal
    (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
    groupAlgebraAugmentationGenerator R G g ∈
      groupAlgebraAugmentationGeneratorIdeal R G

theorem groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    groupAlgebraAugmentationGeneratorIdeal R G ≤ groupAlgebraAugmentationIdeal R G

theorem exists_mem_groupAlgebraAugmentationGeneratorIdeal_add
    (R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
    ∃ y ∈ groupAlgebraAugmentationGeneratorIdeal R G,
      x = y + algebraMap R (MonoidAlgebra R G) (groupAlgebraAugmentation R G x)

theorem groupAlgebraAugmentationGeneratorIdeal_eq_augmentationIdeal
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    groupAlgebraAugmentationGeneratorIdeal R G = groupAlgebraAugmentationIdeal R G

def groupAlgebraAugmentationGeneratorSubtype
    (R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
    groupAlgebraAugmentationIdeal R G

theorem groupAlgebraAugmentationGeneratorSubtype_span_eq_top
    (R : Type u) (G : Type v) [CommRing R] [Group G] :
    Submodule.span (MonoidAlgebra R G)
      (Set.range (groupAlgebraAugmentationGeneratorSubtype R G)) = ⊤

theorem finiteGroupAlgebra_augmentation_apply_eq_sum
    (R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G]
    (x : MonoidAlgebra R G) :
    letI : Fintype G := Fintype.ofFinite G
    groupAlgebraAugmentation R G x = ∑ g : G, x.coeff g := by
  classical
  let : Fintype G := Fintype.ofFinite G
  calc
    groupAlgebraAugmentation R G x = x.coeff.sum (fun _ r => r) := by
      simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
          MonoidAlgebra.lift_apply,
  MonoidHom.one_apply, smul_eq_mul, mul_one]
    _ = ∑ g : G, x.coeff g := by
      exact Finsupp.sum_fintype x.coeff (fun _ r => r) (by intro g; simp only)

theorem finiteGroupAlgebra_algebraMap_continuous
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [Group G] [Finite G] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    Continuous (algebraMap R (MonoidAlgebra R G)) := by
  classical
  let : Fintype G := Fintype.ofFinite G
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  let e : MonoidAlgebra R G ≃ (G → R) :=
    (MonoidAlgebra.coeffEquiv (R := R) (M := G)).trans Finsupp.equivFunOnFinite
  have he : Topology.IsInducing (e : MonoidAlgebra R G → G → R) :=
    Topology.IsInducing.induced e
  rw [he.continuous_iff]
  apply continuous_pi
  intro g
  change Continuous fun r : R => (MonoidAlgebra.single (1 : G) r).coeff g
  by_cases hg : g = 1
  · subst g
    simpa only [MonoidAlgebra.coeff_single, Finsupp.single_apply, ite_eq_left] using
      (continuous_id' : Continuous fun r : R => r)
  · rw [show (fun r : R => (MonoidAlgebra.single (1 : G) r).coeff g) =
        (fun _ : R => 0) from by
          funext r
          simp only [MonoidAlgebra.coeff_single, Finsupp.single_apply,
            ite_eq_right (Ne.symm hg)]]
    exact continuous_const

theorem finiteGroupAlgebra_augmentation_continuous
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [Finite G] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    Continuous (groupAlgebraAugmentation R G) := by
  classical
  let : Fintype G := Fintype.ofFinite G
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  change Continuous (fun x : MonoidAlgebra R G => groupAlgebraAugmentation R G x)
  rw [show (fun x : MonoidAlgebra R G => groupAlgebraAugmentation R G x) =
      (fun x : MonoidAlgebra R G => ∑ g : G, x.coeff g) from by
        funext x
        exact finiteGroupAlgebra_augmentation_apply_eq_sum R G x]
  apply continuous_finsetSum
  intro g _hg
  exact finiteGroupAlgebra_coordinate_continuous R G g

theorem groupAlgebraAugmentation_mapDomainRingHom
    (R : Type u) (G : Type v) (H : Type w) [CommRing R] [Group G] [Group H]
    (φ : G →* H) (x : MonoidAlgebra R G) :
    groupAlgebraAugmentation R H (MonoidAlgebra.mapDomainRingHom R φ x) =
      groupAlgebraAugmentation R G x

theorem groupAlgebraAugmentation_mapRangeRingHom
    (R : Type u) (S : Type w) (G : Type v) [CommRing R] [CommRing S] [Group G]
    (f : R →+* S) (x : MonoidAlgebra R G) :
    groupAlgebraAugmentation S G (MonoidAlgebra.mapRingHom G f x) =
      f (groupAlgebraAugmentation R G x)