Grace/Cumulus/Algebra/Group/Kernel.g17

Open in Workbench Download source

Imports

Homomorphism · Set.Function.Image

Declarations

Source

1-- Kernels and images of group homomorphisms: both are subgroups, a2-- homomorphism is injective exactly when its kernel is trivial, and3-- subgroups pull back and push forward along homomorphisms4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Algebra.Group.Kernel10import Homomorphism11import Set.Function.Image1213-- The kernel of f : G →* H: the elements sent to the unit, written ker(f)14-- wherever a hypothesis in scope supplies the homomorphism.15def kernel (f G H : Set) : Set := { x ∈ G.carrier | f(x) = H.one }1617notation function "ker(f)" => kernel(f, G, H) via hypothesis GroupHom(f, G, H)1819theorem kernel.subset (f G H : Set)20  shows kernel(f, G, H) ⊆ G.carrier21proof22  intros x hx23  have parts := kernel.membership.forward with hx24  exact parts.left2526theorem kernel.mem_carrier (f G H x : Set)27  requires hx : x ∈ kernel(f, G, H)28  shows x ∈ G.carrier29proof30  have parts := kernel.membership.forward with hx31  exact parts.left3233theorem kernel.value (f G H x : Set)34  requires hx : x ∈ kernel(f, G, H)35  shows f(x) = H.one36proof37  have parts := kernel.membership.forward with hx38  exact parts.right3940theorem kernel.of_value (f G H x : Set)41  requires hx : x ∈ G.carrier42  requires vanishes : f(x) = H.one43  shows x ∈ kernel(f, G, H)44proof45  exact kernel.membership.backward with ⟨hx, vanishes⟩4647section KernelLaws48variable (f G H : Set)49hypothesis hom : f : G →* H5051theorem GroupHom.one_mem_kernel52  shows G.one ∈ ker(f)53proof54  have group := GroupHom.source with hom55  have unitIn : G.one ∈ G := Group.one_mem with *56  have value := GroupHom.map_one with hom57  exact kernel.of_value with unitIn, value5859theorem GroupHom.kernel_subgroup60  shows Subgroup(ker(f), G)61proof62  apply Subgroup.mk with (GroupHom.source with hom), (kernel.subset at f, G, H), (GroupHom.one_mem_kernel with hom)63  . intros x hx y hy64    obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx65    obtain ⟨yIn, vy⟩ := kernel.membership.forward with hy66    have vanishes : f(x * y) = H.one by simp [GroupHom.map_mul, vx, vy, one_mul]67    exact kernel.of_value with (Group.mul_mem with *), vanishes68  . intros x hx69    obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx70    have vanishes : f(x⁻¹) = H.one by simp [GroupHom.map_inv, vx, inv_one]71    exact kernel.of_value with (Group.inv_mem with *), vanishes7273-- Two elements have the same image exactly when they differ by an74-- element of the kernel.75theorem GroupHom.apply_eq_iff (a b : G)76  shows f(a) = f(b) ↔ a⁻¹ * b ∈ ker(f)77proof78  have group := GroupHom.source with hom79  have target := GroupHom.target with hom80  have preserved : f(a⁻¹ * b) = f(a)⁻¹ * f(b) := GroupHom.map_inv_mul with *81  have criterion : f(a)⁻¹ * f(b) = H.one ↔ f(a) = f(b) := inv_mul_eq_one with *82  constructor83  . intro equal84    have vanishes := criterion.backward with equal85    rw ← preserved at vanishes86    exact kernel.of_value with (Group.mul_mem with *), vanishes87  . intro member88    have vanishes := kernel.value with member89    rw preserved at vanishes90    exact criterion.forward with vanishes9192theorem GroupHom.injective_of_kernel_trivial93  requires trivial : ∀ x ∈ ker(f), x = G.one94  shows InjectiveBetween(f, G.carrier, H.carrier)95proof96  have group := GroupHom.source with hom97  have function := GroupHom.function with hom98  constructor99  . exact function100  . intros x hx y hy z hz hxz hyz101    have vx := FunctionBetween.apply_value with function, hx, hxz102    have vy := FunctionBetween.apply_value with function, hy, hyz103    have same : f(x) = f(y) by cc104    have criterion : f(x) = f(y) ↔ x⁻¹ * y ∈ ker(f) := GroupHom.apply_eq_iff with *105    have vanishes := trivial with x⁻¹ * y, (criterion.forward with same)106    have solved : x⁻¹ * y = G.one ↔ x = y := inv_mul_eq_one with *107    exact solved.forward with vanishes108109theorem GroupHom.kernel_trivial_of_injective110  requires injective : InjectiveBetween(f, G.carrier, H.carrier)111  shows ∀ x ∈ ker(f), x = G.one112proof113  have group := GroupHom.source with hom114  intros x hx115  obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx116  have unitIn : G.one ∈ G := Group.one_mem with *117  have unitValue := GroupHom.map_one with hom118  have same : f(x) = f(G.one) by cc119  exact Injective.apply_cancel with injective, xIn, unitIn, same120121theorem GroupHom.injective_iff_kernel_trivial122  shows InjectiveBetween(f, G.carrier, H.carrier) ↔ ker(f) = {G.one}123proof124  have subgroup := GroupHom.kernel_subgroup with hom125  have criterion := Subgroup.eq_trivial_iff with subgroup126  constructor127  . intro injective128    have trivial := GroupHom.kernel_trivial_of_injective with hom, injective129    exact criterion.backward with trivial130  . intro equal131    have trivial := criterion.forward with equal132    exact GroupHom.injective_of_kernel_trivial with hom, trivial133134theorem GroupHom.kernel_eq_preimage135  shows ker(f) = functionPreimage(f, G.carrier, {H.one})136proof137  ext x138  constructor139  . intro hx140    obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx141    have value : f(x) ∈ {H.one}142      rw vx143      exact singleton.self144    exact functionPreimage.of_apply with xIn, value145  . intro hx146    have parts := functionPreimage.membership.forward with hx147    have equal := singleton.membership.forward with parts.right148    exact kernel.of_value with parts.left, equal149150-- Images of subgroups are subgroups.151theorem GroupHom.image_subgroup (K : Set)152  requires subgroup : Subgroup(K, G)153  shows Subgroup(functionImage(f, K, H.carrier), H)154proof155  have group := GroupHom.source with hom156  have target := GroupHom.target with hom157  have unitValue := GroupHom.map_one with hom158  have unitK : G.one ∈ K := Subgroup.one_mem with *159  have unitIn : H.one ∈ functionImage(f, K, H.carrier)160    have fUnit : f(G.one) ∈ H by typecheck161    apply functionImage.membership.backward162    refine ⟨?_, G.one, unitK, ?_⟩163    . rwa ← unitValue164    . symm165      exact unitValue166  apply Subgroup.mk with target, (functionImage.subset at f, K, H.carrier), unitIn167  . intros y hy w hw168    obtain ⟨yIn, a, ha, ya⟩ := functionImage.membership.forward with hy169    obtain ⟨wIn, b, hb, wb⟩ := functionImage.membership.forward with hw170    have closed : a * b ∈ K := Subgroup.mul_mem with *171    have product : y * w ∈ H by typecheck172    have preserved : f(a * b) = f(a) * f(b) := GroupHom.map_mul with *173    apply functionImage.membership.backward174    refine ⟨product, a * b, closed, ?_⟩175    cc176  . intros y hy177    obtain ⟨yIn, a, ha, ya⟩ := functionImage.membership.forward with hy178    have closed : a⁻¹ ∈ K := Subgroup.inv_mem with *179    have invY : y⁻¹ ∈ H by typecheck180    have preserved : f(a⁻¹) = f(a)⁻¹ := GroupHom.map_inv with *181    apply functionImage.membership.backward182    refine ⟨invY, a⁻¹, closed, ?_⟩183    cc184185theorem GroupHom.range_subgroup186  shows Subgroup(functionImage(f, G.carrier, H.carrier), H)187proof188  have group := GroupHom.source with hom189  have whole := Subgroup.whole with group190  exact GroupHom.image_subgroup with hom, whole191192-- Preimages of subgroups are subgroups.193theorem GroupHom.preimage_subgroup (K : Set)194  requires subgroup : Subgroup(K, H)195  shows Subgroup(functionPreimage(f, G.carrier, K), G)196proof197  have group := GroupHom.source with hom198  have target := GroupHom.target with hom199  have unitValue := GroupHom.map_one with hom200  have unitK : H.one ∈ K := Subgroup.one_mem with *201  have unitG : G.one ∈ G := Group.one_mem with *202  have unitIn : G.one ∈ functionPreimage(f, G.carrier, K)203    have value : f(G.one) ∈ K by rwa unitValue204    exact functionPreimage.of_apply with unitG, value205  apply Subgroup.mk with group, (functionPreimage.subset at f, G.carrier, K), unitIn206  . intros x hx y hy207    have px := functionPreimage.membership.forward with hx208    have py := functionPreimage.membership.forward with hy209    have xIn := px.left210    have yIn := py.left211    have inK : f(x) * f(y) ∈ K := Subgroup.mul_mem with subgroup, px.right, py.right212    have preserved : f(x * y) = f(x) * f(y) := GroupHom.map_mul with *213    have value : f(x * y) ∈ K by rwa preserved214    exact functionPreimage.of_apply with (Group.mul_mem with *), value215  . intros x hx216    have px := functionPreimage.membership.forward with hx217    have xIn := px.left218    have inK : f(x)⁻¹ ∈ K := Subgroup.inv_mem with subgroup, px.right219    have preserved : f(x⁻¹) = f(x)⁻¹ := GroupHom.map_inv with *220    have value : f(x⁻¹) ∈ K by rwa preserved221    exact functionPreimage.of_apply with (Group.inv_mem with *), value222223theorem GroupHom.kernel_subset_preimage (K : Set)224  requires subgroup : Subgroup(K, H)225  shows ker(f) ⊆ functionPreimage(f, G.carrier, K)226proof227  have unitK : H.one ∈ K := Subgroup.one_mem with subgroup228  intros x hx229  obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx230  have value : f(x) ∈ K by rwa vx231  exact functionPreimage.of_apply with xIn, value232233theorem GroupHom.image_mono (K L : Set)234  requires included : K ⊆ L235  shows functionImage(f, K, H.carrier) ⊆ functionImage(f, L, H.carrier)236proof237  intros y hy238  obtain ⟨yIn, a, ha, ya⟩ := functionImage.membership.forward with hy239  have aL := included with a, ha240  exact functionImage.membership.backward with ⟨yIn, a, aL, ya⟩241242theorem GroupHom.surjective_iff_range243  shows SurjectiveBetween(f, G.carrier, H.carrier) ↔244    functionImage(f, G.carrier, H.carrier) = H.carrier245proof246  have function := GroupHom.function with hom247  have bounded := functionImage.subset at f, G.carrier, H.carrier248  constructor249  . intro surjective250    apply Subset.antisymmetric with bounded251    intros y hy252    obtain ⟨x, hx, edge⟩ := surjective.right with y, hy253    have value := FunctionBetween.apply_value with function, hx, edge254    apply functionImage.membership.backward255    refine ⟨hy, x, hx, ?_⟩256    symm257    exact value258  . intro equal259    constructor260    . exact function261    . intros y hy262      rw ← equal at hy263      obtain ⟨yIn, x, hx, yx⟩ := functionImage.membership.forward with hy264      have edge := FunctionBetween.relates_apply with function, hx265      refine ⟨x, hx, ?_⟩266      rwa yx267268theorem GroupHom.corestrict_surjective269  shows SurjectiveBetween(f, G.carrier, functionImage(f, G.carrier, H.carrier))270proof271  have function := GroupHom.function with hom272  exact functionImage.surjective with function273274theorem GroupHom.kernel_comp_subset (g K : Set)275  requires second : g : H →* K276  shows ker(f) ⊆ kernel(compose(g, f, G.carrier, H.carrier, K.carrier), G, K)277proof278  have fFunction := GroupHom.function with hom279  have gFunction := GroupHom.function with second280  have unitValue := GroupHom.map_one with second281  intros x hx282  obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx283  have composed := compose.apply at g, f, G.carrier, H.carrier, K.carrier, x with *284  have vanishes : compose(g, f, G.carrier, H.carrier, K.carrier)(x) = K.one by cc285  exact kernel.of_value with xIn, vanishes286287end KernelLaws288