Theorems · Theorem · number theory

baseChange_ext

∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} {N₁ : Type uN₁} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup N₁] [inst_4 : Algebra R A] [inst_5 : Module R N₁]
  [inst_6 : Module A N₁] [IsScalarTower R A N₁] [inst_8 : Module R M₂]
  ⦃Q₁ Q₂ : QuadraticMap A (TensorProduct R A M₂) N₁⦄, (∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)) → Q₁ = Q₂

If two quadratic maps from A ⊗[R] M₂ agree on elements of the form 1 ⊗ m, they are equal. In other words, if a base change exists for a quadratic map, it is unique. Note that unlike QuadraticForm.baseChange, this does not need Invertible (2 : R).

Defined in

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Cited by

2 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Quot.sound

Assumes

CommRingCommRingAddCommGroupAddCommGroupAlgebraModuleModuleIsScalarTowerModule