Yamaguchi26AbfaithfulGalois.equivariant_action_kernels
An equivariant injection B ↪ A and equivariant surjection B ↠ C give ker(ρA) ≤ ker(ρB) ≤ ker(ρC). The remaining conjuncts state the nontriviality, faithfulness, and triviality consequences in the observation.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
universe u v w xLean source · statement
theorem equivariant_action_kernels
{Q : Type u} {A : Type v} {B : Type w} {C : Type x}
[Group Q] [Group A] [Group B] [Group C]
(ρA : Q →* MulAut A) (ρB : Q →* MulAut B) (ρC : Q →* MulAut C)
(i : B →* A) (hi : Function.Injective i)
(s : B →* C) (hs : Function.Surjective s)
(hi_equivariant : ∀ (q : Q) (b : B), i (ρB q b) = ρA q (i b))
(hs_equivariant : ∀ (q : Q) (b : B), s (ρB q b) = ρC q (s b)) :
(∀ q : Q, ρA q = 1 → ρB q = 1) ∧
(∀ q : Q, ρB q = 1 → ρC q = 1) ∧
((∃ q : Q, ρC q ≠ 1) → ∃ q : Q, ρA q ≠ 1) ∧
(Function.Injective ρC → Function.Injective ρA) ∧
((∀ q : Q, ρA q = 1) → ∀ q : Q, ρC q = 1)