SurjectivePullbackBoundary.lean

1 import PaperX.FiniteAvoidanceBoundary
2 import PaperX.IrreducibleCharacterRigidity
3 
4 /-! Two limitations of passing through a quotient. Non-surjective restriction
5 can identify inequivalent irreducible representations. Coverage in one finite
6 quotient does not imply coverage in a larger group. -/
7 set_option autoImplicit false
8 noncomputable section
9 
10 namespace PaperX.SurjectivePullbackBoundary
11 open PaperX.CompletionExamples PaperX.QuadraticCharacters
12 open PaperX.FiniteAvoidanceBoundary PaperX.ProfiniteSeparation
13 
14 /-- The actual one-dimensional sign representation over a characteristic-zero field. -/
15 def signRepresentation : Representation ℚ C2 ℚ :=
16   (algebraMap ℚ (Module.End ℚ ℚ)).toMonoidHom.comp
17     ((Units.coeHom ℚ).comp signCharacter)
18 
19 def trivialRepresentation : Representation ℚ C2 ℚ := 1
20 
21 /-- A homomorphism missing the nonidentity element. -/
22 def collapsedMap : C2 →* C2 := 1
23 
24 theorem collapsedMap_not_surjective : ¬ Function.Surjective collapsedMap := by
25   intro h
26   obtain ⟨g, hg⟩ := h generator
27   exact generator_ne_one hg.symm
28 
29 /-- Every rational representation on the one-dimensional rational vector space
30 is irreducible, independently of its acting group. -/
31 theorem rational_line_irreducible {G : Type*} [Monoid G]
32     (ρ : Representation ℚ G ℚ) : ρ.IsIrreducible := by
33   change IsSimpleOrder (Subrepresentation ρ)
34   refine { exists_pair_ne := ?_, eq_bot_or_eq_top := ?_ }
35   · refine ⟨⊥, ⊤, ?_⟩
36     intro h
37     have hh := congrArg Subrepresentation.toSubmodule h
38     exact bot_ne_top hh
39   · intro W
40     rcases eq_bot_or_eq_top W.toSubmodule with h | h
41     · exact Or.inl (Subrepresentation.toSubmodule_injective h)
42     · exact Or.inr (Subrepresentation.toSubmodule_injective h)
43 
44 instance : signRepresentation.IsIrreducible := rational_line_irreducible _
45 instance : trivialRepresentation.IsIrreducible := rational_line_irreducible _
46 
47 theorem representations_not_equivalent :
48     ¬ Nonempty (signRepresentation.Equiv trivialRepresentation) := by
49   intro h
50   have hc := PaperX.IrreducibleCharacterRigidity.character_eq_of_equiv
51     signRepresentation trivialRepresentation h
52   have hg := congrFun hc generator
53   norm_num [Representation.character, signRepresentation, trivialRepresentation,
54     signCharacter, Algebra.algebraMap_eq_smul_one] at hg
55 
56 theorem collapsed_pullbacks_equal :
57     signRepresentation.comp collapsedMap = trivialRepresentation.comp collapsedMap := by
58   ext g
59   simp [collapsedMap]
60 
61 /-- The actual restricted representations admit an equivariant linear isomorphism. -/
62 theorem collapsed_pullbacks_equivalent :
63     Nonempty (Representation.Equiv (signRepresentation.comp collapsedMap)
64       (trivialRepresentation.comp collapsedMap)) := by
65   rw [collapsed_pullbacks_equal]
66   exact ⟨Representation.Equiv.refl _⟩
67 
68 /-- Samples chosen entirely in the first factor of a larger finite group. -/
69 def quotientSamples (g : C2) : C2 × C2 := (g, 1)
70 
71 theorem projected_samples_surjective :
72     Function.Surjective (fun g : C2 => (quotientSamples g).1) := by
73   intro g
74   exact ⟨g, rfl⟩
75 
76 theorem projected_samples_coverage :
77     QuotientCoverage (fun g : C2 => (quotientSamples g).1) := by
78   intro H g
79   exact ⟨g, 1, by simp [quotientSamples]⟩
80 
81 theorem quotient_samples_not_conjugacy_dense :
82     ¬ DenseRange (fun p : C2 × (C2 × C2) =>
83       p.2 * quotientSamples p.1 * p.2⁻¹) := by
84   intro hd
85   obtain ⟨p, hp⟩ := denseRange_discrete.mp hd (1, generator)
86   have hh := congrArg Prod.snd hp
87   simp [quotientSamples] at hh
88   exact generator_ne_one hh.symm
89 
90 theorem quotient_samples_coverage_fails : ¬ QuotientCoverage quotientSamples := by
91   intro hc
92   exact quotient_samples_not_conjugacy_dense
93     (dense_of_quotient_coverage quotientSamples hc)
94 
95 end PaperX.SurjectivePullbackBoundary

Back to source controls