Module

GrpCatCompositeKernel.lean

Nyll.EtaleFundamentalGroups.Inertia.GrpCatCompositeKernel

1 declaration indexed from sourceView source ↗

Module documentation

Kernels of three native group morphisms

The categorical composition and its native group dictionaries are closed in this group-only owner before concrete field and normalization data enter.

Imports2

Mathlib.Algebra.Category.Grp.Basic
Mathlib.Algebra.Group.Subgroup.Ker

Imported by2

theorem

grpCat_comp_comp_ker_of_injective

L25 ↗

EtaleFundamentalGroups.Inertia.grpCat_comp_comp_ker_of_injective

Documentation

Pull back a proved middle kernel through the first map, after cancelling an injective final map in the SAME categorical composite.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u

Lean source · statement

theorem grpCat_comp_comp_ker_of_injective
    (G H M N : GrpCat.{u}) (f : G ⟶ H) (g : H ⟶ M) (e : M ⟶ N)
    (he : Function.Injective e.hom'.toFun)
    (P : Subgroup H.carrier) (hP : g.hom'.ker = P) :
    (f ≫ g ≫ e).hom'.ker = P.comap f.hom'

Module documentation

Kernels of three native group morphisms

Declarations

grpCat_comp_comp_ker_of_injective