FrameLiftCoassoc.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The action law for a normalized lift to the determinant algebra

The polynomial family constructed from a normalized determinant frame is not assumed to be an action. This file proves its additive group law from that of the base family, using the uniqueness of normalized frames.

def OAI.StableCoordinate.FrameLiftCoassoc.iterateMap line 26
Source documentation
Applying the lifted family twice, with two independent parameters.
```
def iterateMap (β : A →ₐ[k] A[X]) : A →ₐ[k] A[X][X] :=
…
```
def OAI.StableCoordinate.FrameLiftCoassoc.sumParameterMap line 30
Source documentation
Applying the lifted family at the sum of two independent parameters.
```
def sumParameterMap (β : A →ₐ[k] A[X]) : A →ₐ[k] A[X][X] :=
…
```
theorem OAI.StableCoordinate.FrameLiftCoassoc.iterateMap_apply line 34
theorem OAI.StableCoordinate.FrameLiftCoassoc.sumParameterMap_apply line 37

theorem OAI.StableCoordinate.FrameLiftCoassoc.coassoc_of_generators line 43

Source documentation

Equality of the two action-law maps can be tested on the five actual quotient generators, and not merely on their values at complex points.

theorem coassoc_of_generators
    (β : Obstruction.C k →ₐ[k] (Obstruction.C k)[X])
    (h : ∀ i : Fin 5,
      (β (Obstruction.cX k i)).map β.toRingHom =
        taylor (X : (Obstruction.C k)[X])
          ((β (Obstruction.cX k i)).map (C : Obstruction.C k →+* (Obstruction.C k)[X]))) :
    ∀ r, (β r).map β.toRingHom =
      taylor (X : (Obstruction.C k)[X]) ((β r).map (C : Obstruction.C k →+* (Obstruction.C k)[X])) := by
…

Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.cX

theorem OAI.StableCoordinate.FrameLiftCoassoc.coassoc_of_normalized_extension line 62

Source documentation

A normalized family on the actual determinant quotient extending a base additive action automatically satisfies the complete bivariate action law.

theorem coassoc_of_normalized_extension
    [IsReduced (Obstruction.C k)]
    (α : PolynomialAdditiveAction k (Obstruction.B k))
    (β : Obstruction.C k →ₐ[k] (Obstruction.C k)[X])
    (hidentity : ∀ r, (β r).coeff 0 = r)
    (hbase : ∀ b, β (BundleCharts.baseMap k b) =
      (α.toAlgHom b).map (BundleCharts.baseMap k).toRingHom) :
    ∀ r, (β r).map β.toRingHom =
      taylor (X : (Obstruction.C k)[X])
        ((β r).map (C : Obstruction.C k →+* (Obstruction.C k)[X])) := by
…

Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.BundleCharts.baseMap

def OAI.StableCoordinate.FrameLiftCoassoc.actionOfNormalizedExtension line 116
Source documentation
Construct the genuine additive action from a normalized extending family. The family is supplied by the separately proved determinant-frame construction; its group law is proved here, not taken as an assumption.
```
def actionOfNormalizedExtension
    [IsReduced (Obstruction.C k)]
    (α : PolynomialAdditiveAction k (Obstruction.B k))
    (β : Obstruction.C k →ₐ[k] (Obstruction.C k)[X])
    (hidentity : ∀ r, (β r).coeff 0 = r)
    (hbase : ∀ b, β (BundleCharts.baseMap k b) =
      (α.toAlgHom b).map (BundleCharts.baseMap k).toRingHom) :
    PolynomialAdditiveAction k (Obstruction.C k) where
…
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.BundleCharts.baseMap
theorem OAI.StableCoordinate.FrameLiftCoassoc.actionOfNormalizedExtension_toAlgHom line 128