FrameQuotientMap.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Actual determinant-quotient maps from frames

A determinant frame in a commutative k-algebra, together with an image of u, gives an actual algebra homomorphism from the exact source ring k[a,d,b,c,u]/(ac-bd-1). This is the quotient-map construction needed when a normalized polynomial frame is turned into a lifted additive action.

def OAI.StableCoordinate.FrameLift.Frame.polynomialMap line 26
Source documentation
Evaluation on the five independent determinant-presentation variables.
```
def Frame.polynomialMap (F : Frame S) (u : S) : Obstruction.P k 5 →ₐ[k] S :=
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.Obstruction.P
theorem OAI.StableCoordinate.FrameLift.Frame.polynomialMap_relation line 30
Source documentation
Every determinant frame satisfies the exact source relation.
```
theorem Frame.polynomialMap_relation (F : Frame S) (u : S) :
    F.polynomialMap (k := k) u (Obstruction.determinantRelation k) = 0 := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.Obstruction.determinantRelation
theorem OAI.StableCoordinate.FrameLift.Frame.ideal_le_ker_polynomialMap line 36
Source documentation
The determinant relation generates an ideal in the kernel of evaluation.
```
theorem Frame.ideal_le_ker_polynomialMap (F : Frame S) (u : S) :
    Obstruction.idealC k ≤ RingHom.ker (F.polynomialMap (k := k) u).toRingHom := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.Obstruction.idealC
def OAI.StableCoordinate.FrameLift.Frame.quotientMap line 43
Source documentation
The actual map out of the source determinant quotient induced by a frame. The image of the fifth coordinate u is arbitrary and independently specified.
```
def Frame.quotientMap (F : Frame S) (u : S) : Obstruction.C k →ₐ[k] S :=
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.FrameLift.Frame.quotientMap_cX line 47
theorem OAI.StableCoordinate.FrameLift.Frame.quotientMap_a line 52
theorem OAI.StableCoordinate.FrameLift.Frame.quotientMap_d line 55
theorem OAI.StableCoordinate.FrameLift.Frame.quotientMap_b line 58
theorem OAI.StableCoordinate.FrameLift.Frame.quotientMap_c line 61
theorem OAI.StableCoordinate.FrameLift.Frame.quotientMap_u line 64
theorem OAI.StableCoordinate.FrameLift.determinant_algHom_ext line 69
Source documentation
Maps from the concrete determinant quotient are determined by all five coordinate images.
```
theorem determinant_algHom_ext {φ ψ : Obstruction.C k →ₐ[k] S}
    (h : ∀ i : Fin 5, φ (Obstruction.cX k i) = ψ (Obstruction.cX k i)) : φ = ψ := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.cX
def OAI.StableCoordinate.FrameLift.sourceFrame line 76
Source documentation
The canonical determinant frame in the exact quotient.
```
def sourceFrame (k : Type*) [CommRing k] : Frame (Obstruction.C k) where
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.Obstruction.C
def OAI.StableCoordinate.FrameLift.frameOfHom line 84
Source documentation
Each algebra map gives its frame of coordinate images.
```
def frameOfHom (φ : Obstruction.C k →ₐ[k] S) : Frame S :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.FrameLift.Frame
theorem OAI.StableCoordinate.FrameLift.frameOfHom_a line 87
theorem OAI.StableCoordinate.FrameLift.frameOfHom_d line 89
theorem OAI.StableCoordinate.FrameLift.frameOfHom_b line 91
theorem OAI.StableCoordinate.FrameLift.frameOfHom_c line 93
theorem OAI.StableCoordinate.FrameLift.quotientMap_sourceFrame line 96
theorem OAI.StableCoordinate.FrameLift.Frame.quotientMap_natural line 103
Source documentation
Naturality of the quotient-map construction under a target algebra map.
```
theorem Frame.quotientMap_natural (F : Frame S) (u : S) (φ : S →ₐ[k] T) :
    φ.comp (F.quotientMap u) = (F.map φ.toRingHom).quotientMap (φ u) := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.FrameLift.Frame.quotientMap
theorem OAI.StableCoordinate.FrameLift.quotientMap_frameOfHom line 109
theorem OAI.StableCoordinate.FrameLift.determinant_algHom_ext_frame line 117
Source documentation
Equality of the determinant frame and the fifth-coordinate image gives actual equality of quotient algebra homomorphisms.
```
theorem determinant_algHom_ext_frame {φ ψ : Obstruction.C k →ₐ[k] S}
    (hF : frameOfHom φ = frameOfHom ψ)
    (hu : φ (Obstruction.cX k 4) = ψ (Obstruction.cX k 4)) : φ = ψ := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.FrameLift.frameOfHom, OAI.StableCoordinate.Obstruction.cX
theorem OAI.StableCoordinate.FrameLift.quadric_algHom_ext line 123
Source documentation
Algebra maps from the quadric quotient are determined by its four generators.
```
theorem quadric_algHom_ext {φ ψ : Obstruction.B k →ₐ[k] S}
    (h : ∀ i : Fin 4, φ (Obstruction.bX k i) = ψ (Obstruction.bX k i)) : φ = ψ := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.bX
def OAI.StableCoordinate.FrameLift.sourceBaseMap line 130
Source documentation
The existing bundle base map with the canonical source quotient aliases.
```
def sourceBaseMap (k : Type*) [CommRing k] : Obstruction.B k →ₐ[k] Obstruction.C k :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.FrameLift.baseMap_bX line 134
Source documentation
The already-constructed base map, expressed in the canonical source names.
```
@[simp] theorem baseMap_bX (i : Fin 4) :
    sourceBaseMap k (Obstruction.bX k i) =
      ![Obstruction.cX k 0 * Obstruction.cX k 2,
        Obstruction.cX k 1 * Obstruction.cX k 3,
        Obstruction.cX k 1 * Obstruction.cX k 2, Obstruction.cX k 4] i :=
…
```
Mentions: OAI.StableCoordinate.FrameLift.sourceBaseMap, OAI.StableCoordinate.Obstruction.bX, OAI.StableCoordinate.Obstruction.cX
theorem OAI.StableCoordinate.FrameLift.Frame.quotientMap_comp_baseMap line 143
Source documentation
A frame lying over the four images of a base map gives an actual extension of that base map to the determinant quotient.
```
theorem Frame.quotientMap_comp_baseMap (F : Frame S) (u : S)
    (φ : Obstruction.B k →ₐ[k] S)
    (hx : F.a * F.b = φ (Obstruction.bX k 0))
    (hy : F.d * F.c = φ (Obstruction.bX k 1))
    (hz : F.d * F.b = φ (Obstruction.bX k 2))
    (hu : u = φ (Obstruction.bX k 3)) :
    (F.quotientMap u).comp (sourceBaseMap k) = φ := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.bX, OAI.StableCoordinate.FrameLift.sourceBaseMap
theorem OAI.StableCoordinate.FrameLift.comp_baseMap_eq_iff line 160
Source documentation
Restriction to the source base records exactly the three frame products and the independent coordinate u.
```
theorem comp_baseMap_eq_iff {φ ψ : Obstruction.C k →ₐ[k] S} :
    φ.comp (sourceBaseMap k) = ψ.comp (sourceBaseMap k) ↔
      SameBase (frameOfHom φ) (frameOfHom ψ) ∧
      φ (Obstruction.cX k 4) = ψ (Obstruction.cX k 4) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.FrameLift.sourceBaseMap, OAI.StableCoordinate.FrameLift.SameBase, OAI.StableCoordinate.FrameLift.frameOfHom, OAI.StableCoordinate.Obstruction.cX
theorem OAI.StableCoordinate.FrameLift.normalized_quotientMap_unique line 182
Source documentation
Normalized polynomial maps of the determinant quotient are unique over the same base map. This is an actual equality of algebra homomorphisms.
```
theorem normalized_quotientMap_unique {R σ : Type*} [CommRing R] [Algebra k R]
    [IsReduced R] {φ ψ : Obstruction.C k →ₐ[k] MvPolynomial σ R}
    (hbase : φ.comp (sourceBaseMap k) = ψ.comp (sourceBaseMap k))
    (hzero : (frameOfHom φ).map MvPolynomial.constantCoeff =
      (frameOfHom ψ).map MvPolynomial.constantCoeff) : φ = ψ := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.FrameLift.sourceBaseMap, OAI.StableCoordinate.FrameLift.frameOfHom