ObstructionPrincipalization.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Principalization and invariant transport in the exact obstruction rings

The generic polynomial identity proved in BundlePrincipalization is instantiated here in the source's actual rings B and C, through the injective two-chart base map. The final lemmas prove the last step of source Proposition prop:lift: once an actual locally nilpotent extension has been constructed, a nonzero invariant in the source ideal forces it to annihilate v.

def OAI.StableCoordinate.Obstruction.determinantBasepoint line 23
Source documentation
Evaluation at an actual determinant-one matrix supplies a scalar retraction.
```
noncomputable def determinantBasepoint : C k →ₐ[k] k :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.C
instance OAI.StableCoordinate.Obstruction.determinantCharZero line 34
Source documentation
The determinant coordinate ring inherits characteristic zero from its coefficient ring; this is proved using the displayed scalar retraction.
```
instance determinantCharZero [CharZero k] : CharZero (C k) where
…
```
Mentions: OAI.StableCoordinate.Obstruction.C
abbrev OAI.StableCoordinate.Obstruction.baseMap line 40
Source documentation
The source's injective map B → C, with the canonical obstruction-ring API.
```
noncomputable abbrev baseMap : B k →ₐ[k] C k := BundleCharts.baseMap k
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.BundleCharts.baseMap
theorem OAI.StableCoordinate.Obstruction.baseMap_bX line 42
theorem OAI.StableCoordinate.Obstruction.baseMap_injective line 48
Source documentation
Injectivity is proved by two explicit local sections, not assumed.
```
theorem baseMap_injective : Function.Injective (baseMap k) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.baseMap
theorem OAI.StableCoordinate.Obstruction.baseMap_sB line 51
theorem OAI.StableCoordinate.Obstruction.baseMap_f0 line 55
theorem OAI.StableCoordinate.Obstruction.baseMap_g0 line 59
theorem OAI.StableCoordinate.Obstruction.map_I_eq_span_v line 64
Source documentation
Exact source principalization: the extended ideal IC is (v).
```
theorem map_I_eq_span_v :
    Ideal.map (baseMap k).toRingHom (I k) = Ideal.span ({v k} : Set (C k)) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.baseMap, OAI.StableCoordinate.Obstruction.I, OAI.StableCoordinate.Obstruction.v, OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.Obstruction.baseMap_factor_of_mem_I line 74
Source documentation
Every element of the distinguished ideal admits the required factorization in the total ring, with its actual image under the base map.
```
theorem baseMap_factor_of_mem_I {h : B k} (hh : h ∈ I k) :
    ∃ q : C k, baseMap k h = v k * q := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.I, OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.baseMap, OAI.StableCoordinate.Obstruction.v
theorem OAI.StableCoordinate.Obstruction.extension_ne_zero line 88
Source documentation
An actual extension of a nonzero derivation remains nonzero because the source ring embeds in the total ring.
```
theorem extension_ne_zero
    (hD : D ≠ 0) (hExt : ∀ b, D' (baseMap k b) = baseMap k (D b)) : D' ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.baseMap
theorem OAI.StableCoordinate.Obstruction.extension_annihilates_v line 101
Source documentation
The principalized invariant is fixed by any actual locally nilpotent lift. This is the final factorial-closure argument of source prop:lift.
```
theorem extension_annihilates_v
    (hLND : StableCoordinate.IsLocallyNilpotent D')
    (hExt : ∀ b, D' (baseMap k b) = baseMap k (D b))
    {h : B k} (hh : h ∈ I k) (h0 : h ≠ 0) (hFix : D h = 0) : D' (v k) = 0 := by
…
```
Mentions: OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.Obstruction.baseMap, OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.I, OAI.StableCoordinate.Obstruction.v
theorem OAI.StableCoordinate.Obstruction.extension_nonzero_and_annihilates_v line 117
Source documentation
The two conclusions used by rigidity after constructing the lifted action.
```
theorem extension_nonzero_and_annihilates_v
    (hD : D ≠ 0) (hLND : StableCoordinate.IsLocallyNilpotent D')
    (hExt : ∀ b, D' (baseMap k b) = baseMap k (D b))
    (hInv : ∃ h : B k, h ∈ I k ∧ h ≠ 0 ∧ D h = 0) :
    D' ≠ 0 ∧ D' (v k) = 0 := by
…
```
Mentions: OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.Obstruction.baseMap, OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.I, OAI.StableCoordinate.Obstruction.v