Module

MultiAwayPrimeOrUnitDescent.lean

Nyll.EtaleFundamentalGroups.Kummer.Descent.MultiAwayPrimeOrUnitDescent

3 declarations indexed from sourceView source ↗

Module documentation

Unit descent with inactive boundary units

After localizing a strict-normal-crossings chart at a prime, every boundary parameter is either still prime or has become a unit. This file extends the multi-away unit descent theorem to precisely that situation, without reindexing the surviving boundary components.

Imports1

Nyll.EtaleFundamentalGroups.Kummer.Descent.MultiAwayUnitDescent

Imported by2

theorem

dvd_left_of_dvd_mul_finsetProduct_of_prime_or_unit

L27 ↗

EtaleFundamentalGroups.Kummer.dvd_left_of_dvd_mul_finsetProduct_of_prime_or_unit

Documentation

Remove a finite family of prime-or-unit factors from the right side of a divisibility relation. Nondivisibility is required only for the prime factors; unit factors cancel directly.

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_prime_or_unit
    {R : Type u} [CommRing R] [IsDomain R]
    {ι : Type w} (s : Finset ι) (t : ι → R) {a b : R}
    (ht : ∀ i ∈ s, Prime (t i) ∨ IsUnit (t i))
    (hta : ∀ i ∈ s, Prime (t i) → ¬ t i ∣ a)
    (h : a ∣ b * ∏ i ∈ s, t i) :
    a ∣ b

theorem

isUnit_of_isUnit_algebraMap_away_finsetProduct_of_prime_or_unit

L59 ↗

EtaleFundamentalGroups.Kummer.isUnit_of_isUnit_algebraMap_away_finsetProduct_of_prime_or_unit

Documentation

Let S be obtained by inverting a product whose factors are each prime or a unit. If a is divisible by none of the prime factors and becomes a unit in S, then it was already a unit.

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_prime_or_unit
    {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) ∨ IsUnit (t i))
    (hta : ∀ i ∈ s, Prime (t i) → ¬ t i ∣ a)
    (ha : IsUnit (algebraMap R S a)) :
    IsUnit a

theorem

isUnit_natCast_of_isUnit_algebraMap_away_finsetProduct_of_prime_or_unit

L86 ↗

EtaleFundamentalGroups.Kummer.isUnit_natCast_of_isUnit_algebraMap_away_finsetProduct_of_prime_or_unit

Documentation

Characteristic zero along every surviving prime component supplies the nondivisibility needed to descend a positive natural-number unit. Boundary components which became units after localization require no residue characteristic hypothesis.

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_of_prime_or_unit
    {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) ∨ IsUnit (t i))
    (hCharZero : ∀ i ∈ s, Prime (t i) →
      CharZero (R ⧸ Ideal.span {t i}))
    {n : ℕ} (hn : 0 < n)
    (hnS : IsUnit (algebraMap R S (n : R))) :
    IsUnit (n : R)

Module documentation

Unit descent with inactive boundary units

Declarations

dvd_left_of_dvd_mul_finsetProduct_of_prime_or_unit

isUnit_of_isUnit_algebraMap_away_finsetProduct_of_prime_or_unit

isUnit_natCast_of_isUnit_algebraMap_away_finsetProduct_of_prime_or_unit