FiniteJointQuotient108.lean

1 import PaperXI.SmoothDegreeQuotient
2 import Mathlib.Topology.Algebra.OpenSubgroup
3 
4 /-! A single finite quotient for two smooth actions, constructed from their
5 actual joint kernel. No faithful quotient or finite image is assumed. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.FiniteJointQuotient108
9 open Representation
10 variable {k K W U : Type*} [Field k] [Group K]
11   [AddCommGroup W] [Module k W] [AddCommGroup U] [Module k U]
12 
13 def kernel (ρ : Representation k K W) (σ : Representation k K U) : Subgroup K :=
14   ρ.ker ⊓ σ.ker
15 
16 instance kernel_normal (ρ : Representation k K W) (σ : Representation k K U) :
17     (kernel ρ σ).Normal := by unfold kernel; infer_instance
18 
19 abbrev quotient (ρ : Representation k K W) (σ : Representation k K U) := K ⧸ kernel ρ σ
20 
21 def first (ρ : Representation k K W) (σ : Representation k K U) :
22     Representation k (quotient ρ σ) W :=
23   QuotientRepresentation.descend (kernel ρ σ) ρ inf_le_left
24 
25 def second (ρ : Representation k K W) (σ : Representation k K U) :
26     Representation k (quotient ρ σ) U :=
27   QuotientRepresentation.descend (kernel ρ σ) σ inf_le_right
28 
29 @[simp] theorem first_comp (ρ : Representation k K W) (σ : Representation k K U) :
30     (first ρ σ).comp (QuotientGroup.mk' (kernel ρ σ)) = ρ := rfl
31 
32 @[simp] theorem second_comp (ρ : Representation k K W) (σ : Representation k K U) :
33     (second ρ σ).comp (QuotientGroup.mk' (kernel ρ σ)) = σ := rfl
34 
35 variable [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K]
36   [FiniteDimensional k W] [FiniteDimensional k U]
37 
38 /-- Finiteness follows from compactness and smoothness on finite-dimensional
39 carriers; the two actions descend through the same quotient. -/
40 theorem finite (ρ : Representation k K W) (σ : Representation k K U)
41     (hρ : SmoothDegreeQuotient.IsSmooth ρ) (hσ : SmoothDegreeQuotient.IsSmooth σ) :
42     Finite (quotient ρ σ) :=
43   (kernel ρ σ).quotient_finite_of_isOpen
44     ((SmoothDegreeQuotient.isOpen_kernel_of_smooth ρ hρ).inter
45       (SmoothDegreeQuotient.isOpen_kernel_of_smooth σ hσ))
46 
47 end PaperXI.FiniteJointQuotient108

Back to source controls