Module

Complement.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.Complement

1 declaration indexed from sourceView source ↗

Module documentation

Units on the complement of a boundary product

If the equation of a boundary is a finite product of component parameters, then every parameter occurring in that product becomes a unit on the boundary complement. This is the elementary algebraic input used by the explicit Kummer charts.

Imports1

Mathlib.RingTheory.Localization.Away.Basic

Imported by2

theorem

isUnit_algebraMap_of_mem_away_finsetProduct

L24 ↗

EtaleFundamentalGroups.isUnit_algebraMap_of_mem_away_finsetProduct

Documentation

Every factor of a boundary product becomes a unit after the product is inverted.

Source context 2 commands

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

namespace EtaleFundamentalGroups
universe u v w

Lean source · statement

theorem isUnit_algebraMap_of_mem_away_finsetProduct
    {R : Type u} {S : Type v} {ι : Type w}
    [CommRing R] [CommRing S] [Algebra R S]
    (s : Finset ι) (t : ι → R)
    [IsLocalization.Away (∏ i ∈ s, t i) S]
    {i : ι} (hi : i ∈ s) :
    IsUnit (algebraMap R S (t i))

Module documentation

Units on the complement of a boundary product

Declarations

isUnit_algebraMap_of_mem_away_finsetProduct