Module

MultiAwayUnitDescent.lean

Nyll.EtaleFundamentalGroups.Kummer.Descent.MultiAwayUnitDescent

3 declarations indexed from sourceView source ↗

Module documentation

Unit descent from a multi-boundary complement

This file extends unit descent from one prime boundary parameter to a finite product of prime parameters. A divisor of a power of the boundary product which is divisible by none of its prime factors must be a unit.

Imports1

Nyll.EtaleFundamentalGroups.Kummer.Descent.Unit

Imported by6

theorem

dvd_left_of_dvd_mul_finsetProduct_of_primes_of_not_dvd

L25 ↗

EtaleFundamentalGroups.Kummer.dvd_left_of_dvd_mul_finsetProduct_of_primes_of_not_dvd

Documentation

Strip a finite product of prime factors from the right side of a divisibility relation when none of those factors divides the left side.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open scoped BigOperators
universe u v w

Lean source · statement

theorem dvd_left_of_dvd_mul_finsetProduct_of_primes_of_not_dvd
    {R : Type u} [CommRing R] [IsDomain R]
    {ι : Type w} (s : Finset ι) (t : ι → R) {a b : R}
    (ht : ∀ i ∈ s, Prime (t i))
    (hta : ∀ i ∈ s, ¬ t i ∣ a)
    (h : a ∣ b * ∏ i ∈ s, t i) :
    a ∣ b

theorem

isUnit_of_isUnit_algebraMap_away_finsetProduct_of_primes_of_not_dvd

L54 ↗

EtaleFundamentalGroups.Kummer.isUnit_of_isUnit_algebraMap_away_finsetProduct_of_primes_of_not_dvd

Documentation

Let S be obtained by inverting a finite product of prime elements. An element divisible by none of those primes was already a unit if its image is a unit in S.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open scoped BigOperators
universe u v w

Lean source · statement

theorem isUnit_of_isUnit_algebraMap_away_finsetProduct_of_primes_of_not_dvd
    {R : Type u} {S : Type v} {ι : Type w}
    [CommRing R] [IsDomain R] [CommRing S] [Algebra R S]
    (s : Finset ι) (t : ι → R)
    [IsLocalization.Away (∏ i ∈ s, t i) S]
    {a : R} (ht : ∀ i ∈ s, Prime (t i))
    (hta : ∀ i ∈ s, ¬ t i ∣ a)
    (ha : IsUnit (algebraMap R S a)) :
    IsUnit a

theorem

isUnit_natCast_of_isUnit_algebraMap_away_finsetProduct

L80 ↗

EtaleFundamentalGroups.Kummer.isUnit_natCast_of_isUnit_algebraMap_away_finsetProduct

Documentation

For a positive natural number, characteristic zero on every boundary component supplies all nondivisibility inputs needed by multi-boundary unit descent.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open scoped BigOperators
universe u v w

Lean source · statement

theorem isUnit_natCast_of_isUnit_algebraMap_away_finsetProduct
    {R : Type u} {S : Type v} {ι : Type w}
    [CommRing R] [IsDomain R] [CommRing S] [Algebra R S]
    (s : Finset ι) (t : ι → R)
    [IsLocalization.Away (∏ i ∈ s, t i) S]
    (ht : ∀ i ∈ s, Prime (t i))
    (hCharZero : ∀ i ∈ s, CharZero (R ⧸ Ideal.span {t i}))
    {n : ℕ} (hn : 0 < n)
    (hnS : IsUnit (algebraMap R S (n : R))) :
    IsUnit (n : R)

Module documentation

Unit descent from a multi-boundary complement

Declarations

dvd_left_of_dvd_mul_finsetProduct_of_primes_of_not_dvd

isUnit_of_isUnit_algebraMap_away_finsetProduct_of_primes_of_not_dvd

isUnit_natCast_of_isUnit_algebraMap_away_finsetProduct