FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Additive
Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Additive.
instance instZeroPrimePowerCompletedGroupAlgebraAugmentationIdeal :
Zero (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
zero := ⟨fun i =>
(0 : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i), by
intro i j hij
apply Subtype.ext
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(0 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 0
exact map_zero _⟩The zero element of the prime-power completed augmentation ideal is the compatible family of zero elements at all finite stages.
instance instAddPrimePowerCompletedGroupAlgebraAugmentationIdeal :
Add (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
add x y := ⟨fun i =>
(show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from x.1 i) +
(show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from y.1 i), by
intro i j hij
apply Subtype.ext
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j) +
((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
from y.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j)) =
(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from y.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
rw [map_add]
exact congrArg₂ HAdd.hAdd
(congrArg Subtype.val (x.2 i j hij))
(congrArg Subtype.val (y.2 i j hij))⟩Addition in the prime-power completed augmentation ideal is defined coordinatewise through finite stages.
instance instAddZeroClassPrimePowerCompletedGroupAlgebraAugmentationIdeal :
AddZeroClass (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
zero := 0
add := (· + ·)
zero_add x := by
apply Subtype.ext
funext i
apply Subtype.ext
change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
PrimePowerCompletedGroupAlgebraStage ℓ G i) =
((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
PrimePowerCompletedGroupAlgebraStage ℓ G i)
simp only [zero_add]
add_zero x := by
apply Subtype.ext
funext i
apply Subtype.ext
change ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal
(ℓ := ℓ) (G := G) i from x.1 i) :
PrimePowerCompletedGroupAlgebraStage ℓ G i) +
(0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) =
((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
PrimePowerCompletedGroupAlgebraStage ℓ G i)
simp only [add_zero]Addition in the prime-power completed augmentation ideal is defined coordinatewise through finite stages.
instance instNegPrimePowerCompletedGroupAlgebraAugmentationIdeal :
Neg (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
neg x := ⟨fun i =>
-(show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from x.1 i), by
intro i j hij
apply Subtype.ext
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(-(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
-(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
rw [map_neg]
exact congrArg Neg.neg (congrArg Subtype.val (x.2 i j hij))⟩Negation on the prime-power completed augmentation ideal is defined coordinatewise through finite-stage negations.
instance instSubPrimePowerCompletedGroupAlgebraAugmentationIdeal :
Sub (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
sub x y := ⟨fun i =>
(show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from x.1 i) -
(show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from y.1 i), by
intro i j hij
apply Subtype.ext
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
((((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j)) -
(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
from y.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
((((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i)) -
(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from y.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i)))
rw [map_sub]
exact congrArg₂ HSub.hSub
(congrArg Subtype.val (x.2 i j hij))
(congrArg Subtype.val (y.2 i j hij))⟩Subtraction on the prime-power completed augmentation ideal is defined coordinatewise through the finite-stage augmentation ideals.
instance instSMulNatPrimePowerCompletedGroupAlgebraAugmentationIdeal :
SMul ℕ (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
smul m x := ⟨fun i =>
m • (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from x.1 i), by
intro i j hij
apply Subtype.ext
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
rw [map_nsmul]
exact congrArg (m • ·) (congrArg Subtype.val (x.2 i j hij))⟩The prime-power completed augmentation ideal carries natural-number scalar multiplication coordinatewise at every finite quotient stage.
instance instSMulIntPrimePowerCompletedGroupAlgebraAugmentationIdeal :
SMul ℤ (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
smul m x := ⟨fun i =>
m • (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from x.1 i), by
intro i j hij
apply Subtype.ext
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
rw [map_zsmul]
exact congrArg (m • ·) (congrArg Subtype.val (x.2 i j hij))⟩The prime-power completed augmentation ideal carries integer scalar multiplication coordinatewise at every finite quotient stage.
instance instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
(i : PrimePowerCompletedGroupAlgebraIndex G) :
AddCommGroup ((primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) := by
dsimp [primePowerCompletedGroupAlgebraAugmentationIdealSystem]
infer_instanceAddition in the prime-power completed augmentation ideal is defined coordinatewise through finite stages.
instance instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily :
AddCommGroup
((i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) :=
inferInstanceAddition in the prime-power completed augmentation ideal is defined coordinatewise through finite stages.
theorem coe_zero_primePowerCompletedGroupAlgebraAugmentationIdeal :
((0 : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = 0The inclusion of the completed augmentation ideal preserves zero.
Show proof
by
funext i
rflProof. Work with the prime-power completed augmentation ideal as the coordinatewise kernel of the finite-stage augmentations. Addition, scalar multiplication, inclusion into the completed group algebra, subtype linear maps, and limit equivalences are checked after every prime-power finite stage. The augmentation ideal condition is preserved by transition maps, and inverse-limit extensionality assembles the completed augmentation-ideal statements.
□theorem coe_add_primePowerCompletedGroupAlgebraAugmentationIdeal
(x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
((x + y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = x + yThe inclusion of the completed augmentation ideal preserves addition.
Show proof
by
funext i
rflProof. Work with the prime-power completed augmentation ideal as the coordinatewise kernel of the finite-stage augmentations. Addition, scalar multiplication, inclusion into the completed group algebra, subtype linear maps, and limit equivalences are checked after every prime-power finite stage. The augmentation ideal condition is preserved by transition maps, and inverse-limit extensionality assembles the completed augmentation-ideal statements.
□theorem coe_neg_primePowerCompletedGroupAlgebraAugmentationIdeal
(x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
((-x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = -xThe inclusion of the completed augmentation ideal preserves negation.
Show proof
by
funext i
rflProof. Work with the prime-power completed augmentation ideal as the coordinatewise kernel of the finite-stage augmentations. Addition, scalar multiplication, inclusion into the completed group algebra, subtype linear maps, and limit equivalences are checked after every prime-power finite stage. The augmentation ideal condition is preserved by transition maps, and inverse-limit extensionality assembles the completed augmentation-ideal statements.
□theorem coe_sub_primePowerCompletedGroupAlgebraAugmentationIdeal
(x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
((x - y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = x - yThe inclusion of the completed augmentation ideal preserves subtraction.
Show proof
by
funext i
rflProof. Work with the prime-power completed augmentation ideal as the coordinatewise kernel of the finite-stage augmentations. Addition, scalar multiplication, inclusion into the completed group algebra, subtype linear maps, and limit equivalences are checked after every prime-power finite stage. The augmentation ideal condition is preserved by transition maps, and inverse-limit extensionality assembles the completed augmentation-ideal statements.
□theorem coe_nsmul_primePowerCompletedGroupAlgebraAugmentationIdeal
(m : ℕ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
((m • x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = m • xThe inclusion of the completed augmentation ideal preserves natural-number scalar multiplication.
Show proof
by
funext i
rflProof. Work with the prime-power completed augmentation ideal as the coordinatewise kernel of the finite-stage augmentations. Addition, scalar multiplication, inclusion into the completed group algebra, subtype linear maps, and limit equivalences are checked after every prime-power finite stage. The augmentation ideal condition is preserved by transition maps, and inverse-limit extensionality assembles the completed augmentation-ideal statements.
□theorem coe_zsmul_primePowerCompletedGroupAlgebraAugmentationIdeal
(m : ℤ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
((m • x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = m • xThe inclusion of the completed augmentation ideal preserves integer scalar multiplication.
Show proof
by
funext i
rflProof. Work with the prime-power completed augmentation ideal as the coordinatewise kernel of the finite-stage augmentations. Addition, scalar multiplication, inclusion into the completed group algebra, subtype linear maps, and limit equivalences are checked after every prime-power finite stage. The augmentation ideal condition is preserved by transition maps, and inverse-limit extensionality assembles the completed augmentation-ideal statements.
□instance instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdeal :
AddCommGroup (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :=
Function.Injective.addCommGroup
(fun x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G =>
(x :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i))
Subtype.val_injective
(coe_zero_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
(coe_add_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
(coe_neg_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
(coe_sub_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
(fun x m => coe_nsmul_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) m x)
(fun x m => coe_zsmul_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) m x)Addition in the prime-power completed augmentation ideal is defined coordinatewise through finite stages.