Module

SubgroupRestrictionOfImage.lean

Nyll.EtaleFundamentalGroups.Inertia.SubgroupRestrictionOfImage

3 declarations indexed from sourceView source ↗

Module documentation

Induced subgroup restriction from a proved image equality

The map is the literal ambient homomorphism on subgroup elements. A proved image equality supplies membership and every target element's actual lift.

Imports1

Mathlib.Algebra.Group.Subgroup.Map

Imported by2

def

subgroupRestrictionOfImage

L21 ↗

EtaleFundamentalGroups.Inertia.subgroupRestrictionOfImage

Documentation

The literal restriction to subgroups whose image equality is proved.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

def subgroupRestrictionOfImage
    {G : Type u} {H : Type v} [Group G] [Group H]
    (f : G →* H) (P : Subgroup G) (Q : Subgroup H) (h : P.map f = Q) : P →* Q

theorem

subgroupRestrictionOfImage_val

L27 ↗

EtaleFundamentalGroups.Inertia.subgroupRestrictionOfImage_val

Documentation

The induced homomorphism is the same ambient homomorphism on values.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem subgroupRestrictionOfImage_val
    {G : Type u} {H : Type v} [Group G] [Group H]
    (f : G →* H) (P : Subgroup G) (Q : Subgroup H) (h : P.map f = Q) (x : P) :
    ((subgroupRestrictionOfImage f P Q h).toFun x).val = f.toFun x.val

theorem

subgroupRestrictionOfImage_surjective

L34 ↗

EtaleFundamentalGroups.Inertia.subgroupRestrictionOfImage_surjective

Documentation

The proved image equality supplies surjectivity of this same restriction.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem subgroupRestrictionOfImage_surjective
    {G : Type u} {H : Type v} [Group G] [Group H]
    (f : G →* H) (P : Subgroup G) (Q : Subgroup H) (h : P.map f = Q) :
    Function.Surjective (subgroupRestrictionOfImage f P Q h).toFun

Module documentation

Induced subgroup restriction from a proved image equality

Declarations

subgroupRestrictionOfImage

subgroupRestrictionOfImage_val

subgroupRestrictionOfImage_surjective