NYLL
Module

FiniteQuotientRangeTransport.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteQuotientRangeTransport
2 declarations indexed from sourceView source ↗

Module documentation

Transport and triviality of finite quotient ranges

These group-theoretic lemmas transport the range of a finite quotient through successive homomorphisms without unfolding the quotient construction.

Imports1
Imported by1

Declarations

theorem

range_map_map_eq_of_comp_eq

L23 ↗
EtaleFundamentalGroups.Inertia.range_map_map_eq_of_comp_eq
Documentation

If a composite quotient is identified with a canonical homomorphism, then any subsequent range identification transports back to the original quotient range.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe uG uH uK uM
Lean source · statement
theorem range_map_map_eq_of_comp_eq
    {G : Type uG} {H : Type uH} {K : Type uK} {M : Type uM}
    [Group G] [Group H] [Group K] [Group M]
    (q : G →* H) (f : H →* K) (c : K →* M)
    (u : G →* K) (I : Subgroup M)
    (hcomp : f.comp q = u) (hrange : u.range.map c = I) :
    (q.range.map f).map c = I
theorem

subgroup_eq_bot_of_range_map_map_eq_of_coprime_every_prime

L38 ↗
EtaleFundamentalGroups.Inertia.subgroup_eq_bot_of_range_map_map_eq_of_coprime_every_prime
Documentation

If a finite quotient range has cardinality prime to every rational prime, then every subgroup obtained from it by successive range maps is trivial.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe uG uH uK uM
Lean source · statement
theorem subgroup_eq_bot_of_range_map_map_eq_of_coprime_every_prime
    {G : Type uG} {H : Type uH} {K : Type uK} {M : Type uM}
    [Group G] [Group H] [Group K] [Group M]
    (q : G →* H) (f : H →* K) (c : K →* M)
    (I : Subgroup M) [Finite q.range]
    (hrange : (q.range.map f).map c = I)
    (hCoprime : ∀ p : ℕ, p.Prime → Nat.Coprime (Nat.card q.range) p) :
    I = ⊥

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.