## Algebraize tactic #

This file defines the `algebraize` tactic. The basic functionality of this tactic is to automatically add `Algebra` instances given `RingHom`s. For example, `algebraize [f, g]` where `f : A →+* B` and `g : B →+* C` are `RingHom`s, will add the instances `Algebra A B` and `Algebra B C` corresponding to these `RingHom`s.

## Further functionality #

When given a composition of `RingHom`s, e.g. `algebraize [g.comp f]`, the tactic will also try to add the instance `IsScalarTower A B C` if possible.

After having added suitable `Algebra` and `IsScalarTower` instances, the tactic will search through the local context for `RingHom` properties that can be converted to properties of the corresponding `Algebra`. For example, given `f : A →+* B` and `hf : f.FiniteType`, then `algebraize [f]` will add the instance `Algebra A B` and the corresponding property `Algebra.FiniteType A B`. The tactic knows which `RingHom` properties have a corresponding `Algebra` property through the `algebraize` attribute.

## Algebraize attribute #

The `algebraize` attribute is used to tag `RingHom` properties that can be converted to `Algebra` properties. It assumes that the tagged declaration has a name of the form `RingHom.Property` and that the corresponding `Algebra` property has the name `Algebra.Property`.

If not, the `Name` of the corresponding algebra property can be provided as optional argument. The specified declaration should be one of the following:

1. An inductive type (i.e. the `Algebra` property itself), in this case it is assumed that the `RingHom` and the `Algebra` property are definitionally the same, and the tactic will construct the `Algebra` property by giving the `RingHom` property as a term. Due to how this is performed, we also need to assume that the `Algebra` property can be constructed only from the homomorphism, so it cannot have any other explicit arguments.
2. A lemma (or constructor) proving the `Algebra` property from the `RingHom` property. In this case it is assumed that the `RingHom` property is the final argument, and that no other explicit argument is needed. The tactic then constructs the `Algebra` property by applying the lemma or constructor.

Here are three examples of properties tagged with the `algebraize` attribute:

    @[algebraize]
    def RingHom.FiniteType (f : A →+* B) : Prop :=
      @Algebra.FiniteType A B _ _ f.toAlgebra

An example when the `Name` is provided (as the `Algebra` does not have the expected name):

    @[algebraize Module.Finite]
    def RingHom.Finite (f : A →+* B) : Prop :=
      letI : Algebra A B := f.toAlgebra
      Module.Finite A B

An example with a constructor as parameter (as the two properties are not definitionally the same):

    @[algebraize Algebra.Flat.out]
    class RingHom.Flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) : Prop where
      out : f.toAlgebra.Flat := by infer_instance

## algebraize_only #

To avoid searching through the local context and adding corresponding `Algebra` properties, use `algebraize_only` which only adds `Algebra` and `IsScalarTower` instances.

source
def Lean.Attr.algebraizeGetParam (thm : Name) (stx : Syntax) :
AttrM Name

Function that extracts the name of the corresponding `Algebra` property from a `RingHom` property that has been tagged with the `algebraize` attribute. This is done by either returning the parameter of the attribute, or by assuming that the tagged declaration has name `RingHom.Property` and then returning `Algebra.Property`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
opaque Lean.Attr.algebraizeAttr :
ParametricAttribute Name

A user attribute that is used to tag `RingHom` properties that can be converted to `Algebra` properties. Using an (optional) parameter, it will also generate a `Name` of a declaration which will help the `algebraize` tactic access the corresponding `Algebra` property.

There are two cases for what declaration corresponding to this `Name` can be.

1. An inductive type (i.e. the `Algebra` property itself), in this case it is assumed that the `RingHom` and the `Algebra` property are definitionally the same, and the tactic will construct the `Algebra` property by giving the `RingHom` property as a term.
2. A lemma (or constructor) proving the `Algebra` property from the `RingHom` property. In this case it is assumed that the `RingHom` property is the final argument, and that no other explicit argument is needed. The tactic then constructs the `Algebra` property by applying the lemma or constructor.

Finally, if no argument is provided to the `algebraize` attribute, it is assumed that the tagged declaration has name `RingHom.Property` and that the corresponding `Algebra` property has name `Algebra.Property`. The attribute then returns `Algebra.Property` (so assume case 1 above).

source
def Mathlib.Tactic.Algebraize.addAlgebraInstanceFromRingHom (f ft : Lean.Expr) :
Lean.Elab.Tactic.TacticM Unit

Given an expression `f` of type `RingHom A B` where `A` and `B` are commutative semirings, this function adds the instance `Algebra A B` to the context (if it does not already exist).

This function also requires the type of `f`, given by the parameter `ft`. The reason this is done (even though `ft` can be inferred from `f`) is to avoid recomputing `ft` in the `algebraize` tactic, as when `algebraize` calls `addAlgebraInstanceFromRingHom` it has already computed `ft`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.Algebraize.addIsScalarTowerInstanceFromRingHomComp (fn : Lean.Expr) :
Lean.Elab.Tactic.TacticM Unit

Given an expression `g.comp f` which is the composition of two `RingHom`s, this function adds the instance `IsScalarTower A B C` to the context (if it does not already exist).

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.Algebraize.addProperties (t : Array Lean.Expr) :
Lean.Elab.Tactic.TacticM Unit

This function takes an array of expressions `t`, all of which are assumed to be `RingHom`s, and searches through the local context to find any additional properties of these `RingHoms`, after which it tries to add the corresponding `Algebra` properties to the context. It only looks for properties that have been tagged with the `algebraize` attribute, and uses this tag to find the corresponding `Algebra` property.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
structure Mathlib.Tactic.Algebraize.Config :
Type

Configuration for `algebraize`.

- properties : Bool

  If true (default), the tactic will search the local context for `RingHom` properties that can be converted to `Algebra` properties.

Instances For

source
instance Mathlib.Tactic.Algebraize.instInhabitedConfig :
Inhabited Config
Equations

- Mathlib.Tactic.Algebraize.instInhabitedConfig = { default := Mathlib.Tactic.Algebraize.instInhabitedConfig.default }

source
def Mathlib.Tactic.Algebraize.instInhabitedConfig.default :
Config
Equations

- Mathlib.Tactic.Algebraize.instInhabitedConfig.default = { properties := default }

Instances For

source
def Mathlib.Tactic.Algebraize.elabAlgebraizeConfig :
Lean.Syntax → Lean.Elab.Tactic.TacticM Config

Function elaborating `Algebraize.Config`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.algebraizeTermSeq :
Lean.ParserDescr

A list of terms passed to `algebraize` as argument.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.tacticAlgebraize__ :
Lean.ParserDescr

Tactic that, given `RingHom`s, adds the corresponding `Algebra` and (if possible) `IsScalarTower` instances, as well as `Algebra` corresponding to `RingHom` properties available as hypotheses.

Example: given `f : A →+* B` and `g : B →+* C`, and `hf : f.FiniteType`, `algebraize [f, g]` will add the instances `Algebra A B`, `Algebra B C`, and `Algebra.FiniteType A B`.

See the `algebraize` tag for instructions on what properties can be added.

The tactic also comes with a configuration option `properties`. If set to `true` (default), the tactic searches through the local context for `RingHom` properties that can be converted to `Algebra` properties. The macro `algebraize_only` calls `algebraize -properties`, so in other words it only adds `Algebra` and `IsScalarTower` instances.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.tacticAlgebraize_only__ :
Lean.ParserDescr

Version of `algebraize`, which only adds `Algebra` instances and `IsScalarTower` instances, but does not try to add any instances about any properties tagged with `@[algebraize]`, like for example `Finite` or `IsIntegral`.

Equations

- One or more equations did not get rendered due to their size.

Instances For