RightActionInstances.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

15 declarations, 0 contain sorry, 0 declared as axioms

Right-action instances on tensor products

Right-action instances making M ⊗[R] S an S-module / S-algebra when S is a commutative R-algebra. These are scoped instances kept in their own namespace to avoid clashing with the standard left-action instances.

Imports (12)

Imported by 5 files

lemma TensorProduct.RightActions.smul_def line 67 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, AddCommMonoid, Algebra, Module, TensorProduct, Eq, HSMul.hSMul, TensorProduct.RightActions.instSMul, LinearEquiv, RingHom.id, LinearEquiv.symm, TensorProduct.comm
Proof uses: rfl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma TensorProduct.RightActions.algebraMap_eval line 104 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, Algebra, Semiring, Eq, TensorProduct, RingHom, Algebra.algebraMap, TensorProduct.RightActions.instAlgebra, TensorProduct.tmul, OfNat.ofNat
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
def TensorProduct.RightActions.Algebra.TensorProduct.comm The A-algebra isomorphism A ⊗ B = B ⊗ A, available in the TensorProduct.RightActions scope line 107 source
Source documentation
The A-algebra isomorphism A ⊗ B = B ⊗ A, available in the TensorProduct.RightActions scope.

standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, Algebra, Semiring, AlgEquiv, TensorProduct, TensorProduct.RightActions.instAlgebra
Proof uses: Algebra.TensorProduct.comm, AlgEquiv.mk, AlgEquiv.toEquiv
18 instances, coercions and auxiliary constants left out.
```
def Algebra.TensorProduct.comm : A ⊗[R] B ≃ₐ[A] B ⊗[R] A where
…
```
lemma TensorProduct.RightActions.Algebra.TensorProduct.comm_apply_tmul line 112 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, Algebra, Semiring, Eq, TensorProduct, AlgEquiv, TensorProduct.RightActions.instAlgebra, TensorProduct.RightActions.Algebra.TensorProduct.comm, TensorProduct.tmul
Proof uses: Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma TensorProduct.RightActions.Algebra.TensorProduct.comm_symm_apply_tmul line 116 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, Algebra, Semiring, Eq, TensorProduct, AlgEquiv, TensorProduct.RightActions.instAlgebra, AlgEquiv.symm, TensorProduct.RightActions.Algebra.TensorProduct.comm, TensorProduct.tmul
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
def TensorProduct.RightActions.Module.TensorProduct.comm The A-module isomorphism A ⊗ M = M ⊗ A, available in the TensorProduct.RightActions scope line 120 source
Source documentation
The A-module isomorphism A ⊗ M = M ⊗ A, available in the TensorProduct.RightActions scope.

standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, AddCommMonoid, Module, Algebra, LinearEquiv, RingHom.id, TensorProduct, TensorProduct.RightActions.instModule
Proof uses: AddEquiv, LinearEquiv.toAddEquiv, TensorProduct.comm, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, AddEquiv.toEquiv, Equiv.invFun
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def Module.TensorProduct.comm : A ⊗[R] M ≃ₗ[A] M ⊗[R] A where
…
```
lemma TensorProduct.RightActions.Module.TensorProduct.comm_apply_tmul line 132 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, AddCommMonoid, Module, Algebra, Eq, TensorProduct, LinearEquiv, RingHom.id, TensorProduct.RightActions.instModule, TensorProduct.RightActions.Module.TensorProduct.comm, TensorProduct.tmul
Proof uses: rfl
24 instances, coercions and auxiliary constants left out.
lemma TensorProduct.RightActions.Module.TensorProduct.comm_symm_apply_tmul line 135 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, AddCommMonoid, Module, Algebra, Eq, TensorProduct, LinearEquiv, RingHom.id, TensorProduct.RightActions.instModule, LinearEquiv.symm, TensorProduct.RightActions.Module.TensorProduct.comm, TensorProduct.tmul
Proof uses: rfl
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
abbrev TensorProduct.RightActions.LinearMap.baseChange Base extension of an R-linear map V → W to an A-linear map V ⊗ A → W ⊗ A line 159 source
Source documentation
Base extension of an R-linear map V → W to an A-linear map V ⊗ A → W ⊗ A. Available in the TensorProduct.RightActions scope.

standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Algebra, LinearMap, RingHom.id, TensorProduct, TensorProduct.RightActions.instModule
Proof uses: LinearMap.comp, TensorProduct.RightActions.Module.TensorProduct.comm, LinearMap.baseChange, LinearEquiv.symm
20 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev LinearMap.baseChange (R : Type*) [CommRing R]
    (V W : Type*) [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W]
    (A : Type*) [CommRing A] [Algebra R A]
    (φ : V →ₗ[R] W) : V ⊗[R] A →ₗ[A] W ⊗[R] A :=
…
```
lemma TensorProduct.RightActions.LinearMap.baseChange_id line 168 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Algebra, Eq, LinearMap, RingHom.id, TensorProduct, TensorProduct.RightActions.instModule, TensorProduct.RightActions.LinearMap.baseChange, LinearMap.id
Proof uses: LinearMap.ext, of_eq_true, Eq.trans, True, congrFun', congrArg, Function.comp, TensorProduct.RightActions.Module.TensorProduct.comm, LinearMap.comp, LinearMap.baseChange, LinearEquiv.symm, LinearEquiv, LinearMap.comp.congr_simp, LinearMap.baseChange_id, Eq.refl, LinearEquiv.apply_symm_apply, eq_self
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem TensorProduct.RightActions.LinearMap.baseChange_comp line 175 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Algebra, LinearMap, RingHom.id, Eq, TensorProduct, TensorProduct.RightActions.instModule, LinearMap.comp, TensorProduct.RightActions.LinearMap.baseChange
Proof uses: LinearMap.ext, of_eq_true, Eq.trans, LinearEquiv, TensorProduct.RightActions.Module.TensorProduct.comm, LinearMap.baseChange, LinearEquiv.symm, True, congr, congrArg, Function.comp, LinearEquiv.symm_apply_apply, congrFun', LinearMap.comp.congr_simp, LinearMap.baseChange_comp, Eq.refl, eq_self
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
example TensorProduct.RightActions.(example at line 184) line 184 source
abbrev TensorProduct.RightActions.LinearEquiv.baseChange Base extension of an R-linear iso V → W to an A-linear iso V ⊗ A → W ⊗ A line 189 source
Source documentation
Base extension of an R-linear iso V → W to an A-linear iso V ⊗ A → W ⊗ A. Available in the TensorProduct.RightActions scope.

standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Algebra, LinearEquiv, RingHom.id, TensorProduct, TensorProduct.RightActions.instModule
Proof uses: LinearMap, TensorProduct.RightActions.LinearMap.baseChange, LinearEquiv.mk, LinearEquiv.symm
21 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
noncomputable abbrev LinearEquiv.baseChange (R : Type*) [CommRing R]
    (V W : Type*) [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W]
    (A : Type*) [CommRing A] [Algebra R A]
    (φ : V ≃ₗ[R] W) : V ⊗[R] A ≃ₗ[A] W ⊗[R] A where
…
```
def TensorProduct.RightActions.AlgebraMap.baseChange Base extension of an R-algebra map B → C to an A-linear map B ⊗ A → C ⊗ A line 207 source
Source documentation
Base extension of an R-algebra map B → C to an A-linear map B ⊗ A → C ⊗ A. Available in the TensorProduct.RightActions scope.

standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, Ring, Algebra, AlgHom, TensorProduct, TensorProduct.RightActions.instAlgebra
Proof uses: Algebra.TensorProduct.map, AlgHom.id, AlgHom.mk, AlgHom.toRingHom
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def AlgebraMap.baseChange (R : Type*) [CommRing R]
    (B C : Type*) [Ring B] [Algebra R B] [Ring C] [Algebra R C]
    (A : Type*) [CommRing A] [Algebra R A]
    (φ : B →ₐ[R] C) : B ⊗[R] A →ₐ[A] C ⊗[R] A where
…
```
def TensorProduct.RightActions.Algebra.TensorProduct.basis Right action version of Algebra.TensorProduct.basis -- base extension of a basis over a tensor product line 216 source
Source documentation
Right action version of Algebra.TensorProduct.basis -- base extension of a basis over a tensor product.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommSemiring, Algebra, AddCommMonoid, Module, Module.Basis, TensorProduct, TensorProduct.RightActions.instModule
Proof uses: Module.Basis.map, Algebra.TensorProduct.basis, TensorProduct.RightActions.Module.TensorProduct.comm
11 instances, coercions and auxiliary constants left out.
```
def Algebra.TensorProduct.basis {R : Type*} (A : Type*) {M : Type*} {ι : Type*}
    [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M]
    (b : Module.Basis ι R M) :
    Module.Basis ι A (M ⊗[R] A) :=
…
```