Module

CyclicProjection.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.GroupTheory.CyclicProjection

3 declarations indexed from sourceView source ↗

Module documentation

The cyclic group argument in Abhyankar's lemma

This file isolates the finite-group calculation in the proof of SGA 1, Expose X, Lemma 3.6. A cyclic group embedded in a product of two cyclic groups has order dividing the order of the second factor when the order of the first factor already divides it. Consequently, a surjective projection to the second factor is an isomorphism.

Imports1

Mathlib.GroupTheory.SpecificGroups.Cyclic

Imported by2

theorem

cyclic_right_projection_injective_of_card_dvd

L32 ↗

TameAbhyankar.SGA1.cyclic_right_projection_injective_of_card_dvd

Documentation

The group-theoretic order argument in the proof of tame Abhyankar.

If M embeds in G x H, its projection to H is surjective, and |G| divides |H|, then the projection M -> H is injective.

Source context 6 commands

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

noncomputable section
namespace TameAbhyankar.SGA1
variable {M G H : Type*}
variable [Group M] [Group G] [Group H]
variable [Finite M] [Finite H]
variable [IsCyclic M] [IsCyclic G]

Lean source · statement

theorem cyclic_right_projection_injective_of_card_dvd
    (toLeft : M →* G) (toRight : M →* H)
    (hpair : Function.Injective (toLeft.prod toRight))
    (hright : Function.Surjective toRight)
    (hcard : Nat.card G ∣ Nat.card H) :
    Function.Injective toRight

theorem

cyclic_right_projection_bijective_of_card_dvd

L67 ↗

TameAbhyankar.SGA1.cyclic_right_projection_bijective_of_card_dvd

Documentation

Under the hypotheses of the cyclic Abhyankar argument, the right projection is an isomorphism on the underlying finite groups.

Source context 6 commands

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

noncomputable section
namespace TameAbhyankar.SGA1
variable {M G H : Type*}
variable [Group M] [Group G] [Group H]
variable [Finite M] [Finite H]
variable [IsCyclic M] [IsCyclic G]

Lean source · statement

theorem cyclic_right_projection_bijective_of_card_dvd
    (toLeft : M →* G) (toRight : M →* H)
    (hpair : Function.Injective (toLeft.prod toRight))
    (hright : Function.Surjective toRight)
    (hcard : Nat.card G ∣ Nat.card H) :
    Function.Bijective toRight

theorem

cyclic_right_projection_ker_eq_bot_of_card_dvd

L79 ↗

TameAbhyankar.SGA1.cyclic_right_projection_ker_eq_bot_of_card_dvd

Documentation

Equivalently, the relative group occurring as the kernel of the right projection is trivial.

Source context 6 commands

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

noncomputable section
namespace TameAbhyankar.SGA1
variable {M G H : Type*}
variable [Group M] [Group G] [Group H]
variable [Finite M] [Finite H]
variable [IsCyclic M] [IsCyclic G]

Lean source · statement

theorem cyclic_right_projection_ker_eq_bot_of_card_dvd
    (toLeft : M →* G) (toRight : M →* H)
    (hpair : Function.Injective (toLeft.prod toRight))
    (hright : Function.Surjective toRight)
    (hcard : Nat.card G ∣ Nat.card H) :
    MonoidHom.ker toRight = ⊥

Module documentation

The cyclic group argument in Abhyankar's lemma

Declarations

cyclic_right_projection_injective_of_card_dvd

cyclic_right_projection_bijective_of_card_dvd

cyclic_right_projection_ker_eq_bot_of_card_dvd