Skip to content

Instantly share code, notes, and snippets.

@kckennylau

kckennylau/bug.lean Secret

Created Jun 15, 2018
Embed
What would you like to do?
import analysis.topology.topological_structures
import analysis.topology.continuity
import group_theory.coset
class topological_group (α : Type*) [topological_space α] [group α] extends topological_monoid α : Prop :=
(continuous_inv : continuous (λ p : α, p⁻¹))
theorem continuous_inv {α : Type*} [topological_space α] [group α]
[topological_group α] : continuous (λ p : α, p⁻¹) :=
topological_group.continuous_inv α
theorem continuous_conj {α : Type*} [topological_space α]
[group α] [topological_group α] {y : α} :
continuous (λ x, y * x * y⁻¹) :=
continuous_mul (continuous_mul continuous_const continuous_id) continuous_const
instance topological_group.one_closure.normal_subgroup (α : Type*)
[topological_space α] [group α] [topological_group α] :
normal_subgroup (closure ({1} : set α)) :=
{ mul_mem := λ x y hx hy S ⟨hs1, hs2⟩,
have H1 : _ := continuous_iff_is_closed.1 (topological_monoid.continuous_mul α) S hs1,
have H2 : closure (set.prod ({1} : set α) ({1} : set α)) = _ := closure_prod_eq,
have H3 : (x, y) ∈ closure (set.prod ({1} : set α) ({1} : set α)),
from H2.symm ▸ ⟨hx, hy⟩,
H3 _ ⟨H1, by simpa using hs2⟩,
one_mem := λ _ ⟨_, H⟩, by simpa using H,
inv_mem := λ _ H S ⟨hs1, hs2⟩, H _
⟨continuous_iff_is_closed.1
continuous_inv _ hs1,
show ({1} : set α) ⊆ { x | x⁻¹ ∈ S },
by simpa using hs2⟩,
normal := λ x H y S ⟨hs1, hs2⟩, H _
⟨continuous_iff_is_closed.1 continuous_conj _ hs1,
show ({1} : set α) ⊆ { x | y * x * y⁻¹ ∈ S },
by simpa using hs2⟩ }
instance topological_group.coinduced {α : Type*} {β : Type*}
[t : topological_space α] [group α] [group β] [topological_group α]
(f : α → β) [is_group_hom f] (hf1 : function.surjective f)
(hf2 : ∀ S, is_open S → is_open (f ⁻¹' (f '' S))) :
@topological_group β (topological_space.coinduced f t) _ :=
by letI := topological_space.coinduced f t; from
{ continuous_mul :=
have @prod.topological_space β β
(@topological_space.coinduced α β f t)
(@topological_space.coinduced α β f t)
= @topological_space.coinduced (α × α) (β × β)
(λ p, (f p.1, f p.2)) prod.topological_space,
from have H1 : prod.fst ∘ (λ p : α × α, (f p.1, f p.2)) = f ∘ prod.fst,
from rfl,
have H2 : prod.snd ∘ (λ p : α × α, (f p.1, f p.2)) = f ∘ prod.snd,
from rfl,
have H3 : topological_space.induced f (topological_space.coinduced f t) ≤ t,
from induced_le_iff_le_coinduced.2 (le_refl _),
le_antisymm
(lattice.sup_le
(induced_le_iff_le_coinduced.1 (by rw [induced_compose, H1, ← induced_compose];
from le_trans (induced_mono H3) lattice.le_sup_left))
(induced_le_iff_le_coinduced.1 (by rw [induced_compose, H2, ← induced_compose];
from le_trans (induced_mono H3) lattice.le_sup_right)))
(λ S hs, is_open_prod_iff.2 $ λ x y hxy,
let ⟨m, hm⟩ := hf1 x, ⟨n, hn⟩ := hf1 y in
let ⟨u, v, hu, hv, hmu, hnv, H⟩ := is_open_prod_iff.1 hs m n (by simpa [hm, hn] using hxy) in
⟨f '' u, f '' v, hf2 u hu, hf2 v hv, ⟨m, hmu, hm⟩, ⟨n, hnv, hn⟩,
λ ⟨p, q⟩ ⟨⟨P, hp1, hp2⟩, ⟨Q, hq1, hq2⟩⟩,
by simp at hp2 hq2; rw [← hp2, ← hq2]; from @H (P, Q) ⟨hp1, hq1⟩⟩),
have H1 : (λ p : α × α, f p.1 * f p.2) = f ∘ (λ p : α × α, p.1 * p.2),
from funext $ λ ⟨p, q⟩, eq.symm $ is_group_hom.mul f _ _,
by rw this; from continuous_coinduced_dom
(show continuous (λ p : α × α, f p.1 * f p.2),
by rw H1; from continuous_mul'.comp continuous_coinduced_rng),
continuous_inv := continuous_coinduced_dom $
have H : (λ p, p⁻¹) ∘ f = f ∘ (λ p, p⁻¹),
from funext $ λ _, eq.symm $ is_group_hom.inv f _,
show continuous ((λ p, p⁻¹) ∘ f),
by rw H; from continuous_inv.comp continuous_coinduced_rng }
def left_cosets.mul {G : Type*} [group G] (N : set G) [normal_subgroup N] :
left_cosets N → left_cosets N → left_cosets N :=
by letI := left_rel N; from quotient.lift₂ (λ x y, ⟦x*y⟧)
(assume a₁ a₂ b₁ b₂ : G,
assume H1 : a₁⁻¹ * b₁ ∈ N,
assume H2 : a₂⁻¹ * b₂ ∈ N,
quotient.sound $ show (a₁ * a₂)⁻¹ * (b₁ * b₂) ∈ N,
from calc (a₁ * a₂)⁻¹ * (b₁ * b₂)
= (a₂⁻¹ * (a₁⁻¹ * b₁) * a₂⁻¹⁻¹) * (a₂⁻¹ * b₂) : by simp [mul_assoc]
... ∈ N : is_submonoid.mul_mem
(normal_subgroup.normal _ H1 _) H2)
def left_cosets.inv {G : Type*} [group G] (N : set G) [normal_subgroup N] :
left_cosets N → left_cosets N :=
by letI := left_rel N; from quotient.lift (λ x, ⟦x⁻¹⟧)
(assume m n : G,
assume H : m⁻¹ * n ∈ N,
quotient.sound $ show m⁻¹⁻¹ * n⁻¹ ∈ N,
from calc m⁻¹⁻¹ * n⁻¹
= m * (m⁻¹ * n)⁻¹ * m⁻¹ : by simp [mul_assoc]
... ∈ N : normal_subgroup.normal _ (is_subgroup.inv_mem H) _)
instance quotient_group {G : Type*} [group G] (N : set G) [normal_subgroup N] :
group (left_cosets N) :=
by letI := left_rel N; from
{ mul := left_cosets.mul N,
mul_assoc := λ x y z, quotient.induction_on₃ x y z $ λ p q r,
show ⟦p * q * r⟧ = ⟦p * (q * r)⟧, by rw mul_assoc,
one := ⟦1⟧,
one_mul := λ x, quotient.induction_on x $ λ m,
show1 * m⟧ = ⟦m⟧, by rw one_mul,
mul_one := λ x, quotient.induction_on x $ λ m,
show ⟦m * 1⟧ = ⟦m⟧, by rw mul_one,
inv := left_cosets.inv N,
mul_left_inv := λ x, quotient.induction_on x $ λ m,
show ⟦m⁻¹ * m⟧ = ⟦1⟧, by rw mul_left_inv }
inductive abelianization.rel (G : Type*) [group G] : G → G → Prop
| basic : ∀ x y z w, abelianization.rel (x * y * z * w) (x * z * y * w)
def abelianization (G : Type*) [group G] : Type* :=
quot (abelianization.rel G)
def abelianization.mul (G : Type*) [group G] :
abelianization G → abelianization G → abelianization G :=
begin
refine quot.lift (λ x, quot.lift (λ y, quot.mk (rel G) (x * y)) _) _,
{ intros m n h,
cases h with m n p q,
calc quot.mk (rel G) (x * ((m * n * p) * q))
= quot.mk (rel G) (x * m * n * p * q) : by simp [mul_assoc]
... = quot.mk (rel G) (x * m * p * n * q) : quot.sound ⟨_, _, _, _⟩
... = quot.mk (rel G) (x * ((m * p * n) * q)) : by simp [mul_assoc] },
{ intros m n h,
apply funext,
apply quot.ind,
intro x,
cases h with m n p q,
calc quot.mk (rel G) (m * n * p * q * x)
= quot.mk (rel G) (m * n * p * (q * x)) : by simp [mul_assoc]
... = quot.mk (rel G) (m * p * n * (q * x)) : quot.sound ⟨_, _, _, _⟩
... = quot.mk (rel G) (m * p * n * q * x) : by simp [mul_assoc] }
end
def abelianization.inv (G : Type*) [group G] :
abelianization G → abelianization G :=
begin
refine quot.lift (λ x, quot.mk _ (x⁻¹)) _,
intros m n h,
cases h with m n p q,
calc quot.mk (rel G) (m * n * p * q)⁻¹
= quot.mk (rel G) (q⁻¹ * p⁻¹ * n⁻¹ * m⁻¹) : by simp [mul_assoc]
... = quot.mk (rel G) (q⁻¹ * n⁻¹ * p⁻¹ * m⁻¹) : quot.sound ⟨_, _, _, _⟩
... = quot.mk (rel G) (m * p * n * q)⁻¹ : by simp [mul_assoc]
end
instance abelianization.comm_group (G : Type*) [group G] :
comm_group (abelianization G) :=
{ mul := abelianization.mul G,
mul_assoc := by repeat { refine quot.ind (λ x, _) }; simp [abelianization.mul, mul_assoc],
one := quot.mk _ 1,
one_mul := by refine quot.ind (λ x, _); simp [abelianization.mul],
mul_one := by refine quot.ind (λ x, _); simp [abelianization.mul]; congr; apply mul_one,
inv := abelianization.inv G,
mul_left_inv := by refine quot.ind (λ x, _); simp [abelianization.mul, abelianization.inv]; refl,
mul_comm := by refine quot.ind (λ x, _); refine quot.ind (λ y, _); simp [abelianization.mul];
suffices : quot.mk (rel G) (1 * x * y * 1) = quot.mk (rel G) (1 * y * x * 1);
[simpa, from quot.sound ⟨_, _, _, _⟩] }
instance abelianization.comm_group' (G : Type*) [group G] :
comm_group (quot (rel G)) :=
abelianization.comm_group G
instance abelianization.is_group_hom (G : Type*) [group G] :
is_group_hom (quot.mk (rel G) : G → abelianization G) :=
⟨λ x y, rfl⟩
instance abelianization.topological_space (G : Type*) [t : topological_space G] [group G]
[topological_group G] : topological_space (abelianization G) :=
topological_space.coinduced (quot.mk _) t
instance abelianization.topological_group (G : Type*) [topological_space G] [group G]
[topological_group G] : topological_group (abelianization G) :=
topological_group.coinduced (quot.mk (rel G)) quot.exists_rep $ λ S hs,
have (⋃ x : { x // quot.mk (rel G) x = 1}, (λ y, x.1 * y) ⁻¹' S)
= quot.mk (rel G) ⁻¹' (quot.mk (rel G) '' S),
from set.ext $ λ z,
⟨λ ⟨S, ⟨⟨g, h1⟩, rfl⟩, h2⟩, ⟨g * z, h2, by simp [is_group_hom.mul (quot.mk (rel G)), h1]⟩,
λ ⟨g, h1, h2⟩, ⟨_, ⟨⟨g * z⁻¹, by simp [is_group_hom.mul (quot.mk (rel G)), is_group_hom.inv (quot.mk (rel G)), h2]⟩, rfl⟩, by simp [h1]⟩⟩,
this ▸ is_open_Union $ λ x : {x // quot.mk (rel G) x = 1},
continuous_mul continuous_const continuous_id _ hs
/-{ continuous_mul := λ S hs1, is_open_prod_iff.2 $
have _ := is_open_prod_iff.1 (topological_monoid.continuous_mul G _ hs1),
by refine quot.ind (λ x, _); refine quot.ind (λ y, _);
from λ h, let ⟨u, v, hu, hv, hxu, hyv, H⟩ := this x y h in
⟨quot.mk _ '' u, quot.mk _ '' v,
show is_open (quot.mk (rel G) ⁻¹' (quot.mk (rel G) '' u)),
from have (⋃ x : { x // quot.mk (rel G) x = 1}, (λ y, x.1 * y) ⁻¹' u)
= quot.mk (rel G) ⁻¹' (quot.mk (rel G) '' u),
from set.ext $ λ z,
⟨λ ⟨S, ⟨⟨g, h1⟩, rfl⟩, h2⟩, ⟨g * z, h2, by simp [is_group_hom.mul (quot.mk (rel G)), h1]⟩,
λ ⟨g, h1, h2⟩, ⟨_, ⟨⟨g * z⁻¹, by simp [is_group_hom.mul (quot.mk (rel G)), is_group_hom.inv (quot.mk (rel G)), h2]⟩, rfl⟩, by simp [h1]⟩⟩,
this ▸ is_open_Union $ λ x : {x // quot.mk (rel G) x = 1},
(continuous_mul continuous_const continuous_id) _ hu,
show is_open (quot.mk (rel G) ⁻¹' (quot.mk (rel G) '' v)),
from have (⋃ x : { x // quot.mk (rel G) x = 1}, (λ y, x.1 * y) ⁻¹' v)
= quot.mk (rel G) ⁻¹' (quot.mk (rel G) '' v),
from set.ext $ λ z,
⟨λ ⟨S, ⟨⟨g, h1⟩, rfl⟩, h2⟩, ⟨g * z, h2, by simp [is_group_hom.mul (quot.mk (rel G)), h1]⟩,
λ ⟨g, h1, h2⟩, ⟨_, ⟨⟨g * z⁻¹, by simp [is_group_hom.mul (quot.mk (rel G)), is_group_hom.inv (quot.mk (rel G)), h2]⟩, rfl⟩, by simp [h1]⟩⟩,
this ▸ is_open_Union $ λ x : {x // quot.mk (rel G) x = 1},
(continuous_mul continuous_const continuous_id) _ hv,
⟨x, hxu, rfl⟩, ⟨y, hyv, rfl⟩,
λ ⟨p, q⟩, by refine quot.induction_on p (λ m, _);
refine quot.induction_on q (λ n, _);
from λ ⟨⟨P, hp1, hp2⟩, ⟨Q, hq1, hq2⟩⟩,
suffices quot.mk (rel G) P * quot.mk (rel G) Q ∈ S,
by rw [hp2, hq2] at this; simpa using this,
@H (P, Q) ⟨hp1, hq1⟩⟩,
continuous_inv := λ S hs,
show is_open (quot.mk (rel G) ⁻¹' ((λ p : abelianization G, p⁻¹) ⁻¹' S)),
from have (λ p : G, p⁻¹) ⁻¹' (quot.mk (rel G) ⁻¹' S)
= quot.mk (rel G) ⁻¹' ((λ p : abelianization G, p⁻¹) ⁻¹' S),
from set.ext $ λ z, by simp [is_group_hom.inv (quot.mk (rel G))],
this ▸ (topological_group.continuous_inv G _ $
continuous_coinduced_rng _ hs) }-/
def Hausdorff_abelianization (G : Type*) [topological_space G] [group G]
[topological_group G] :=
left_cosets (closure ({1} : set (abelianization G)))
instance Hausdorff_abelianization.setoid (G : Type*) [topological_space G] [group G]
[topological_group G] : setoid (abelianization G) :=
left_rel $ closure {1}
instance Hausdorff_abelianization.comm_group (G : Type*) [topological_space G] [group G]
[topological_group G] : comm_group (Hausdorff_abelianization G) :=
{ mul_comm := λ x y, quotient.induction_on₂ x y $ λ m n,
show ⟦m * n⟧ = ⟦n * m⟧, by rw mul_comm,
.. quotient_group _ }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment