FrameCoassociativity.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Coassociativity of normalized determinant-frame lifts

A polynomial algebra map with the identity specialization has the additive group law on all four frame entries as soon as it has that law on the three quadric products. This is proved as an equality of two-parameter polynomial frames, not by evaluating at field-valued parameters.

def OAI.StableCoordinate.FrameLift.iterateHom line 25
Source documentation
The iterated polynomial substitution in an additive coaction.
```
def iterateHom (β : R →+* R[X]) : R →+* R[X][X] :=
…
```
Mentions: OAI.StableCoordinate.R
def OAI.StableCoordinate.FrameLift.addParameterHom line 29
Source documentation
Substitute the sum of the two independent action parameters.
```
def addParameterHom (β : R →+* R[X]) : R →+* R[X][X] :=
…
```
Mentions: OAI.StableCoordinate.R
def OAI.StableCoordinate.FrameLift.CoassociativeAt line 34
Source documentation
Coassociativity at one particular ring element.
```
def CoassociativeAt (β : R →+* R[X]) (r : R) : Prop :=
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.FrameLift.iterateHom_apply line 38
theorem OAI.StableCoordinate.FrameLift.addParameterHom_apply line 42
theorem OAI.StableCoordinate.FrameLift.outer_constantCoeff_agrees line 46
Source documentation
The two-parameter substitutions agree at outer parameter zero.
```
theorem outer_constantCoeff_agrees (β : R →+* R[X])
    (hβ : ∀ r, (β r).coeff 0 = r) (r : R) :
    Polynomial.constantCoeff (iterateHom β r) =
      Polynomial.constantCoeff (addParameterHom β r) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.iterateHom, OAI.StableCoordinate.FrameLift.addParameterHom
theorem OAI.StableCoordinate.FrameLift.coassociative_frame line 57
Source documentation
Group law on the base coordinates gives equality of the two iterated frames by normalized polynomial-frame uniqueness.
```
theorem coassociative_frame [IsReduced R]
    (β : R →+* R[X]) (hβ : ∀ r, (β r).coeff 0 = r)
    (F : Frame R)
    (hbase : CoassociativeAt β (F.a*F.b) ∧
      CoassociativeAt β (F.d*F.c) ∧ CoassociativeAt β (F.d*F.b)) :
    F.map (iterateHom β) = F.map (addParameterHom β) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.FrameLift.CoassociativeAt, OAI.StableCoordinate.FrameLift.iterateHom, OAI.StableCoordinate.FrameLift.addParameterHom

theorem OAI.StableCoordinate.FrameLift.coassociative_on_frame_entries line 79

Source documentation

Coassociativity therefore holds on each of the four frame entries.

theorem coassociative_on_frame_entries [IsReduced R]
    (β : R →+* R[X]) (hβ : ∀ r, (β r).coeff 0 = r)
    (F : Frame R)
    (hbase : CoassociativeAt β (F.a*F.b) ∧
      CoassociativeAt β (F.d*F.c) ∧ CoassociativeAt β (F.d*F.b)) :
    CoassociativeAt β F.a ∧ CoassociativeAt β F.d ∧
      CoassociativeAt β F.b ∧ CoassociativeAt β F.c := by
…

Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.FrameLift.CoassociativeAt