InfinitesimalCharts.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Infinitesimal neighbourhoods in formally étale charts

Formal smoothness and formal unramifiedness give compatible isomorphisms on the quotients by powers of an ideal whenever the residue map is an isomorphism.

theorem OAI.CartierSections.scalarTower_self line 21
Source documentation
The multiplication action of a commutative ring on itself forms a scalar tower.
```
theorem scalarTower_self {R : Type*} [CommRing R] : IsScalarTower R R R :=
…
```
theorem OAI.CartierSections.quotient_reduction_nilpotent line 31
Source documentation
The image of an ideal modulo a power of itself is nilpotent.
```
theorem quotient_reduction_nilpotent (I : Ideal S) (n : ℕ) :
    IsNilpotent (I.map (Ideal.Quotient.mkₐ R (I^n))) := by
…
```

theorem OAI.CartierSections.formally_smooth_lift_to_power line 39

Source documentation

Formal smoothness lifts a residue map to every finite infinitesimal neighbourhood.

theorem formally_smooth_lift_to_power [Algebra.FormallySmooth R A]
    (I : Ideal S) {n : ℕ} (hn : 0 < n) (f : A →ₐ[R] S ⧸ I) :
    ∃ g : A →ₐ[R] S ⧸ I^n,
      (Ideal.Quotient.factorₐ R (Ideal.pow_le_self hn.ne')).comp g = f := by
…

theorem OAI.CartierSections.formally_unramified_unique_to_power line 53

Source documentation

Formal unramifiedness gives uniqueness of lifts of a residue map.

theorem formally_unramified_unique_to_power [Algebra.FormallyUnramified R A]
    (I : Ideal S) {n : ℕ} (hn : 0 < n) (f g : A →ₐ[R] S ⧸ I^n)
    (h : (Ideal.Quotient.factorₐ R (Ideal.pow_le_self hn.ne')).comp f =
      (Ideal.Quotient.factorₐ R (Ideal.pow_le_self hn.ne')).comp g) : f = g := by
…

def OAI.CartierSections.quotientPowerMap line 71
Source documentation
The map on each infinitesimal neighbourhood induced by the algebra map.
```
def quotientPowerMap (I : Ideal R) (n : ℕ) :
    R ⧸ I^n →ₐ[R] A ⧸ (I.map (algebraMap R A))^n :=
…
```
theorem OAI.CartierSections.quotientPowerMap_mk line 77
theorem OAI.CartierSections.quotientPowerMap_algebraMap line 81
theorem OAI.CartierSections.quotientPowerMap_factor line 86
def OAI.CartierSections.quotientBaseMap line 94
theorem OAI.CartierSections.etale_quotient_power_bijective line 99
Source documentation
A formally étale map which is an isomorphism modulo I is an isomorphism modulo every power of I.
```
theorem etale_quotient_power_bijective [Algebra.FormallyEtale R A]
    (I : Ideal R) (hI : Function.Bijective (quotientBaseMap (A := A) I)) (n : ℕ) :
…
```
Mentions: OAI.CartierSections.quotientBaseMap