CompletedGroupAlgebra.finiteGroupAlgebra_mapDomainRingHom_continuous
Finite-stage group algebras are functorial by continuous ring homomorphisms.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u vLean source · full declaration
theorem finiteGroupAlgebra_mapDomainRingHom_continuous
(R : Type u) (G H : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [Group H] [Finite G] [Finite H] (φ : G →* H) :
letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
letI : TopologicalSpace (MonoidAlgebra R H) := finiteGroupAlgebraTopology R H
Continuous (MonoidAlgebra.mapDomainRingHom R φ : MonoidAlgebra R G → MonoidAlgebra R H) := by
classical
let : Fintype G := Fintype.ofFinite G
let : Fintype H := Fintype.ofFinite H
let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
let : TopologicalSpace (MonoidAlgebra R H) := finiteGroupAlgebraTopology R H
let e : MonoidAlgebra R H ≃ (H → R) :=
(MonoidAlgebra.coeffEquiv (R := R) (M := H)).trans Finsupp.equivFunOnFinite
have he : Topology.IsInducing (e : MonoidAlgebra R H → H → R) :=
Topology.IsInducing.induced e
have hcoord : ∀ g : G, Continuous fun x : MonoidAlgebra R G => x.coeff g :=
finiteGroupAlgebra_coordinate_continuous R G
rw [he.continuous_iff]
apply continuous_pi
intro h
change Continuous fun x : MonoidAlgebra R G =>
(MonoidAlgebra.mapDomainRingHom R φ x : MonoidAlgebra R H).coeff h
rw [show (fun x : MonoidAlgebra R G =>
(MonoidAlgebra.mapDomainRingHom R φ x : MonoidAlgebra R H).coeff h) =
(fun x : MonoidAlgebra R G =>
∑ g ∈ Finset.univ.filter (fun g : G => φ g = h), x.coeff g) from ?_]
· apply continuous_finsetSum
intro g _hg
exact hcoord g
· funext x
change (Finsupp.mapDomain φ x.coeff) h =
∑ g ∈ Finset.univ.filter (fun g : G => φ g = h), x.coeff g
rw [Finsupp.mapDomain, Finsupp.sum]
rw [Finsupp.finsetSum_apply]
simp only [Finsupp.single_apply]
change (∑ g ∈ x.coeff.support, if φ g = h then x.coeff g else 0) =
∑ g ∈ Finset.univ.filter (fun g : G => φ g = h), x.coeff g
rw [Finset.sum_filter]
exact Finset.sum_subset (by intro g _hg; simp only [Finset.mem_univ]) (by
intro g _hguniv hgnot
by_cases hφ : φ g = h
· simp only [hφ, ↓reduceIte, Finsupp.notMem_support_iff.mp hgnot]
· simp only [hφ, ↓reduceIte])