CoactionBaseNaturality.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Coassociativity on the image of an equivariant base algebra

An arbitrary polynomial family extending a genuine additive action on a base algebra already satisfies the action law on that base image. This lemma is used before the determinant-frame uniqueness argument: it supplies equality of the three base products of the two candidate composite frames.

theorem OAI.StableCoordinate.CoactionLND.universal_translate_map line 24

Source documentation

Universal Taylor translation commutes with change of coefficient ring.

theorem universal_translate_map (p : B[X]) (i : B →+* A) :
    (taylor (X : B[X]) (p.map (C : B →+* B[X]))).map (mapRingHom i) =
      taylor (X : A[X]) ((p.map i).map (C : A →+* A[X])) := by
…

theorem OAI.StableCoordinate.CoactionLND.coassoc_on_image_of_extension line 40
Source documentation
Coassociativity transfers to the image of the base under any polynomial family extending an actual base action. No group law or normalization for β is assumed.
```
theorem coassoc_on_image_of_extension
    (α : PolynomialAdditiveAction k B) (β : A →ₐ[k] A[X]) (i : B →ₐ[k] A)
    (hβ : ∀ b, β (i b) = (α.toAlgHom b).map i.toRingHom) (b : B) :
    (β (i b)).map β.toRingHom =
      taylor (X : A[X]) ((β (i b)).map (C : A →+* A[X])) := by
…
```
Mentions: OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction