LocalMultiplier.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Local principality and rounded divisor inequalities

Local algebra for uniform Cartier sections.

theorem OAI.CartierSections.LocalMultiplier.exists_unit_quotient_of_span_eq line 24
Source documentation
In a local domain, if finitely many principal ideals sum to a nonzero principal ideal, one generator divided by the latter generator is a unit. This is the local invertible-sum-ideal assertion used on the log resolution.
```
theorem exists_unit_quotient_of_span_eq
    {A ι : Type*} [CommRing A] [IsDomain A] [IsLocalRing A] [Fintype ι]
    (f : ι → A) (g : A) (hg : g ≠ 0)
    (hspan : Ideal.span (Set.range f) = Ideal.span ({g} : Set A)) :
    ∃ i b, IsUnit b ∧ f i = g * b := by
…
```
theorem OAI.CartierSections.LocalMultiplier.rounding_criterion line 55
Source documentation
Literal Laurent-monomial membership in the rounded divisor sheaf becomes a strict linear inequality. The strict inequality retains rounding walls.
```
theorem rounding_criterion (n : ℤ) (K t : ℝ) :
    -n ≤ ⌈K - t⌉ ↔ t < K + n + 1 := by
…
```
def OAI.CartierSections.LocalMultiplier.admittingExponents line 64
Source documentation
Exponents giving a fixed Laurent monomial in a mixed rounded divisor. D i j is the coefficient of the i-th resolved summand along the j-th snc component. K j and n j are the relative-canonical and monomial exponents.
```
def admittingExponents {ι κ : Type*} [Fintype ι]
    (c : ℝ) (D : ι → κ → ℝ) (K : κ → ℝ) (n : κ → ℤ) : Set (ι → ℝ) :=
…
```
theorem OAI.CartierSections.LocalMultiplier.mem_admittingExponents_iff line 69
theorem OAI.CartierSections.LocalMultiplier.admittingExponents_convex line 77
Source documentation
The admitting set is convex, including all simplex faces.
```
theorem admittingExponents_convex {ι κ : Type*} [Fintype ι]
    (c : ℝ) (D : ι → κ → ℝ) (K : κ → ℝ) (n : κ → ℤ) :
    Convex ℝ (admittingExponents c D K n) := by
…
```
Mentions: OAI.CartierSections.LocalMultiplier.admittingExponents
theorem OAI.CartierSections.LocalMultiplier.admittingExponents_nonempty_iff line 104
Source documentation
If the resolved sum divisor is a coefficientwise minimum achieved by one summand, the admitting set is nonempty exactly for the target Laurent monomials. This bridges actual local principality to the rounding-cell calculation.
```
theorem admittingExponents_nonempty_iff {ι κ : Type*} [Fintype ι]
    (c : ℝ) (hc : 0 ≤ c) (D : ι → κ → ℝ) (d K : κ → ℝ) (n : κ → ℤ)
    (hle : ∀ i j, d j ≤ D i j) (i₀ : ι) (heq : ∀ j, D i₀ j = d j) :
    (admittingExponents c D K n).Nonempty ↔
      ∀ j, -n j ≤ ⌈K j - c * d j⌉ := by
…
```
Mentions: OAI.CartierSections.LocalMultiplier.admittingExponents
def OAI.CartierSections.LocalMultiplier.exponentSimplex line 132
Source documentation
The simplex on which the rounding subdivision is made; no face is omitted.
```
def exponentSimplex {ι : Type*} [Fintype ι] (c : ℝ) : Set (ι → ℝ) :=
…
```
theorem OAI.CartierSections.LocalMultiplier.admittingExponents_relativelyOpen line 137
Source documentation
For finitely many snc components, the admitting set is relatively open in the closed exponent simplex, not in its affine ambient space.
```
theorem admittingExponents_relativelyOpen {ι κ : Type*} [Fintype ι] [Finite κ]
    (c : ℝ) (D : ι → κ → ℝ) (K : κ → ℝ) (n : κ → ℤ) :
    IsOpen {p : exponentSimplex (ι := ι) c |
…
```
Mentions: OAI.CartierSections.LocalMultiplier.exponentSimplex

theorem OAI.CartierSections.LocalMultiplier.admittingExponents_contractible line 158

Source documentation

A nonempty coefficientwise admitting region is contractible.

theorem admittingExponents_contractible {ι κ : Type*} [Fintype ι]
    (c : ℝ) (D : ι → κ → ℝ) (K : κ → ℝ) (n : κ → ℤ)
    (hne : (admittingExponents c D K n).Nonempty) :
    ContractibleSpace (admittingExponents c D K n) :=
…

Mentions: OAI.CartierSections.LocalMultiplier.admittingExponents

theorem OAI.CartierSections.LocalMultiplier.exists_eq_top_of_iSup_eq_top line 167
Source documentation
In a local ring even an arbitrarily indexed sum of ideals can be the unit ideal only if one summand is the unit ideal. Here iSup is the literal ideal sum; no finiteness of the real exponent index set is required.
```
theorem exists_eq_top_of_iSup_eq_top {A ι : Type*}
    [CommRing A] [IsLocalRing A] (I : ι → Ideal A)
    (hI : (⨆ i, I i) = ⊤) : ∃ i, I i = ⊤ := by
…
```