Points of a formal group law in the maximal ideal

In the standing setting of the p-adic kit and for finite ι, the tuples ChabautyColeman.FormalGroupLaw.Points with entries in the maximal ideal form a commutative monoid under evaluation of F (addition is total on 𝔪-tuples since the values of series with vanishing constant term stay in 𝔪); each monoid axiom is the corresponding formal axiom of F, evaluated via ChabautyColeman.MvPSeries.eval_subst. Inverses are not constructed here.

Main definitions

• ChabautyColeman.FormalGroupLaw.Points: the 𝔪-tuples, with their AddCommMonoid structure.

Blueprint node: def:fgl.

def ChabautyColeman.FormalGroupLaw.Points {O : Type u_1} [CommRing O] {ι : Type u_2} [IsLocalRing O] (Φ : FormalGroupLaw O ι) : Type (max u_1 u_2)

The 𝔪-points of a formal group law: tuples with entries in the maximal ideal. The group law is evaluation of F. The carrier family is applied explicitly to Φ because the law is a phantom parameter selecting that addition, while its coefficients do not change the underlying tuple type.

Equations

• Φ.Points = (fun (_formalGroupLaw : ChabautyColeman.FormalGroupLaw O ι) => ι → ↥(IsLocalRing.maximalIdeal O)) Φ

@[instance_reducible]

instance ChabautyColeman.FormalGroupLaw.instZeroPoints {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [IsLocalRing O] : Zero Φ.Points

Equations

• Φ.instZeroPoints = { zero := fun (x : ι) => 0 }

@[simp]

theorem ChabautyColeman.FormalGroupLaw.zero_apply_coe {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [IsLocalRing O] (i : ι) : ↑(0 i) = 0

def ChabautyColeman.FormalGroupLaw.pairFam {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [IsLocalRing O] (z w : Φ.Points) : ι ⊕ ι → O

The evaluation-point family attached to a pair of points: the first block of variables gets z, the second w.

Equations

• Φ.pairFam z w = Sum.elim (fun (j : ι) => ↑(z j)) fun (j : ι) => ↑(w j)

theorem ChabautyColeman.FormalGroupLaw.pairFam_mem {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [IsLocalRing O] (z w : Φ.Points) (s : ι ⊕ ι) : Φ.pairFam z w s ∈ IsLocalRing.maximalIdeal O

theorem ChabautyColeman.FormalGroupLaw.hasEval_coe {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [Finite ι] (z : Φ.Points) : MvPowerSeries.HasEval fun (j : ι) => ↑(z j)

theorem ChabautyColeman.FormalGroupLaw.hasEval_pairFam {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [Finite ι] (z w : Φ.Points) : MvPowerSeries.HasEval (Φ.pairFam z w)

@[instance_reducible]

noncomputable instance ChabautyColeman.FormalGroupLaw.instAddPoints {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [Finite ι] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] : Add Φ.Points

Equations

• Φ.instAddPoints = { add := fun (z w : Φ.Points) (i : ι) => ⟨ChabautyColeman.MvPSeries.eval (Φ.pairFam z w) (Φ.F i), ⋯⟩ }

@[simp]

theorem ChabautyColeman.FormalGroupLaw.add_apply_coe {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [Finite ι] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] (z w : Φ.Points) (i : ι) : ↑((z + w) i) = MvPSeries.eval (Φ.pairFam z w) (Φ.F i)

@[instance_reducible]

noncomputable instance ChabautyColeman.FormalGroupLaw.instAddCommMonoidPoints {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [Finite ι] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] : AddCommMonoid Φ.Points

Equations

• One or more equations did not get rendered due to their size.