FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Multiplicative
Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / System / Ring / Multiplicative.
import
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.CoefficientRings
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike
instance instOnePrimePowerCompletedGroupAlgebra : One (PrimePowerCompletedGroupAlgebra ℓ G) where
one := ⟨fun i => (1 : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(1 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 1
exact map_one _⟩The prime-power completed group algebra has a coordinatewise multiplicative identity.
instance instMulPrimePowerCompletedGroupAlgebra : Mul (PrimePowerCompletedGroupAlgebra ℓ G) where
mul x y := ⟨fun i =>
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) *
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by
intro i j hij
calc
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) *
(show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j))
=
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) *
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j) := by
rw [map_mul]
_ =
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) *
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i) := by
exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩Multiplication on the completed group algebra is defined coordinatewise through the finite-stage group-algebra products.
instance instNatCastPrimePowerCompletedGroupAlgebra :
NatCast (PrimePowerCompletedGroupAlgebra ℓ G) where
natCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(n : PrimePowerCompletedGroupAlgebraStage ℓ G j) = n
exact map_natCast _ _⟩Natural number casts in the prime-power completed group algebra are computed coordinatewise.
instance instIntCastPrimePowerCompletedGroupAlgebra :
IntCast (PrimePowerCompletedGroupAlgebra ℓ G) where
intCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(n : PrimePowerCompletedGroupAlgebraStage ℓ G j) = n
exact map_intCast _ _⟩Integer casts in the prime-power completed group algebra are computed coordinatewise.
instance instRingPrimePowerCompletedGroupAlgebraStage
(i : PrimePowerCompletedGroupAlgebraIndex G) :
Ring ((primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
dsimp [primePowerCompletedGroupAlgebraSystem, PrimePowerCompletedGroupAlgebraStage]
infer_instanceThe completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.
instance instRingPrimePowerCompletedGroupAlgebraFamily :
Ring
((i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) :=
inferInstanceThe completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.
instance instPowPrimePowerCompletedGroupAlgebra : Pow (PrimePowerCompletedGroupAlgebra ℓ G) ℕ where
pow x n := ⟨fun i => (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) ^ n, by
intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) ^ n) =
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) ^ n
rw [map_pow]
exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩Powers in the prime-power completed group algebra are computed coordinatewise.
theorem coe_one_primePowerCompletedGroupAlgebra :
((1 : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
(1 :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i)The multiplicative identity in the prime-power completed group algebra is computed coordinatewise.
Show proof
by
funext i
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem coe_mul_primePowerCompletedGroupAlgebra
(x y : PrimePowerCompletedGroupAlgebra ℓ G) :
((x * y : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
(x * y :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i)Multiplication in the prime-power completed group algebra is computed coordinatewise.
Show proof
by
funext i
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem coe_natCast_primePowerCompletedGroupAlgebra
(n : ℕ) :
((n : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
(n :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i)Natural number casts in the prime-power completed group algebra are computed coordinatewise.
Show proof
by
funext i
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem coe_intCast_primePowerCompletedGroupAlgebra
(n : ℤ) :
((n : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
(n :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i)Integer casts in the prime-power completed group algebra are computed coordinatewise.
Show proof
by
funext i
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem coe_pow_primePowerCompletedGroupAlgebra
(x : PrimePowerCompletedGroupAlgebra ℓ G) (n : ℕ) :
((x ^ n : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
(x ^ n :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i)Powers in the prime-power completed group algebra are computed coordinatewise.
Show proof
by
funext i
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□instance instRingPrimePowerCompletedGroupAlgebra :
Ring (PrimePowerCompletedGroupAlgebra ℓ G) :=
Function.Injective.ring
(fun x : PrimePowerCompletedGroupAlgebra ℓ G =>
(x :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i))
Subtype.val_injective
(coe_zero_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
(coe_one_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
(coe_add_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
(coe_mul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
(coe_neg_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
(coe_sub_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
(fun n x => coe_nsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) n x)
(fun n x => coe_zsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) n x)
(fun x n => coe_pow_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) x n)
(by
intro n
exact coe_natCast_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) n)
(by
intro z
exact coe_intCast_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) z)The completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.