Algebraize tactic

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

Further functionality

When given a composition of RingHoms, 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 peformed, we also need to assume that the Algebra property can be constructed only from the homomorphism, so it can not 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 definitonally 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.

def Lean.Attr.algebraizeGetParam (thm : Lean.Name) (stx : Lean.Syntax) : Lean.AttrM Lean.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.

opaque Lean.Attr.algebraizeAttr : Lean.ParametricAttribute Lean.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).

def Mathlib.Tactic.Algebraize.addAlgebraInstanceFromRingHom (f : Lean.Expr) (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 requries 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.

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 RingHoms, 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.

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 RingHoms, 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.

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.

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

Equations

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

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

Function elaborating Algebraize.Config.

Equations

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

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.

def Mathlib.Tactic.tacticAlgebraize____ : Lean.ParserDescr

Tactic that, given RingHoms, 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 (config := {properties := false}), so in other words it only adds Algebra and IsScalarTower instances.

Equations

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

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.