FLT/Mathlib/Algebra/Module/TransferInstance.lean

GitHub source file

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

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

2 declarations, 0 contain sorry, 0 declared as axioms

Transferring a module structure along a bare Equiv

Mathlib PR #42291 replaced Equiv.module and Equiv.linearEquiv with AddEquiv-based versions, on the grounds that "it is typically easy to construct this richer equivalence".

That is not the case when transporting a structure along an arbitrary bijection, as in Finite.equivFin M : M ≃ Fin (Nat.card M): the target carries no additive structure at all until it is transported along the bijection, so there is no AddEquiv to be had beforehand. FLT/Patching/Utils/StructureFiniteness.lean needs exactly that, so we reinstate the original Equiv-based forms here under primed names.

Imports (1)
Imported by 2 files
  1. abbrev Equiv.module' Transfer Module across an Equiv, where the additive structure on the source is itself obtained by transporting the one on the target back along the equivalence line 32 source

    Source documentation

    Transfer Module across an Equiv, where the additive structure on the source is itself obtained by transporting the one on the target back along the equivalence.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Semiring, Equiv, AddCommMonoid, Module, Equiv.addCommMonoid

    Proof uses: AddEquiv.module, Equiv.addEquiv

    3 instances, coercions and auxiliary constants left out.

    protected abbrev module' (e : α ≃ β) [AddCommMonoid β] [Module R β] :
    letI := e.addCommMonoid
…
  2. def Equiv.linearEquiv' Documented declaration: linearEquiv' line 42 source

    Source documentation

    An equivalence e : α ≃ β gives a linear equivalence α ≃ₗ[R] β, where the R-module structure on α is the one obtained by transporting the R-module structure on β back along e.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Semiring, Equiv, AddCommMonoid, Module, LinearEquiv, RingHom.id, Equiv.addCommMonoid, Equiv.module'

    Proof uses: AddEquiv.linearEquiv, Equiv.addEquiv

    5 instances, coercions and auxiliary constants left out.

    def linearEquiv' (e : α ≃ β) [AddCommMonoid β] [Module R β] :
    letI := e.addCommMonoid
…